2 колок

38) Визначення теорії 1-го порядку. Числення предикатів 1-го порядку.

Під теорією 1-го порядку розуміємо формальну систему T=(L, A, P), де L мова 1-го порядку, A  множина аксіом, яка розбита на множину логічних аксіом і множину власних аксіом, P множина правил виведення.

39) Модель теорії 1-го порядку. Теорема істинності

Моделлю теорії 1-го порядку T називається інтерпретація мови теорії, на якій істинні всі власні аксіоми теорії T.

Формула  називається істинною в теорії T, якщо  істинна на кожній моделі теорії T.

Теорема 6.1.2 (теорема істинності). Кожна теорема теорії 1-го порядку T істинна в T.

40) Теорема тавтології

Кожна тавтологія є теоремою.

Наслідок. Якщо {₁, ..., _n}╞  та ₁, ..., _n , то .

41) Теорема дедукції

Нехай A  замкнена формула. Тоді для довільної формули B маємо: T AB  T [A] B.

Наслідок. Нехай A₁, ..., A_n  замкнені формули. Тоді для довільної формули B маємо T A₁...A_nB  T [A₁, ..., A_n] B.

42) Визначення несуперечливості теорії 1-го порядку, повної (максимальної) теорії 1-го порядку

Теорія 1-го порядку T називається несуперечливою, якщо не існує формули  такої, що T | та T | .

Несуперечлива теорія 1-го порядку T називається повною, якщо для кожної замкненої формули  маємо T | або T | .

43) Теорема Лінденбаума

Кожна нeсупeрeчлива теорія 1-го порядку має нeсупeрeчливe простe повнe розширeння.

44) Поняття розвязності, перелічності теорії 1-го порядку. Теорема про розвязність

Розв'язність теорії означає алгоритмічну розв'язність множини її теорем відносно множини всіх формул мови теорії.

Перелічність означає: множина теорем теорії алгоритмічно перелічна.

Нехай T  повна теорія 1-го порядку із алгоритмічно перелічною множиною аксіом. Тоді T розв’язна.

Наслідок. Кожна повна перелічна теорія 1--го порядку розв’язна.

45) Теорема Гьоделя про повноту, 1-е та 2-е формулювання

Теорема (теорема Гьоделя про повноту, 1-е формулювання). Нехай T  теорія 1-го порядку. Тоді формула  істинна в T  T .

Теорема (теорема Гьоделя про повноту, 2-е формулювання). Теорія 1-го порядку T несуперечлива  T має модель.

46) Теорема компактності

Приклад (теорема компактності, 1-е формулювaння). Формула  істинна в T   істинна в деякій САЧ КT.

Приклад (теорема компактності, 2-е формулювання). Теорія 1-го порядку T має модель  кожна САЧ теорії T має модель.

47) Теореми Льовенгейма-Сколема

Теорема (теорема Льовенгейма-Сколема про спуск). Нехай теорія 1-го порядку T потужності  має модель, тоді T має модель потужності .

Теорема (теорема Льовенгейма-Сколема про підйом) Нехай теорія 1-го порядкуTпотужностімає нескінченну модель. ТодіTмає модель довільної потужності.

48) Визначення категоричності, а-категоричної теорії 1-го порядку. Теорема Лося-Воота

Теорія 1-го порядку категорична, якщо всі її моделі ізоморфні.

Теорія 1-го порядку T -категорична, якщо всі її моделі потужності  ізоморфні.

Теорема (Лось-Воот). Нехай   деяка нескінченна потужність. Нехай T  несуперечлива теорія потужності , всі моделі якої нескінченні, причому T -категорична.. Тоді T  повна теорія.

49) Секвенційні числення класичних логік 1-го порядку. Базові секвенційні форми

Враховуючи, що для класичних логік на кванторному рівні базовими є композиції ,  та x, для секвенцій відмічених формул можна ввести базові секвенційні форми _, _, _, _ та _ і _:

_ _

_ _

_ _ .

50) Секвенційні числення НКЛ кванторного рівня. Базові секвенційні форми

Для секвенцій відмічених формул вводимо такі базові секвенційні форми:

_ _

_ _

_RT _RT

_RR _RR

_R _R

_R _R

_N при y(A) _N при y(A)

_R _R

_R _R