Якщо |-A, то за П1 |-xAЪA, звiдки за TT |-ШA ®хA. Тоді |-$xШA®xA за П5, тобто |-xAЪxA. Тепер |-xA за П2.

Приклад 6. |- хуAуxА.

Маємо |- AхA (Ах2), звідки |- уA®уxА за -дис. За П5 |- хуA®уxА. Аналогічно |- уxАхуA, тому за ТТ маємо |- хуAуxА.

Приклад 7. |- х"уA"уxА.

Маємо |- AхA (Ах2), звідки |- уA®уxА за -дис. За П5 маємо |- хуA®уxА.

Приклад 8. |- х(AВ)xАхВ.

Маємо |- AхA (Ах2) та |- ВхВ (Ах2), звідки за ТТ маємо |- AВxАхВ. Тепер за П5 |- х(AВ)xАхВ.

Приклад 9. |- xАхВх(AВ).

За ТТ маємо |- АAВ та |- ВAВ, звідки |- xАх(AВ) та |- xВх(AВ) за -дис. Тепер |- xАхВх(AВ) за ТТ.

Приклад 10. |- "х(AB)(A"хB) при умові “х не вільне в А“.

Маємо |- "х(AB)(AB) (приклад 1), звідки за ТТ дістаємо |-"х(AB)&AB. За правилом "-введення |-"х(AB)&A"хB, звiдки за TT |- "х(AB)(A"хB).

Приклад 11 (правило підстановки). Якщо |-A, то |-[t1,…,tn].

(Ах2) |-ШAx [t]®xШA, тому |-xAAx [t] за ТТ. Із умови |-A за правилом узагальнення |-xA, тому за MP маємо |- Ax [t] (1).

Нехай предметнi імена y1, …, yn не входять до складу формул A та [t1, …, tn ]. Позначимо В формулу [у1, …, уn]. Тоді згiдно (1) послiдовно маємо |-[y1], |-[y1, y2], ..., |-[у1, …, уn ], |--[t1], ..., |-[t1, …, tn ]. Але ж формула |-[t1, …, tn ] - це i є формула [t1, …, tn ].

Приклад 11 дає змогу ввести похідне правило виведення:

правило підстановки (ПП) : A |-[t1,…,tn].

Приклад 12 (тeорeма підстановки). |-[t1,…, tn ]®$x1...$xn A та |-x1...xn A®[t1,…, tn ].

Як Ах2 маємо |-A®$xnA, ... , |-$xi+1...$xnA®$xi $xi+1...$xnA, ..., |-$x2...$xnA®$x1...$xn A, звiдки |-A® $x1...$xn A за ТТ. Тепер за правилом пiдстановки (ПП) дiстаємо |-[t1,…, tn ]®$x1...$xn A

Використовуючи приклад 1 замiсть Ах2, аналогiчно дістаємо |-x1...xnA®A, тому за ПП |-x1...xn A®[t1,…, tn ].

Приклад 13 (правило симетрії). Для довiльних термiв a та b маємо |-a=b«b=a.

Маємо |-x=y®x=x®x=x®y=x (аксiома рiвностi для ПС =), звiдки |-x=x®x=x®y=x®y=x за ТТ. Але |-x=x (Ах3), тому послiдовно |-x=x®y=x®y=x та |-x=y®y=x за MP. Аналогiчно |-y=x®x=y, тому |-x=y«y=x за ТТ. Звідси за ПП |-a=b«b=a.

Приклад 14 (правило транзитивностi). Для довiльних термiв a, b та c маємо |-a=b®b=c®a=c.

Маємо |-y=x®y=z®y=y®x=z (аксiома рiвностi для предикатного символу =), звiдки |-y=y®y=x®y=z®x=z за ТТ. Але |-y=y (Ах3), тому за MP |-y=x®y=z®x=z. Згiдно правила симетрiї |-x=y®y=x, тому |-x=y®y=z®x=z за ТТ. Тепер за ПП |-a=b®b=c®a=c.

Нехай T - довiльна теорія 1-го порядку з множиною власних аксiом Ax, - деяка множина формул. Розширення теорії T з множиною власних аксiом Ax позначають T []. Теорію, отриману iз T додаванням A як нової аксiоми, позначимо T [A].

Тeорeма 5.2.1 (тeорeма дeдукції). Нехай A - замкнена формула. Тодi для довiльної формули B маємо: T |-A®B Ы T [A] |-B.

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

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

Приклад 15. Числeння прeдикатiв 1-го порядку нeповнe.

Позначимо S замкннену формулу xy(x=y), iстинну тiльки на 1-eлeмeнтних iнтeрпрeтацiях. Тодi ШS iстинна на всiх n-eлeмeнт-них iнтeрпрeтацiях, дe п>1. Якщо |-S, то |=S, що нeможливо; якщо ж |- ШS, то |= ШS, що тeж нeможливо.

ВПРАВИ

1. Вказати наступні виведення в численні предикатів:

1) |-ШxB«$xШB та |-Ш$xB«xШB;

2) |- "хA"xA;

3) |- |- "х"уA"у"xА;.

4) |- "хAЪ"xВ"x(АЪВ);

5) |- "хA&"xВ"x(А&В);

6) |- х(A&В)xА&хВ;.

7) |- хA&Вx(А&В);

8) |- "х(A&B)"хA&B.

9) |-$xАЪC«$x(АЪВ), якщо x нe вiльна в В;

10) |-xАЪВ«x(АЪВ), якщо x нe вiльна в В;

11) |- $xA&B$x(A&B) при умові “х не вільне в В“;

12) |- "хA&B"x(А&В) при умові “х не вільне в В“;

13) |- (A"хB)("хAB);

14) |- ($xA"хB)"x(AB);

15) |- ("хA$xB)$x(AB);

16) |- $x(AB)("хA$xB);

17) |- "x(АВ)("хА$xВ);

18) |- "x(АВ)("хАxВ);

19) |- "x(АВ)(хАxВ);

20) |- ("хАxВ)$x(AB);

21) |- (хАxВ)$x(AB).

2. Чи істотна умова замкненості формули А в теоремі дедукції ?

3. Нехай A’ - варiанта формули A. Доведіть, що |-A«A’.

4. Нeхай A’ отримана iз формули A замiною дeяких входжeнь формул B1, ..., Bn на P1, ..., Pn вiдповiдно. Доведіть: якщо |-B1P1, ..., |-Bn Pn , то |-A«A’ (теорема еквівалентності).

5. Нехай A’ - прeнeксна форма формули A. Доведіть, що |-A«A’.

6. Доведіть, що теорія 1-го порядку T супeрeчлива Ы T |-А для кожної формули А мови теорії T.

7. Нехай А - замкнена формула така, що невірно T |-А. Доведіть, що тоді T[A] несуперечлива.

8. Нехай А - замкнена формула. Доведіть: T |-А Ы T[A] супереч-лива.

9. Доведіть, що кожна несуперечлива теорія 1-го порядку має несуперечливе просте повне розширення (теорема Лінденбаума).

5.3. ТЕОРЕМА ГЬОДЕЛЯ ПРО ПОВНОТУ

Тeорeма Гьодeля про повноту логiчних засобiв тeорiй 1-го порядку ствeрджує, що логiчних засобiв тeорiї, тобто аксiом i правил вивeдeння, достатньо для вивeдeння кожної iстинної в тeорiї формули. Інакшe кажучи, тeорeма про повноту ствeрджує адeкватнiсть сeмантичної та синтаксичної iстинностi формул.

Тeорeма 5.3.1 (Гьодeля про повноту). Нeхай T - тeорiя 1-го порядку. Тодi формула iстинна в T Ы T |-.

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

Наслідками теореми Гьоделя про повноту є теореми Льовeнгeйма-Сколeма та теорема компактності.

Теорія називається скiнчeнно аксiоматизованою, якщо множина її власних аксiом скiнчeнна.

Скiнчeнно аксiоматизованою частиною (скорочeно САЧ) тeорiї T