4 - Исчисление предикатов. Построение теории P. Правила естественного вывода. Глобальные свойства теории P (Конспект лекций), страница 2

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

В результате язык модифицируется так, что в нем не будет функциональныхсимволов. Наличие сортов переменных ограничивает их использование при формировании элементарных формул. Снятие ограничений приводит к тому, что, например, вместе с p(x, y)появляется формула p(y, x), т.е.

происходит расширение множества элементарных формул. Допуская такое расширение, приходим к односортному языку, в котором термы — это переменныеодного сорта.Далее мы покажем, что множество выводимых формул совпадает с множеством логическихзаконов в данном языке. Начнем с важного свойства, присущего выводу из гипотез. Оказывается, что вывод из гипотез сохраняет истинность формул при фиксированной модели ификсированной оценке.ÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓО множестве формул, выводимых в исчислении предикатов.

Лемма об истинности при фиксированной оценке. Следствия: о том, что любая выводимая формула общезначима; о непротиворечивости исчисления предикатов. Понятие формальной аксиоматической теории.Непротиворечивость, полнота формальной аксиоматической теории.ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-124.3. Глобальные свойства теории PПоследняя секвенция вытекает из правила p2.ÔÍ-12Пример 4.2.

Используя правила естественного вывода, докажем выводимость в теории Pформулы ∃x X → ¬∀x¬X, т.е. построим вывод секвенции ` ∃x X → ¬∀x¬X. Имеем цепочкупреобразований снизу вверх“:”` ∃x X → ¬∀x¬X ⇐ ∃x X ` ¬∀x¬X ⇐ X ` ¬∀x¬X ⇐ ∀x¬X ` ¬X ⇐ ∀x¬X ` ∀x¬X.ÌÃÒÓИспользование правил естественного вывода такое же, как и в случае исчисления высказываний.ÌÃÒÓÌÃÒÓ` ∃yXyx → ∃xXÌÃÒÓСледствие 4.1. Если Γ ` X и все формулы в Γ являются логическими законами, то и Xесть логический закон. В частности, если ` X, то X — логический закон.J Как и в случае исчисления высказываний, последнее следствие показывает, что исчислениепредикатов является непротиворечивым. Действительно, если ` X, то по следствию 4.1 формула X общезначима. Предположение ` ¬X приводит к выводу, что и ¬X общезначима.

Но нетни одной формулы, которая общезначима вместе со своим отрицанием. Это непосредственновытекает из определения: если X общезначима, то, выбрав произвольную модель M , а в нейоценку θ, получим истинную формулу Xθ. Но тогда (¬X)θ ≡ ¬Xθ ложна, а формула ¬X неявляется тождественно истинной в M , т.е. ¬X не является общезначимой. IÌÃÒÓÔÍ-12Далее мы докажем, что любая общезначимая формула выводима в исчислении предикатов.Однако воспроизвести доказательство из исчисления высказываний не удастся. Появились новые понятия интерпретации и модели, и нам необходимо понятие, напоминающее вывод изгипотез, но связанное с понятием интерпретации.Уточним смысл термина аксиоматической формальной теории, понимая под этим пару T =(Ω, A) из некоторого логико-математического языка Ω, снбженного набором 15 схем аксиоми 2 правил вывода исчисления предикатов, и некоторого множества A замкнутых формул вязыке Ω.

Формулы из множества A будем называть нелогическими аксиомами теории.Выводом в теории T = (Ω, A) будем называть вывод в исчислении предикатов из гипотез Γ,где Γ ⊂ A — конечный список нелогических аксиом. Таким образом, нелогические аксиомыиспользуются в дополнение к стандартному набору логических аксиом (т.е. аксиом исчисленияпредикатов). Конечная формула X всякого вывода теории называется выводимой в ней, иэтот факт мы будем обозначать T ` X.

Выводимые формулы еще называют теоремамиÔÍ-12Следствие 4.2. Теория P непротиворечива.ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓJ Доказательство проводится индукцией по длине вывода. Утверждение очевидно, если выводсодержит одну формулу, которая в этом случае есть либо аксиома (являющаяся логическимзаконом), либо гипотеза Xj . Но тогда Y θ и Xj θ — одно и то же.Предположим утверждение доказано для всех выводов длины менее k. Рассмотрим произвольный вывод Z1 , Z2 , .

. . , Zk из гипотез Γ длины k с конечной формулой Y = Zk . ФормулаY есть либо логический закон, либо гипотеза, либо получена по правилу заключения, либо поправилу всеобщности. В первых двух случаях рассуждения те же, что и при k = 1. В третьемслучае в выводе есть формулы Zj и Zl = Zj → Y . Если в какой-либо модели M при оценке θистинны формулы X1 θ, Xm θ, то в силу предположения индукции формулы Zj θ и (Zj → Y )θ истинны в M .

В этом случае правило заключения гарантирует истинность в M формулы Y θ, т.е.утверждение теоремы доказано в случае, когда формула Y получена по правилу заключения.Пусть Y получена по правилу обобщения, т.е. Y = ∀xZj для некоторой формулы Zj , j < k.Предположим, что в выводе формулы Zj использованы все гипотезы X1 , . .

. , Xm (неиспользуемые можно просто не рассматривать). В силу структурного требования каждая из этихформул не имеет свободных вхождений переменной x. Обозначив через x1 = x, x2 , . . . , xrвсе переменные, имеющие вхождения в вывод формулы Zj , рассмотрим любую совокупностьоценок θa , отличающихся только значением a, котороеставится в соответствие переменнойx.

Такие оценки можно записать в виде θa = xa θ , где θ — общая часть всех этих оценок,относящаяся к переменным x2 , . . . , xr . Применение любой из оценок θa к формулам X1 , . . . ,Xm дает один и тот же результат X1 θ, . . . , Xm θ, поскольку переменная x в эти формулы невходит. Пусть все формулы X1 θ, . . . , Xm θ в выбранной модели M истинны. Тогда для любогозначения a истинны формулы X1 θa , .

. . , Xm θa . Согласно индуктивному предположению длялюбого значения a истинна формула Zj θa . Следовательно, для данной оценки θ в соответствиис интерпретацией квантора всеобщности истинна формула (∀xZj )θ или, что то же самое Y θ.Тем самым утверждение теоремы доказано для формулы Y в случае, когда она получена поправилу обобщения. IÌÃÒÓÔÍ-12ÌÃÒÓ46ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-124. ИСЧИСЛЕНИЕ ПРЕДИКАТОВÌÃÒÓX = ∀x2 ∀x3 .

. . ∀xn (∃x1 p(x1 , x2 , . . . , xn ) → ∀x1 p(x1 , x2 , . . . , xn )).Γ, ¬X ` X ∨ YΓ, ¬X, X ` YΓ, ¬X, Y ` YΓ`X ∨YТеорема 4.2. Любая непротиворечивая формальная аксиоматическая теория имеет счетнуюмодель.ÔÍ-12J Для построения соответствующей интерпретации нужно выбрать произвольное счетное множество (неважно какое), конкретизировать функциональные символы и константы (опять-такиневажно как), и придать смысл предикатным символам.

Последнее является ключевым: необходимо так конкретизировать предикатные символы, что все нелогические аксиомы станутистинными. Ясно, что сосредоточиться надо на символах, входящих в нелогические аксиомы.Разобраться можно, проведя синтаксический анализ нелогических аксиом. Сделать это можнотак.В логико-математический язык Ω формальной теории введем дополнительное счетное множество констант, получив расширенный язык Ψ. Очевидно, что рассматриваемая формальнаятеория T будет формальной теорией и с языком Ψ, причем непротиворечивой (обозначим ее Tψ ).В этом языке рассмотрим множество D всех замкнутых термов (чтобы такие существовали внужном количестве, и нужно расширение языка). Это будет носителем нашей интерпретации.ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12Γ, ¬X, X ∨ Y ` YÌÃÒÓÌÃÒÓЭто правило обратимо, т.е..

Действительно, воспользовавшись правилом сечения, поΓ, ¬X ` Yлучаем:Γ, ¬X ` YÔÍ-12Γ`X ∨YΓ, ¬X ` Y(см. пример 2.3).Γ`X ∨YÌÃÒÓНетрудно убедиться в том что эта формула истинна в одних интерпретациях и ложна в других.Присоединим ее в качестве нелогической аксиомы. Тогда получим непротиворечивую теориюT0 .

Действительно, если T0 ` Y и T0 ` ¬Y , то X ` Y и X ` ¬Y (X — единственная нелогическая аксиома), откуда в силу правила введения отрицания заключаем, что ` ¬X. Но этоневерно, поскольку ¬X не является общезначимой. В то же время и сама формула X по темже соображениям не выводима в исчислении предикатов.Однако исчисление предикатов полно в широком смысле. Доказательство этого факта,известного как теорема Геделя о полноте, опирается на следующую теорему, также дока-ÌÃÒÓÌÃÒÓэтой теории. Построенное нами исчисление предикатов можно трактовать как формальнуюаксиоматическую теорию с пустым множеством нелогических аксиом.Любая интерпретация языка Ω будет также называться интерпретацией формальной аксиоматической теории T . Модель теории T — это такая интерпретация теории, при которойкаждая нелогическая аксиома является истинной (аксиомы замкнуты и не требуют оценки).Для исчисления предикатов любая интерпретация является моделью, поскольку имеет толькологические аксиомы, истинные в любой интерпретации.Если формальная теория имеет модель, то она называется интерпретируемой.

Отметим, что если среди нелогических аксиом есть противоречия (т.е. формулы, ложные в любойинтерпретации), то такая теория не интерпретируема. Теория непротиворечива, если несуществует такой замкнутой формулы X, что T ` X и T ` ¬X.Формальную теорию называют полной в узком смысле, если присоединение любой невыводимой замкнутой формулы к списку нелогических аксиом приводит к противоречивой теории.Полнота в широком смысле для исчисления предикатов — выводимость в этой теории любой общезначимой формулы.Покажем, что исчисление предикатов не является полным в узком смысле. Полагаем, чтоязык этой теории имеет хотя бы один предикатный символ p положительной арности (иначеэто исчисление высказываний).