6. Исчисление предикатов

Рассмотрим построение теории первого порядка.

Компонентами теории первого порядка являются следующие.

1. Алфавит составляют:

· Предметные константы – буквы начала латинского алфавита с натуральными индексами: , , …, , , … Предметные символы – это имена (обозначения) предметов.

· Предметные переменные – буквы конца латинского алфавита с натуральными индексами: , , …, , , …

· Функциональные буквы – строчные буквы латинского алфавита с натуральными индексами (верхний индекс указывает число переменных, нижний – номер функциональной буквы): , , …

· Предикатные буквы – заглавные буквы латинского алфавита с натуральными индексами (верхний индекс указывает число переменных, нижний – номер предикатной буквы): , , ,... (индексы можно не указывать).

· Логические связки: .

· Квантор всеобщности .

· Синтаксические символы – скобки (, ) и запятая.

2. Формула определяется несколькими этапами. Вначале вводится понятие терма.

Определение. 1) Предметные константы и предметные переменные есть Термы.

2) Если , , …, , – термы, – функциональная буква, то – терм.

3) Символ является термом тогда и только тогда, когда это следует из 1) и 2).

Примеры. 1. Пусть – предметная переменная, – предметная константа, , – функциональные буквы. Тогда , – термы.

2. Пусть – предметная переменная, – предметная константа, , – функциональные буквы. Тогда , – термы. Здесь символы , имеют только формальный смысл и не интерпретируются как обозначения тригонометрических функций.

Определение. Если , , …, , – термы, – предикатная буква, то символ называется элементарной формулой.

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

Примеры. 1. В условиях первого примера, если – предикатная буква, то – элементарная формула.

2. В условиях второго примера, если – предикатная буква, то – элементарная формула.

Теперь определим формулу логики предикатов.

Определение. 1) Всякая элементарная формула есть формула.

2) Если , – формулы, то формулами являются также символы , , .

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

Примеры. 1. В условиях первого примера, – формула.

2. В условиях второго примера, – формула.

В теории первого порядка, как и в исчислении высказываний, допускаются формулы с другими логическими связками, а также допускается использование квантора существования. Известна формула (см. Глава 5. Предикаты.).

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

Определение. Пусть – формула, – переменная, которая входит в формулу (один или несколько раз). Вхождение в формулу называется Связанным, если либо – переменная в кванторе (), либо находится в области действия квантора . Если вхождение в не связано, то оно называется свободным.

Пример. В формуле вхождения обеих переменных свободные.

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

В формуле вхождения обеих переменных связаны.

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

Пример. Рассмотрим подстановку вместо всех свободных вхождений в формулы из предыдущего примера.

В формуле вхождение свободное, следовательно, получаем .

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

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

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

Пример. Рассмотрим формулу и терм . не свободен для переменной в данной формуле, так как лежит в области действия квантора, тем более не свободен для переменной .

Пусть теперь дан терм . свободен для переменной .

Уточним понятие интерпретации для множества формул теории первого порядка.

Определение. Интерпретацией множества формул называется область интерпретации и заданное на ней соответствие, которое каждой предикатной букве ставит в соответствие -местный предикат на , каждой функциональной букве – -местную функцию на , каждой предметной константе – элемент множества .

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

Пример. На множестве рассмотрим формулу . Интерпретируем эту формулу следующим образом: . Тогда мы получим предикат .

Рассмотрим теперь формулу . При интерпретации она превращается в истинное высказывание .

Определение. Интерпретация называется Моделью формальной теории (или некоторого множества формул), если все формулы формальной теории (или множества формул) истинны в данной интерпретации.

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

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

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

Теорема. Отношение логической эквивалентности является отношением эквивалентности.

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

Теорема. Отношение логического следствия является отношением предпорядка.

Определение. Формула называется Противоречивой, если она ложна в любой интерпретации.

Теорема. Пусть – формула, – переменная в формуле , терм свободен для переменной в формуле . Тогда формула общезначима.

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

.

Покажем, что это высказывание истинно. Возможны два случая.

1. , следовательно .

2. .

Соотношение выполнено при любых значениях . Подставим этот набор значений в терм : . Подставим последнее выражение в предикат . Получим:

.

Но, поскольку терм свободен для переменной в формуле , получаем:

Следовательно, по свойству импликации получаем, что , что и требовалось доказать.

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

Доказательство аналогично доказательству предыдущей теоремы.

Теперь мы можем вернуться к построению теории первого порядка.

3. Аксиомы теории первого порядка делятся на два класса:

· Логические аксиомы:

1) .

2) .

3) .

4) , где терм свободен для переменной в формуле .

5) , где – несвободная переменная в формуле .

Отметим, что аксиомы 1) – 3) – тавтологии, 4) и 5) – общезначимые формулы.

· Собственные аксиомы.

У каждой теории первого порядка свои собственные аксиомы.

4. Правила вывода.

1) Modus ponens (МР).

├.

2) Правило обобщения Gen.

├.

Определение. Теория первого порядка без собственных аксиом называется исчислением предикатов первого порядка (или чистым исчислением предикатов).

Без доказательства приведем теоремы.

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

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

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

< Предыдущая		Следующая >