Главная Случайная страница Контакты | Мы поможем в написании вашей работы! | ||
|
Все результаты этого параграфа относятся к произвольной теории первого порядка. Всякая теория первого порядка является формальной теорией.
Определение 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; Прочитано: 731 | Нарушение авторского права страницы | Мы поможем в написании вашей работы!