НОУ ІНТУЇТ | лекція | обчислення предикатів

1. загальнозначущі формули

Анотація: Розглядається обчислення, аналогічне обчисленню висловлювань, для формул першого порядку, аксіоми, правила виведення, області дії формул, питання коректності

загальнозначущі формули

Обчислення висловлювань ( "Обчислення висловлювань" ) Дозволяло виводити все тавтології з деякого набору базисних тавтологію (названих аксіомами) за допомогою деяких правил виведення (насправді єдиного правила modus ponens). Зараз ми хочемо вирішити аналогічну задачу для формул першого порядку. Відповідне обчислення називається обчисленням предикатів.

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

Загальнозначущі формули в логіці предикатів грають ту ж роль, що тавтології в логіці висловлювань. Між ними є і формальний зв'язок: якщо взяти будь-яку тавтологію і замість вхідних в неї пропозіціональних змінних підставити довільні формули сигнатури , Вийде загальнозначуща формула. Справді, нехай є деяка інтерпретація сигнатури і деяка оцінка (тобто фіксовані значення індивідуальна змінних). Тоді кожна з підставлених формул стане істинною або помилковою, а значення всієї формули визначається за допомогою таблиць істинності для логічних зв'язок, тобто за тими ж правилами, що в логіці висловлювань.

Звичайно, бувають і інші загальнозначущі формули, які не є приватним випадками пропозіціональних тавтологію. Наприклад, формула

общезначима (тут істотно, що носій будь-якій інтерпретації непорожній). Інші приклади загальнозначущих формул (у другому випадку - довільна формула):

87. Чи буде общезначима формула (а) ; (Б) ?

Багато питань можна сформулювати як питання про общезначимости деяких формул. Наприклад, можна записати властивості рефлексивності, транзитивності і антисиметричність у вигляді формул , і сигнатури і потім написати формулу

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

88. Напишіть формули і перевірте, що наведена нами формула не общезначима, хоча істинна у всіх кінцевих інтерпретаціях.

89. Відомо, що формула істинна у всіх кінцевих і рахункових інтерпретаціях. Чи можна з цього зробити висновок, що вона общезначима? (Вказівка: скористайтеся теоремою Левенгейма-Сколема про елементарну подмодели.)

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

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

Двоїсте до общезначимости поняття - здійснимість. Формула називається здійсненною, якщо вона істинна в деякій інтерпретації на деякій оцінці. Очевидно, формула общезначима тоді і тільки тоді, коли формула не є здійсненним.

90. Закінчите твердження: здійсненність формули з параметрами рівносильна здійсненності замкнутої формули, яка вийде, якщо \,

Щоб перевірити, чи є формула тавтологією, досить підставити в неї всі можливі набори значень змінних. Хоча цей процес може бути на практиці нездійсненний (наборів занадто багато), теоретично ми маємо простий алгоритм перевірки, чи є формула тавтологією. Для загальнозначущих формул в загальному випадку такого алгоритму не існує (теорема Черча; її доказ можна прочитати в [5] ); він є тільки для дуже обмежених класів формул. Наприклад, якщо сигнатура містить тільки нульместние предикатні символи, то завдання по суті зводиться до перевірки тавтологічні (в цьому випадку квантори фіктивні). Трохи складніший випадок з одномісними предикатами.

91. Нехай сигнатура містить тільки одномісні предикати. Доведіть, що будь-яка здійсненне формула цієї сигнатури, що містить різних предикатів, здійсненна в деякій кінцевої інтерпретації, що містить не більше елементів. Як використовувати цей факт для алгоритмічної перевірки виконуваності формул такий сигнатури?