n="justify">? xA? A (x: = t) общезначима.
Доказ:
Якщо висновок імплікації істинно, то і вся імплікація істинна.
Тепер припустимо, що в деякій інтерпретації при деякій оцінці змінних ? формула A (x: = t) має оцінку брехня.
Позначимо через ? оцінку терма t при оцінці змінних ?. Розглянемо оцінку змінних ? ?, Яка відрізняється від оцінки ? хіба що у змінній x, оцінка ? ? якої дорівнює ?. Порівняємо оцінку формули A при оцінці змінних ? ? та оцінку формули A (x: = t) при оцінці змінних ?.
Так як терм t вільний для змінної x у формулі A, то вільні всі входження змінних в примірники терма t, підставлені замість вільних входжень x. Тому при оцінці формули A (x: = t) оцінка будь-якої вершини, яка лежить на шляху від вершини t до кореня, використовує лише оцінку ? терма t при оцінці змінних ? ( останнє правило оцінки не застосовується, оскільки всі входження змінних втерм t вільні).
У точності ті ж оцінки отримають ці вершини, коли обчислюється оцінка формули A при оцінці змінних ? ?.
В інших вершинах оцінки формул A і A (x: = t) і поготів збігаються (там записано одне і те ж).
Отже, при оцінці змінних ? ? оцінкою формули A є брехня. Те ж саме вірно для формули A (x: = t) при оцінці ?. Тоді за останнім правилом оцінки формула ? xA має оцінку брехня при оцінці ?. Значить, в цьому випадку оцінка формули ? xA? A (x: = t) - істина.
Отже, при обох можливих оцінках формули A (x: = t) формула ? xA? A (x: = t) має оцінку істина. Тому вона загальнозначуща.
Коректність ІП і наслідки з неї
Теорема. У ІП виводяться тільки загальнозначущі формули. p align="justify"> Доказ. Потрібно перевірити загальзначимість аксіом і те, що правила виведення зберігають загальзначимість. Ми вже довели загальзначимість аксіом: аксіоми (A1-A3) загальнозначимі по затв. 3.38 (В«Нехай A - тавтологія, x1, ..., xn - набір пропозіціональних змінних, які входять в A, а F1, ..., Fn - формули ВП. Тоді формула A (F1, ..., Fn) - общезначима В»), а загальзначимість аксіом (A4-A5) доведена в утвержденіях3.48, 3.45 (В« Якщо терм t вільний для змінної x у формулі A, то формула ? xA? A (x: = t)-общезначима В»іВ« Якщо у формулі A немає вільних входжень змінної x, то формула ? x (A? B)? (A? ? xB) - общезначима В»).
(A1)
(A2)
(A3)
(A4) в умовах 3.48
(A5) в умовах 3.45
Якщо при деякій оцінці змінних формулиA, A? B істинні, то і формула B також істинна при цій оцінці змінних. Тому правило modusponens з загальнозначущих формул виводить тільки загальнозначущі. p> Залишається перевірити, що правило узагальнення зберігає загальзначимість. Дійсно, з общезначимости A випливає, що в будь-якій інтерпретації при будь оцінці змінних вона істинна. Але тоді за визначенням інтерпретації квантора формула? X A також істинна в будь-якій інтерпретації при будь оцінці змінних. p> Як наслідок отримуємо несуперечливість числення предикатів. Оскільки в численні предикатів виводяться тільки загальнозначущі формули, то з формул A і - | A виведеної може бути тільки одна. p align="justify"> Буквально так само, як в обчисленні висловлювань, визначається висновок з безлічі формул (гіпотез). Формули, що виводяться з аксіом числення предикатів і аксіом деякої теорії T, називаються виведеними в T або (формальними) теоремами теорії T. Так як аксіоми числення предикатів містять аксіоми числення висловів, а правило modus ponens є одним з правил виведення, то будь-яка тавтолог...
