Чистое исчисление предикатов. 2.1. Свойства чистого исчисления предикатов

Лекция 2

2.1. Свойства чистого исчисления предикатов.

На самом деле все наши дальнейшие результаты будут верны для любой теории первого порядка, а не только для исчисления К.

Утверждение 2.1.1. Если фл А теории К есть частный случай тавтологии, то фл А есть теорема теории К и может быть выведена только с употреблением схем А1 – А3 и правила МР.

Доказательство. Возьмём вывод тавтологии А в L и сделаем в нём всюду такие изменения: (i) если пп входит в вывод, то на места всех её вхождений во все фл вывода подставляем ту фл теории К, которая подставлялась вместо этой пп при получении фл А; (ii) если данная пп не входит в вывод, то на места всех её вхождений во все фл вывода подставляем одну и ту же фл теории К (произвольную). Полученная новая последовательность фл и будет выводом нашей фл А в К, при этом использовались только отмеченные в Утверждении 2.1.1 схемы и правила вывода.

Упражнение. Возьмите какой-либо из выводов, полученных ранее для теории L, и преобразуйте сначала полученную тавтологию, а затем её вывод так, как указано выше!

Утверждение 2.1.2. Чистое исчисление предикатов непротиворечиво.

Доказательство. Для фл А через П(А) обозначим фл, которая получится из А опусканием всех кванторов и стоящих за ними пп. Полученное выражение является пф (вместо пп в них будут стоять прб). Наша операция П проносится через пс (проверьте это!). Если фл А есть пример схем аксиом А1 – А5, то П(А) – тавтология (проверьте это для схем А4 и А5). Проверьте также, что правила МР и Gen преобразуют тавтологии в тавтологии. Если бы теперь в К выводились фл В и ØВ, то оба выражения П(В) и П(ØВ) были бы тавтологиями, однако последнее невозможно (почему?). Итак, теория К – непротиворечива.

Замечание. Чуть ниже мы приведём другое доказательство непротиворечивости К, использующее теорему о полноте для чистого исчисления предикатов К.

Теорема о дедукции прямо на исчисление предикатов К не переносится. Например, пусть А „ "xА(x), однако не всегда „ А ®"xA(x). Вот пример. Рассмотрим область из двух элементов а и в. Пусть фл А интерпретируется свойством, которым обладает только элемент а. Тогда фл А выполнена при любой оценке, отображающей пп x в а, а фл "xA(x) не выполнена ни при какой оценке, т.е. фл А ®"xA(x) не есть озф. Но в теореме о полноте мы докажем, что всякая теорема теории К является озф.

Но все же некоторая ослабленная форма теоремы о дедукции остаётся верной и для исчисления К. Рассмотрим конечное множество фл Г, фл АÎГ и вывод В₁,…,В_n из Г, снабженный обоснованием каждого шага.

Определение. Скажем, что В_i в этом выводе зависит от А, если В_i есть А и обоснованием В_i служит принадлежность В_i к Г или В_i обосновано как следствие по МР или Gen некоторых предшествующих фл, хотя бы одна из которых зависит от А. Приведём пример. Докажем, что А, "xА(x)®С „ "xС.

1. А гипотеза

2. "xА(x) из 1. по Gen

3. "xА(x)®С гипотеза

4. С из 2. и 3. По МР

5. "xС из 4 по Gen.

В приведенном выводе шаг 1 зависит от А, шаг 2 зависит от А, шаг 3 зависит от "xА(x)®С, шаг 4 зависит от А и от "xА(x)®С и шаг 5 зависит от А и от "xА(x)®С.

Утверждение 2.1.3. Если фл В не зависит от фл А в выводе Г, А „ В, то Г „ В.

Доказательство. Пусть В₁,…,В_n=В – вывод В из {Г, А} и пусть В не зависит от А. Проведём индукцию по длине вывода. Итак, пусть наше Утверждение 2.1.3 верно для всякого вывода, длина которого меньше n. Если В принадлежит Г или есть аксиома, то наше утверждение верно. Если В есть непосредственное следствие каких-либо фл (одной или двух в зависимости от правила вывода), то, т.к. В не зависит от А, то от А не зависит ни одна из этих фл и по предположению индукции из Г выводятся эти фл а, следовательно, и фл В.

Утверждение 2.1.4. Теорема о дедукции для исчисления К.

Пусть Г, А „ В и пусть при этом существует такой вывод, в котором ни при каком применении правила Gen к фл, зависящим в этом выводе от А, не связывается квантором никакая свободная переменная фл А. Тогда Г „ А®В.

Прежде чем доказывать Утверждение 2.1.4, дадим его более слабые, но полезные в применении следствия.

Следствие 2.1.5. Если Г, А „ В и вывод свободен от применения правила Gen к свободным переменным из фл А, то Г „ А® В.

Следствие 2.1.6. Если фл А замкнута и Г, А „ В, то Г „ А® В.

Докажем теперь Утверждение 2.1.4. Используем индукцию по построению вывода. Пусть В₁,…,В_n=В есть вывод В из {Г,А}, удовлетворяющий условиям Утверждения 2.1.4. Докажем теперь для всякого i £ n наше Утверждение 2.1.4. Если В_i есть аксиома или B_i принадлежит Г, то Г „А®В_i, т.к. B_i®(A®B_i) есть аксиома. Если В_i=А, то Утверждение 2.1.4 верно в силу выводимости А®А. Если есть j и k меньшие i такие, что В_к есть В_j®B_i, то в силу индукционного предположения, имеем Г„А®В_j и Г„А®(В_j®B_i). Используя схему аксиом А2 и правило МР, получим Г„А®В_i. Наконец, пусть найдётся j< i такое, что В_i="x_кB_j. По предположению, Г „А®В_j и В_j либо не зависит от А, либо переменная x_k не свободна в фл А. Если первое, то в силу Утверждения 2.1.3 имеем Г „В_j и, по правилу Gen, Г„"x_кB_j, т.е. Г„В_i. Используя схему аксиом А1 и МР, имеем Г„А®В_i. Если же x_к не свободная переменная фл А, то по схеме А5 „"x_k(A®В_j)®(A®"x_kB_j). Т.к. Г„А®В_j, то по правилу Gen получаем Г„"x_k(А®В_j) и, по МР, Г„A®"x_kB_j, т.е. Г „А®В_i. Это и завершает наше доказательство. Т.к. i £ n, то имеем требуемое.

Приведём полезный пример. Докажем, что „"x"yА®"y"xA.

1. "x"yА гипотеза.

2. "x"yА®"yA схема А4

3. "yA из 1 и 2 по МР

4. "yА®A схема А4

5. А из 3 и 4 по МР

6. "xA из 5 по Gen

7. "y"xA из 6 по Gen

В силу 1 – 7 получаем, что "x"yА„"y"xA и что в нашем выводе ни при одном применении правила Gen не связывается никакая свободная переменная фл "y"xA. Поэтому, на основании Следствия 2.1.5, получаем требуемый результат.

Задача. Докажите выводимость в К таких фл:

а) „"x(A®B)®("xA®"xB); в) „"x(A®B)® ($xA®$xB);

c) „"x(AÙB) º ("xA Ù "xB).

Указание. Используйте теорему о дедукции для исчисления К₄.

2.2 Теорема Гёделя о полноте. Приведение формул логики предикатов к предваренному виду

Утверждение 2.2.1. Теорема о полноте для исчисления К.

Дата добавления: 2014-01-06