Выполнимость и общезначимость формул логики предикатов. Теорема Черча

Формула A выполнима в данной интерпретации, если существует набор <s1, …, sn> значений свободных переменных x1, …, xn формулы A, такой что A(s1, …, sn) = 1.

Формула A истинна в данной интерпретации, если она принамает значение 1 на любом наборе <s1, …, sn> значений своих свободных переменных x1, …, xn.

Формула A общезначима или тождественно – истинна (в логике предикатов), если она истинна в каждой интерпретации.

Формула A выполнима (в логике предикатов), если существует интерпретация, в которой она выполнима.

Формула A общезначима тогда и только тогда, когда формула A не является выполнимой, и формула A выполнима тогда и только тогда, когда формула A не является общезначимой.

Очевидно, что если F и G равносильные (в логике предикатов) формулы, то F ~ G – общезначимая формула.

Теорема Чёрча: не существует алгоритма, который для любой формулы логики предикатов устанавливает, общезначима она или нет. Без доказательства. Другими словами, логика предикатов не разрешима (для предикатов нет таблицы истинности).

19. Исчисление предикатов: аксиомы и правила вывода. Ослабленная теорема о дедукции.

Сформулированное в логике предикатов определение формулы остаётся в силе и для ИП (с той лишь разницей, что в ИП употребляются только два логических символа: , ). Остальные логические символы можно ввести так, как это сделано в ИВ. К системе аксиом исчисления высказываний в исчислении предикатов добавляются ещё две: А4 и А5 (или 11 и 12). При решении задач по исчислению предикатов можно пользоваться одной из двух систем аксиом ИП (двумя сразу нельзя). Каковы бы ни были формулы A, B и C следующие формулы являются аксиомами ИП (при этом не должно нарушаться определение формулы):

А1. А (В А) 1. А (В А)

А2. (А (В С)) ((А В) (А С)) 2. (А В) ((А (В С)) (А С))

А3. ( В А) (( В А) В) 3. А В А

A4.( x)А(x) А(y), где y A(x) 4. А В В

A5.А(y) ( x)А(x), где y A(x) 5. А (В (А В))

6. А (А В)

7. В (А В)

8. (А С) ((В С) ((А В) С)

9. (А В) ((А В) А)

10. А А

11.( x)А(x) А(y), где A(x) не содержит y

12.А(y) ( x)А(x), где A(x) не содержит y

При выводе в ИП можно использовать и 7 теорем: Т1. А А. Т2. А А. Т3. А (А В). Т4. ( В А) (А В). Т5. (А В) ( В А). Т6. А ( В (А В)). Т7. (А В) (( А В) В).