Предикатов. Свойства теорий первого порядка.

 

Для записи формул логики предикатов используется следующий алфавит: скобки, запятые, символы исчисления высказываний (отрицание , импликация ), предметные (индивидные) переменные , предметные (индивидные) константы , предикатные буквы и функциональные буквы . Верхний индекс предикатной или функциональной буквы указывает на число аргументов, а нижний – служит для различия букв с одним и тем же числом аргументов.

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

1) всякая элементарная формула – есть формула.

2) если и - формулы и - предметная переменная, то каждое из следующих выражений есть формула: , и .

3) выражение является формулой тогда и только тогда, когда это следует из правил 1) и 2).

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

Определение 2: Под интерпретацией формулы будем понимать систему, состоящую из непустого множества (область интерпретации) и соответствия, относящего каждой предикатной букве некоторое - местное отношение во множестве ; каждой функциональной букве - некоторую - арную операцию во множестве ; каждой предметной постоянной - некоторый элемент из множества .

Всякая формула, не содержащая свободных переменных в любой интерпретации, является высказыванием. Если же формула содержит свободные переменные, то в любой интерпретации она является предикатом, т. к. она может быть истинной для одних значений переменных и ложной – для других.

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

Определение 4: Формула называется выполнимой, если существует интерпретация, в которой выполнима хотя бы для одного набора значений переменных.

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

Как известно, во всякой интерпретации всякая замкнутая формула (т.е. высказывание) или истинна или ложна, т.е. выполнима либо на каждом наборе переменных, либо ни на одном. Следовательно, всякая замкнутая формула выполнима тогда и только тогда, когда она истинна в какой-нибудь интерпретации.

Определение 5: Будем называть формулу противоречием (в исчислении предикатов), если формула является логически общезначимой (тавтологией) или, что то же самое, если формула ложна во всякой интерпретации.

Определение 6: Говорят, что формула логически влечет формулу , если в любой интерпретации формула выполнима на любом наборе, на котором выполнена формула .

Определение 7: Формулу называют логическим следствием формул из множества , если во всякой интерпретации формула выполнена, если выполнены все формулы из множества .

Определение 8: Две формулы называют логически эквивалентными, если каждая из них логически влечет другую формулу.

Из приведенных выше определений вытекают следующие утверждения:

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

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

в) Если формула логически влечет формулу и истинна данной интерпретации, то в этой же интерпретации истинна и .

В случае исчисления высказываний метод истинностных таблиц дает эффективный способ проверки, является ли произвольная формула тавтологией. Доказано, что для исчисления предикатов не существует эффективного способа проверки того, что произвольная формула является логически общезначимой.

Таким образом, аксиоматический метод, который был «излишней роскошью» при изучении исчисления высказываний, представляется необходимым при изучении формул, содержащих кванторы.

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

Доказано, что теорий первого порядка хватает для описания известных математических теорий. И, во всяком случае, большинство теорий высших порядков может быть «переведено» язык теорий первого порядка.

Обозначим теорию первого порядка буквой .

Определение 10: Символами всякой теории первого порядка служат те же символы, которые мы ввели для исчисления высказываний:

1) логические связки (отрицание и импликация);

2) знаки пунктуации;

3) счетное множество предметных переменных ;

4) непустое множество (конечное или счетное) предикатных букв ;

5) конечное (возможно и пустое) или счетное множество функциональных букв ;

6) конечное (тоже, возможно, пустое) или счетное множество предметных констант .

Таким образом, в различных теориях могут отсутствовать некоторые или даже все функциональные буквы и предметные константы, а также некоторые (но не все) предикатные буквы.

Различные теории могут отличаться друг от друга составом символов. Определения терма, формулы, логических связок остаются в силе для любой теории первого порядка. Разумеется, в каждой конкретной теории при построении термов и формул участвуют только те символы, которые принадлежат данной теории.

Аксиомы теории разбиваются на два класса: логические аксиомы и собственные (или нелогические) аксиомы.

Логические аксиомы: Каковы бы ни были формулы теории , следующие формулы являются логическими аксиомами:

(А1) ;

(А2) ;

(А3) ;

(А4) ,

где - формула теории и – терм этой теории, свободный для переменной в формуле . В частности, терм может совпадать с , тогда получаем аксиому .

(А5) ,

если формула не содержит свободного вхождения переменной .

Собственные аксиомы не могут быть сформулированы в общем случае, т.к. они различные для различных теорий. Например: теория частично упорядоченных множеств (в частности структур); теория натуральных чисел; теория групп в алгебре и т. д. В частности, теория первого порядка, не содержащая собственных аксиом, называется исчислением предикатов первого порядка.

Правилами вывода для всякой теории первого порядка являются:

а) Modus ponens: из и следует (сокращённо: ).

б) Правило обобщения (или связывания квантором всеобщности): из следует . Иногда это правило сокращённо обозначают (от английского слова «generalization».

Определение 11:Моделью теории первого порядка называется всякая интерпретация, в которой истинны все аксиомы теории .

Нетрудно доказать, что если правило modus ponens и правило обобщения применяются к истинным в данной интерпретации формулам, то результатом являются формулы, истинные в той же интерпретации. Следовательно, и всякая теория истинна во всякой её модели.

Далее будет показано, что логические аксиомы выбраны так, чтобы множество всех их логических следствий из аксиом теории в точности совпадало с множеством теорем теории . В частности, для исчисления предикатов первого порядка оказывается, что множество его теорем совпадает с множеством логически общезначимых формул.

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

Это следует из возможности интерпретации такой теории в области, состоящей из одного элемента. Все теоремы теории истинны в такой интерпретации, однако, ни в какой интерпретации никакая формула не может быть истинной вместе со своим отрицанием.

Непротиворечивость произвольной теории первого порядка можно доказать, если эта теория допускает конечную интерпретацию (например, теория частичного порядка или теория групп). Если теория первого порядка не допускает никакой конечной интерпретации, то доказать непротиворечивость такой теории логическими средствами невозможно. Например, теория натуральных чисел не допускает конечной интерпретации, поэтому нельзя доказать ее непротиворечивость.

Теорема 2: Во всяком исчислении предикатов первого порядка всякая теорема является логически общезначимой.

Определение 12: Теория первого порядка называется полной, если для любой замкнутой формулы из этой теории либо выводимой является формула , либо .

Теорема 3: Всякая непротиворечивая теория первого порядка имеет счётную модель (т. е. модель со счётной областью интерпретации).

Следствие 1: Всякая логически общезначимая формула теории первого порядка является теоремой теории .

Следствие 2: (теорема Геделя (1930) о полноте).

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