Полнота и непротиворечивость исчисления предикатов

Теорема полноты и корректности аксиоматического исчисления (теорема Геделя, [4]). Формула j логики предикатов выводима из множества предложений S тогда и только тогда, когда j является следствием S. Формально S ├ j ÛS╞ j.

Следствие. Формула j выводима из аксиом логики предикатов тогда и только тогда, когда j общезначима. Формально ├ j Û╞ j.

Секвенция Ф₁, Ф₂,..., Ф_n |- Ф истинна в модели M = (D,S), если из истинности формул Ф₁, Ф₂,..., Ф_n в модели M следует истинность Ф в этой модели.

Секвенция |- Ф истинна в модели M, если формула Ф тождественно истинна в этой модели.

Теорема. Каждая доказуемая секвенция тождественно истинна.

Доказательство основано на очевидных положениях:

1. Все аксиомы исчисления предикатов истинны.

2. Истинность секвенций, вводящих логические связки, доказывается в исчислении высказываний.

3. Истинность секвенций, вводящих кванторы, доказывается с помощью теорем для кванторов.

Определение противоречивости исчисления: формальное исчисление, заданное множеством аксиом и правил вывода, называется противоречивым, если в этом исчислении можно вывести любую формулу. Иначе в противоречивом исчислении все формулы являются теоремами. Формальное исчисление называется непротиворечивым, если оно не является противоречивым [10].

Определение полноты множества формул: множество формул Т называется полным, если для каждой постоянной формулы либо она сама, либо ее отрицание является следствием из Т [10].

Секвенция называется тождественно истинной, если она истинна в любой алгебраической системе при любой интерпретации.

Обоснованием непротиворечивости исчисления предикатов являются следующие и теоремы.

Первая теорема Геделя о полноте исчисления предикатов (1930). В исчислении предикатов первого порядка все теоремы являются логически общезначимыми формулами, т.е. являются истинными во всех интерпретациях [2].

Иначе: если формула А есть логический закон, то А выводится в исчислении предикатов.

Теорема о неполноте Геделя-Росса. Если множество формул Г содержит аксиомы математической логики и является непротиворечивым, то существует формула А, не содержащая свободных переменных, такая, что оба выражения Г├А и Г├ ØА не выводимы [2].

Пример в рамках любой модели невозможно вывести ни одну из двух формул: «Бог есть», «Бога нет».

Теорема о неполноте не только означает возможность ситуаций, когда нет смысла определять, является ли формула тавтологией или противоречием на основании вывода с использованием правил вывода исчисления предикатов. Пусть в программе вывода доказывается формула А такая, что Г├А и Г├ØА не выводимы, тогда в программе вывода этой формулы никогда не реализуется критерий останова.

В логике высказываний доказуемость или недоказуемость можно определить за конечное число шагов. Но в языке логики предикатов такой подход не годится. Однако это не является существенным недостатком с точки зрения представления знаний и получения выводов.