ЗВ'ЯЗОК З ТЕОРЕМОЮ ГЕДЕЛЯ ПРО ПОВНОТУ

В описаній вище процедурі автоматичного доведення теорем була використана деяка допоміжна дедуктивна система, яка використовує три правила виводу - переобозначеніе змінних, правило резолюції і правило склеювання. Роль аксіом в ній грали диз'юнкт, отримані в процесі перетворень заперечення вихідної теореми. "Повнота '* цієї дедуктивної системи полягала в можливості отримання за кінцеве число кроків константи" брехня "для будь-якого нездійсненного безлічі диз'юнктів. Виявляється, що використана при встановленні даної повноти техніка дуже близька до техніки, яка застосовується для доведення теореми Геделя про повноту наведеної на початку розділу класичної дедуктивної системи логіки предикатів. Щоб провести зіставлення, дамо тут короткий нарис схеми доведення теореми Геделя.

Перш за все, нам знадобиться поняття теорії першого порядку. Це - довільна дедуктивна система, отримана з дедуктивної системи логіки предикатів додаванням деякого (кінцевого або нескінченного) безлічі аксіом. Теорію першого порядку називають суперечливою , якщо в ній виведені одночасно будь-яка формула і її заперечення. Очевидно, в такому випадку в ній виводиться взагалі будь-яка формула. Одна теорія першого є розширенням інший, якщо кожна формула, виведена в другій теорії, виведена також у першій. Нарешті, введемо поняття повної теорії, тобто такий, в якій для будь-якої замкнутої формули виводиться або вона, або її заперечення.

Першим кроком доведення теореми Геделя є встановлення наступної леми Лінденбаума:

Лемма 18. Якщо теорія першого порядку несуперечлива, то існує несуперечливе повне її розширення.

Доказ леми засноване на розгляді послідовності Fo, Fi, ..., що перераховує всі замкнуті формули логіки предикатів. Починаючи з вихідної несуперечливої теорії Т, по цій послідовності будується послідовність теорій Т = Те, 7, ____ Щоразу, як виявляється, що

формула - "Fj не виводиться в теорії 7 *, теорія Т» +1 виходить з Т { додаванням Fi в якості аксіоми. В іншому випадку покладається Т * + 1 = TJ. Потім розглядається теорія Т ', безліч аксіом якої є об'єднанням множин аксіом всіх теорій Те, Т 9 .... Як легко бачити, Т' являє собою несуперечливе повне розширення теорії Т. Дана конструкція цілком аналогічна конструкції, яку застосовували при доведенні теореми Ербрана, коли визначалася нескінченна послідовність істиннісних значень термів ербра- ського універсуму.

Якщо в деякій інтерпретації логіки предикатів істинними все аксіоми теорії першого порядку Т, то називаємо її моделлю теорії Т. Далі доводиться наступна лема:

Лемма 19. Будь-яка несуперечлива теорія першого порядку має модель зі лічильної областю.

Нехай Т - несуперечлива теорія першого порядку. Розглянемо послідовність Fi (xi), F2 (x2), ..в якій перераховуються всі формули логіки предикатів, що містять не більше однієї вільної змінної. Нехай також ai, a2, ... - послідовність різних предметних констант, таких, що ai не міститься в формулах Fi (xi), ..., Fj (xj). Введемо в розгляд формулу 5 П виду -iV Xi jFJ (x *) -> -iFj (a *). Визначаємо теорію Т п як результат приєднання до Т аксіом S , ..., S n , а теорію Т ' - як результат приєднання до Т аксіом Si, S2, - Очевидно, що для встановлення несуперечності Т * досить встановити несуперечливість кожної теорії Т п ; п = 1,2, ____ Останнє неважко встановити індукцією по п. Зауважимо, що формула S n еквівалентна формулі B Xi Gi (xi) -? Gi (ai) y де Gi (xi) є "• Fj (xi). Таке уявлення пояснює сенс додавання аксіом S n : вони дозволяють перейти від формули з зовнішнім квантором існування до формули, отриманої з неї відкиданням квантора і підстановкою "нової" константи замість подкванторной змінної. Цей перехід аналогічний переходу, виконують вище при отриманні сколемовской нормальної форми.

Після встановлення несуперечності теорії Т ' застосовуємо лему Лінденбаума, згідно з якою вона має несуперечливе повне розширення Т ". Використовуючи теорію Т", безпосередньо вказуємо інтерпретацію для теорії Т, в якій істинні всі її аксіоми. Ця інтерпретація будується аналогічно тому, як будувалася інтерпретація в доведенні теореми Ербрана. Областю інтерпретації тут служить безліч М всіх термів, які не мають змінних. Очевидно, воно лічильно. Інтерпретацією константи служить вона сама; функціональний символ / арності п інтерпретується операцією, що переводить терми? i, ..., t n в терм f (t .. Л п ). Ставлення, що є інтерпретацією предикатного символу Р арності п, істинно на наборі термів t y ... y t n тоді і тільки тоді, коли формула P (t ... t n ) виведена в теорії Т ". Доказ того, що в зазначеної інтерпретації буде істинною будь-яка формула F, що виводиться в теорії Т ", здійснюється порівняно нескладної індукцією по побудові формули F. Оскільки будь-яка формула, виведена в Т, виведена також в теорії Т", отримуємо звідси, що побудована інтерпретація є моделлю для Т.

Щоб довести тепер теорему Геделя про повноту, розглянемо довільну замкнуту общезначимую формулу F логіки предикатів. Якщо ця формула не виводиться в логіці предикатів, то можна приєднати її заперечення до аксіом і отримати несуперечливу теорію першого порядку. За доведеною леми, вона має модель. У цій моделі одночасно повинні бути щирі і загальнозначуща формула F, і її заперечення. Отримане протиріччя і встановлює виводимість формули F.

 
Переглянути оригінал
< Попер   ЗМІСТ   ОРИГІНАЛ   Наст >