ія виведена в численні предикатів. Ми сформулюємо це твердження у вигляді леми. p align="justify"> Лемма 3.53. Нехай A1, A2,. . . , An-формули обчислення предикатів, а ? (x1, ..., xn) - тавтологія, до якої входять змінні x1,. . . , Xn. Тоді формула ? (A1, ..., An) виведена в численні предикатів.
Доказ цієї леми очевидно: потрібно підставити в висновок формули ? в обчисленні висловлювань замість змінних xi формули Ai. Отримана послідовність формул буде виводом в численні предикатів.
Ослаблена і слабка теорема дедукції
Теорема 3.54 (ослаблена теорема дедукції). Якщо ?, A ? B і існує висновок B з ?, A, в якому не застосовується правило узагальнення до вільних змінним формули A, то ? ? A? B.
Доказ. Слідуємо схемою доведення теореми дедукції для обчислення висловлювань: висновок ? 1,. . . ,? N формули B з гіпотез ?, A, який існує по умовою теореми, замінюється на послідовність формул A? ? 1,. . . , A ? ? N і індукцією по n доводиться, що цю послідовність можна доповнити до виводу. Для цього треба розібрати два випадки.
. Формула ? I є аксіомою (A1-A5) або формула ? I отримана за правилом modusponens з попередніх формул ? j,? k, j, k У цих випадках побудова виведення A? ? I в припущенні, що вже виведені формули A? ? k, k в точності повторює доказ теореми дедукції для обчислення висловлювань.
. Формула ? I є висновком за правилом Gen з формули ? K, k Це означає, що ? I = ? x? k. Додамо такі формули перед формулою A? ? I:
? x (A? ? k) (Gen)
? x (A? ? k) ? ( A? ? x? k) (A5)
У першому рядку правило узагальнення застосовується до формули A? ? k, яка зустрічається раніше формули A? ? i в послідовності формул, яку ми поповнюємо. Другий рядок - це аксіома (A5). Умови затвердження 3.45 (В«Якщо у формулі A немає вільних входжень змінної x, то формула
? x (A? B)? (A? ? xB)
общезначима В») в даному випадку виконані, тому що за умовою x не є вільною змінною формули A.
Слідство 3.55 (слабка теорема дедукції).
Якщо ?, A ? B іформула A замкнута, то ? ? A? B.
Доказ. Замкнута формула взагалі не містить вільних змінних, тому будь-який висновок B з ?, A задовольняє умові теореми 3.54.
Теорема про повноту ІП
Теорема про повноту для ІП:
У будь-якому ІП 1-го порядку формула є тавти-їй <=> вона загальнозначущої.
Док-во:
Покажемо, що якщо - теорема, то вона общезначима.
Перевіряємо безпосередньо, що схеми аксіом явл. загальнозначимі: (A 1 ) - (A 5 )
MP і G...
