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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

[1] free (x, t, j) означает, что терм t свободен для переменной х в формуле j.

Дата добавления: 2014-11-08; просмотров: 546; Нарушение авторских прав

Мы поможем в написании ваших работ!