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

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

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

Теорема 1: Если формула некоторой теории является частным случаем тавтологии, то формула - есть теорема в теории и может быть выведена с помощью только схем аксиом (А1) - (А3) и правила modus ponens.

Доказательство: Пусть формула получена из некоторой тавтологии с помощью подстановок. Тогда существует вывод формулы в теории (т. к. всякая тавтология в теории является теоремой). Сделаем теперь всюду в этом выводе подстановки по следующему правилу:

1) если какая-нибудь пропозиционная буква входит в , то на месте всех её вхождений в каждую формулу вывода подставляем ту формулу теории , которая подставлялась в тавтологию на места вхождений той же буквы при построении формулы ;

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

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

Если теория первого порядка не содержит собственных аксиом, то она называется исчислением предикатов первого порядка.

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

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

Например, есть .

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

Очевидно, что и . Для всякой аксиомы , полученной по схеме аксиом (1)-(5), выражение является тавтологией. Это очевидно для схем аксиом (А1) - (А3). Всякий частный случай схемы (4) преобразуется операцией в тавтологию вида , а всякий частный случай схемы (А5) преобразуется в тавтологию вида .

Наконец, если и тавтологии, то и - есть тавтология, т. к. результаты применения операции к формуле и совпадают. Следовательно, если есть теорема в теории , то есть тавтология.

Если бы существовала формула в теории , такая, что ├_К и ├_К (здесь знаком ├_К обозначается вывод в теории ), то оба выражения и были бы тавтологиями, что невозможно. Таким образом, теория непротиворечива. Что и требовалось доказать.

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

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

Например, ├_К для любой формулы , но далеко не всегда справедлив вывод ├_К . В самом деле, рассмотрим область, содержащую по крайней мере два элемента и . Пусть - есть некоторое исчисление предикатов. Пусть есть . Проинтерпретируем каким-нибудь свойством, которым обладает только элемент . Тогда выполнено для значения , но не выполняется. Следовательно, формула не является истинной в этой интерпретации, и поэтому не является логически общезначимой. Далее будет доказано, что всякая теорема всякого исчисления предикатов является логически общезначимой.

Однако, некоторая «ослабленная», но полезная форма теоремы дедукции и здесь может быть доказана.

Пусть - некоторая формула, принадлежащая заданному множеству формул , и пусть - какой-нибудь вывод из , снабженный обоснованием каждого шага. Мы будем говорить, что формула зависит от в этом выводе, если:

1) есть и обоснованием есть принадлежность к множеству , или

2) обосновано, как непосредственное следствие по правилу modus ponens или по правилу обобщения () некоторых предшествующих в этом выводе формул, из которых, по крайней мере, одна зависит от формулы .

Например, ├ .

(В₁) - гипотеза.

(В₂) - выводится из (В₁) по правилу .

(В₃) - гипотеза.

(В₄) - выводится из (В₂), (В₃) по правилу .

(В₅) - получается из (В₄) по правилу .

Здесь (В₁) зависит от , (В₂) зависит от , (В₃) зависит от , (В₄) зависит от и от , (В₅) зависит от и от .

Теорема 3: Если не зависит от в выводе ├ , то ├ .

Доказательство: Пусть вывод из и , в котором не зависит от . Докажем теорему индукцией по числу . При утверждение теоремы очевидно. Предположим, что утверждение теоремы справедливо для таких выводов, длина которых меньше (индуктивное допущение). Если принадлежит множеству или является аксиомой, то ├ . Если является непосредственным следствием некоторых (одной или двух) предшествующих формул, то, поскольку не зависит от , то от не зависит ни одна из данных формул. Следовательно, по индуктивному допущению, из выводимы эти (одна или две) формулы, а вместе с ними и . Что и требовалось доказать.

Теорема 4: (теорема дедукции в теории ).

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

Доказательство: Пусть - удовлетворяющий условиям теоремы вывод из . Докажем, что ├ для любого индукцией.

Если принадлежит множеству или является аксиомой, то ├ , т. к. - аксиома. Если совпадает с , то ├ , т. к. ├ теорема 1. Если существуют и , меньшие , такие что есть , то ├ и ├ (по индуктивному предположению). Следовательно, по схеме аксиом (А2) и правилу имеем: ├ .

Предположим, наконец, что существует такое, что есть . По предположению: ├ . Здесь либо не зависит от , либо переменная не является свободной в формуле . Если не зависит от , то в силу теоремы 3 имеем: ├ . Тогда, применяя правило , получаем: ├ , т. е. ├ . По схеме аксиом (А1): ├ . Отсюда по правилу получаем: ├ . Если же не является свободной в формуле , то по схеме аксиом (А5) имеем: ├ . Так как ├ , тогда по правилу , получаем: ├ . И, наконец, по правилу имеем: ├ , т. е. ├ . На этом завершается индукция. Получаем требуемое предложение при условии .

Условия теоремы 4 громоздки, поэтому иногда удобнее использовать более «слабые» следствия из последней теоремы.

Следствие 1: Если ├ и существует вывод, построенный без применения правила обобщения к свободным переменным формулы , то ├ .

Следствие 2: Если формула замкнута и ├ , то ├ .

Замечание: Из доказательств теорем 3 и 4, следствий из теоремы 4 вытекает, что при построении нового вывода ├ (в случае теоремы 3: ├ ) применение правила к любой формуле, зависящей от некоторой формулы из множества , требуется только в том случае, когда и в данном выводе, т. е. в выводе из , имеется применение правила (с той же связываемой переменной) к некоторой формуле, зависящей от .

Видно, что в доказательстве теоремы 4 зависит от той или иной посылки из множества в первоначальном выводе тогда и только тогда, когда зависит от в новом выводе.

Это замечание может быть полезным, когда нужно применить теорему дедукции несколько раз подряд в процессе доказательства какого-либо утверждения о выводимости. Например, чтобы получить ├ из ├ . Поэтому в дальнейшем можно пользоваться этим замечанием наряду с теоремами 3 и 4 и следствиями 1 и 2.

Например, ├ .

Доказательство:

1) - гипотеза;

2) - схема аксиом (А4);

3) - выводимо из пунктов 1 и 2 по правилу ;

4) - схема аксиом (А4);

5) - выводимо из пунктов 3 и 4 по правилу ;

6) - выводимо из пункта 5 по правилу ;

7) - получается из пункта 6 по правилу .

Таким образом, мы имеем: ├ . Причём в построенном выводе, ни при каком применении правила не связывается переменная формулы . Поэтому, на основании следствия 2: ├ .