![]() |
Главная Случайная страница Контакты | Мы поможем в написании вашей работы! | |
|
Все результаты этого параграфа относятся к произвольной теории первого порядка. Всякая теория первого порядка является формальной теорией.
Определение 1: Формула называется частным случаем формулы
, если формула
получается из формулы
с помощью подстановки некоторой формулы
вместо всех вхождений некоторой пропозиционной буквы.
Теорема 1: Если формула некоторой теории
является частным случаем тавтологии, то формула
- есть теорема в теории
и может быть выведена с помощью только схем аксиом (А1) - (А3) и правила modus ponens.
Доказательство: Пусть формула получена из некоторой тавтологии
с помощью подстановок. Тогда существует вывод формулы
в теории
(т. к. всякая тавтология в теории
является теоремой). Сделаем теперь всюду в этом выводе подстановки по следующему правилу:
1) если какая-нибудь пропозиционная буква входит в , то на месте всех её вхождений в каждую формулу вывода подставляем ту формулу теории
, которая подставлялась в тавтологию
на места вхождений той же буквы при построении формулы
;
2) если данная пропозиционная переменная не входит в формулу , то на места всех её вхождений в формулы вывода подставляем произвольную (одну и ту же для данной буквы) формулу теории
.
Полученная таким образом последовательность формул будет выводом формулы в теории
. Теорема доказана.
Если теория первого порядка не содержит собственных аксиом, то она называется исчислением предикатов первого порядка.
Теорема 2: Всякое исчисление предикатов первого порядка непротиворечиво.
Доказательство: Для произвольной формулы обозначим через
выражение, которое получается в результате следующего преобразования формулы
: в этой формуле опускаются все кванторы и термы (вместе с соответствующими скобками и запятыми).
Например, есть
.
По существу, всегда является формулой алгебры высказываний, в которой роль пропозиционных букв играют предикатные буквы
.
Очевидно, что и
. Для всякой аксиомы
, полученной по схеме аксиом (1)-(5), выражение
является тавтологией. Это очевидно для схем аксиом (А1) - (А3). Всякий частный случай
схемы (4) преобразуется операцией
в тавтологию вида
, а всякий частный случай
схемы (А5) преобразуется в тавтологию вида
.
Наконец, если и
тавтологии, то и
- есть тавтология, т. к. результаты применения операции
к формуле
и
совпадают. Следовательно, если
есть теорема в теории
, то
есть тавтология.
Если бы существовала формула в теории
, такая, что ├К
и ├К
(здесь знаком ├К обозначается вывод в теории
), то оба выражения
и
были бы тавтологиями, что невозможно. Таким образом, теория
непротиворечива. Что и требовалось доказать.
Замечание: Операция равносильна интерпретации
в области, состоящей из одного элемента. Все теоремы теории
истинны в такой интерпретации, однако ни в какой интерпретации никакая формула не может быть истинной вместе со своим отрицанием.
Теорема дедукции для исчисления высказываний без соответствующей модификации не может быть проведена для произвольных теорий первого порядка.
Например, ├К
для любой формулы
, но далеко не всегда справедлив вывод ├К
. В самом деле, рассмотрим область, содержащую по крайней мере два элемента
и
. Пусть
- есть некоторое исчисление предикатов. Пусть
есть
. Проинтерпретируем
каким-нибудь свойством, которым обладает только элемент
. Тогда
выполнено для значения
, но
не выполняется. Следовательно, формула
не является истинной в этой интерпретации, и поэтому не является логически общезначимой. Далее будет доказано, что всякая теорема всякого исчисления предикатов является логически общезначимой.
Однако, некоторая «ослабленная», но полезная форма теоремы дедукции и здесь может быть доказана.
Пусть - некоторая формула, принадлежащая заданному множеству формул
, и пусть
- какой-нибудь вывод из
, снабженный обоснованием каждого шага. Мы будем говорить, что формула
зависит от
в этом выводе, если:
1) есть
и обоснованием
есть принадлежность
к множеству
, или
2) обосновано, как непосредственное следствие по правилу modus ponens или по правилу обобщения (
) некоторых предшествующих в этом выводе формул, из которых, по крайней мере, одна зависит от формулы
.
Например, ├
.
(В1) - гипотеза.
(В2) - выводится из (В1) по правилу
.
(В3) - гипотеза.
(В4) - выводится из (В2), (В3) по правилу
.
(В5) - получается из (В4) по правилу
.
Здесь (В1) зависит от , (В2) зависит от
, (В3) зависит от
, (В4) зависит от
и от
, (В5) зависит от
и от
.
Теорема 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: ├
.
Дата публикования: 2014-11-03; Прочитано: 755 | Нарушение авторского права страницы | Мы поможем в написании вашей работы!