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

ÔÍ-12ÔÍ-12ÌÃÒÓМосковский государственный технический университетимени Н.Э. БауманаÌÃÒÓФакультет «Фундаментальные науки»Кафедра «Математическое моделирование»ÌÃÒÓÀ.Í. ÊàíàòíèêîâÈ ÒÅÎÐÈß ÀËÃÎÐÈÒÌÎÂÊîíñïåêò ëåêöèéÔÍ-12Москва2009ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12Äëÿ ñòóäåíòîâ êàôåäðû ÈÓ9ÌÃÒÓÌÃÒÓÌÀÒÅÌÀÒÈ×ÅÑÊÀß ËÎÃÈÊÀÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓ4. ИСЧИСЛЕНИЕ ПРЕДИКАТОВ7) Y → X ∨ Y ;2) X → Y → (X → (Y → Z) → (X → Z));8) X → Z → (Y → Z → (X ∨ Y → Z));3) X ∧ Y → X;9) X → Y → (¬Y → ¬X);4) X ∧ Y → Y ;10) ¬¬X → X;5) (X → Y ) → ((X → Z) → (X → Y ∧ Z));11) X → ¬¬X.6) X → X ∨ Y ;Еще четыре схемы связаны с кванторами (ниже Xtx — правильная подстановка терма tвместо переменной x, Y не содержит свободных вхождений переменной x):∀x X → Xtx ;∀x (Y → X(x)) → (Y → ∀x X(x));Xtx → ∃x X;∀x (X(x) → Y ) → (∃x X(x) → Y ).В дополнение к правилу заключения (modus ponens) добавляется правило обобщения:ÔÍ-1242ÔÍ-12X, X → Y;YX.2∗∀x XКак и в исчислении высказываний, выводом называем последовательность формул языка, вкоторой каждая формула либо аксиома, либо получена по одному из правил вывода из предшествующих формул.

Также вводим понятие вывода из гипотез Γ (частного вывода), в котором1∗ÌÃÒÓ12)13)14)15)ÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓ1) X → (Y → X);ÔÍ-12ÔÍ-12Исчисление предикатов строится как расширение исчисления высказываний. Основная цельта же: формализовать доказательство различного рода утверждений.

Исчисление предикатов — составная часть любой формальной теории, отвечающая за логическую часть теории.Мы будем строить теорию P, языком Ω которой является произвольный логико-математический язык. Фактически мы строим целое семейство формальных теорий. Однако все этитеории имеют единую логическую составляющую, отличаясь лишь способом формированияпредметных выражений — термов. Любую из построенных формальных теорий можно трансформировать так, что предметная составляющая будет простейшей: один сорт переменных приотсутствии констант и функциональных символов.

Упрощается и интерпретация простейшегоязыка. Достаточно задать единую предметную область для всех предметных переменных иуказать отображение, которое n-арному предикатному символу ставит в соответствие булевуфункцию от n переменных, а в случае 0-арного предикатного символа — символ 0 или 1.Зададим аксиомы исчисления предикатов в виде некоторого набора схем аксиом. Первыеодиннадцать схем повторяют схемы исчисления высказываний:ÌÃÒÓÌÃÒÓЯзык алгебры предикатов как расширение языка алгебры высказываний.

Аксиомы исчисления предикатов: схемы аксиом исчисления высказываний плюс 4 аксиомы с кванторами:11) ∀x X → Xtx ; 12) ∀x (Y → X(x)) → (Y → ∀x X(x)); 13) Xtx → ∃x X; 14) ∀x (X(x) → Y ) →; 2∗ ∀xXX . Вывод и вывод из гипотез. Струк(∃x X(x) → Y ). Правила вывода: 1∗ X, X→YYтурное ограничение. Секвенции.ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓ4.1.

Построение теории PÌÃÒÓÌÃÒÓÌÃÒÓ4.2. Правила естественного выводаÔÍ-12Теорема о дедукции. Правила естественного вывода исчисления высказываний. Новые правила:XΓ`Xp1) Γ`∀yp2) Γ`∀xX x (введение общности);Γ`X x (удаление общности);yp3)Γ`XtxΓ`∃x Xt(введение существования);p4)Γ,X`YΓ,∃y Xyx `Y(удаление существования).ÔÍ-12ÔÍ-12ÌÃÒÓПример 4.1. Пусть переменная y не имеет свободных вхождений в X. Тогда ` ∀x X →→ ∀y (Xyx ). Действительно:1) ∀x X → Xyx (схема аксиом 12);2) ∀y (∀x X → Xyx ) (по правилу обобщения из 1);3) ∀y (∀x X → Xyx ) → (∀x X → ∀y Xyx ) (схема аксиом 13);4) ∀x X → ∀y Xyx (по правилу заключения из 2 и 3);ÌÃÒÓв последовательности формул могут находиться формулы из списка Γ.

Однако для вывода изгипотез введем дополнительное структурное требование: если формула ∀x X получена по правилу обобщения, то во всех гипотезах, используемых для вывода этой формулы, переменная xне должна иметь свободных вхождений. Указанное структурное требование не касается аксиом.Поэтому в выводе без гипотез его можно не учитывать.Смысл сформулированного структурного требования становится понятным, если учесть,что вывод должен сохранять истинность формул. Правило заключения сохраняет истинностьформул при фиксированной модели и фиксированной оценке, а именно: если θ — оценка формулы X → Y в данной модели M , то из истинности Xθ и (X → Y )θ следует истинность Y θ.Правило обобщения в отсутствие структурного требования нарушает фиксированность оценкипри выводе.Впрочем, структурное требование касается лишь частного вывода.

Мы могли бы это ограничение не учитывать, но тогда нам придется считаться с ним при сшивке“ частных выводов”в окончательный вывод без гипотез. Поясним сказанное. Выводимость из X формулы ∀x Xследует увязать с выводимостью формулы X → ∀x X, т.е. с тем, что эта формула есть тавтология. Но если переменная x входит в X свободно, то при некоторой интерпретации длянекоторого объекта a формула Xax будет ложной, а для некоторого объекта b формула Xbx —истинной. В этом случае ∀x X в соответствии с интерпретацией квантора всеобщности будетложной формулой при любой оценке, а это приведет к ложности X →∀x X.

Однако эта формулабудет тавтологией, если X не имеет свободных вхождений x.Мы сохраняем запись Γ ` X, означающую, что формула X выводима из списка гипотез Γ.Эту запись называем секвенцией.ÌÃÒÓÌÃÒÓ43ÔÍ-12ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-124. ИСЧИСЛЕНИЕ ПРЕДИКАТОВТеорема 4.1. Если Γ, X ` Y , то Γ ` X → Y .J Доказательство теоремы, как и в исчислении высказываний, проводится индукцией по построению формулы. Рассуждения в основном повторяют доказательство теоремы из исчислениявысказываний. Дополнительно надо лишь рассмотреть случай, когда конечная формула выводаполучена по правилу обобщения.Итак, пусть в выводе X1 , X2 , .

. . , Xi = X, . . . , Xj , . . . , Xn = Y конечная формула Y имеетвид ∀xXj . Этот вывод, как свою часть, содержит и вывод формулы Xj . Если в выводе формулы Xj формула X не используется, то можно считать, что ее нет и в выводе X1 , X2 , . . . ,Xn = Y . Добавляя к этому выводу аксиому ∀x Xj → (X → ∀x Xj ) (схема аксиом 1), а затем наÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12Как и в случае исчисления высказываний, на практике вывод строится с помощью правилестественного вывода. Сохраняются структурные правила естественного вывода, так как онине связаны с сутью самого вывода. Сохраняется теорема о дедукции.

Однако в доказательствоэтой теоремы необходимо внести некоторые коррективы.ÌÃÒÓÌÃÒÓПример: ∃x X → ¬∀x(¬X).ÌÃÒÓÔÍ-12ÌÃÒÓ44основании правила заключения X → ∀x Xj , получим вывод формулы X → Y ≡ X → ∀x Xj из гипотез Γ. Пусть формула X используется в выводе формулы Xj . Тогда, согласно структурномутребованию, формула X не имеет свободных вхождений переменной x. Согласно индуктивномупредположению из вывода Γ, X ` Xj вытекает вывод Γ ` X → Xj , откуда по правилу обобщения (ни X, ни гипотезы, использованные в выводе Xj ) не содержат свободных вхождений x)получаем Γ ` ∀x (X → Xj ). Присоединив аксиому ∀x (X → Xj ) → (X → ∀x Xj ), получаем выводформулы X → ∀x Xj , т.е. формулы X → Y .

IÔÍ-12Теорема о дедукции позволяет без изменений перенести из исчисления высказываний в исчисление предикатов все восемь логических правил естественного вывода, а вслед за ними идополнительные правила естественного вывода: доказательства этих правил не используютправила обобщения. Кроме того, добавляются следующие четыре правила с кванторами:ÌÃÒÓΓ ` Xtx(введение существования);Γ ` ∃x XΓ, X ` Yp4)(удаление существования).Γ, ∃y Xyx ` YΓ`X(введение общности);Γ ` ∀y XyxΓ ` ∀x X(удаление общности);p2)Γ ` Xtxp3)p1)В правилах p1 и p4 переменная x не имеет свободных вхождений в формулы списка Γ иформулу Y . Кроме того, если y отлично от x, то y не входит свободно в X. В правилах p2 иp3 подстановка xt должна быть свободной для формулы X.Докажем четыре новых правила естественного вывода.

При выводе формулы p1 учтем, чтоформулы списка Γ не содержат свободных вхождений переменной x:ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-124. ИСЧИСЛЕНИЕ ПРЕДИКАТОВΓ ` ∀xX → ∀yXyxΓ ` ∀xXΓ`X` ∀y(∀xX → Xyx ) → (∀xX → ∀yXyx )Γ ` ∀y(∀xX → Xyx )` ∀y(∀xX → Xyx )ÌÃÒÓÌÃÒÓΓ ` ∀yXyxÔÍ-12ÔÍ-12` ∀xX → XyxФормула p2 непосредственно следует из аксиомы 12:Γ ` Xtx` ∀xX → XtxΓ ` ∀xXАналогично выводится и формула p3:` Xtx → ∃xXΓ, ∃yXyx ` YΓ, ∃yXyx ` ∃xXΓ, ∃yXyx ` ∃xX → Y∃yXyx ` ∃xXΓ ` ∃xX → YΓ ` ∀x(X → Y )` ∀x(X → Y ) → (∃xX → Y )Γ`X →YΓ, X ` YÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12Наиболее длинный вывод получается для правила p4:ÌÃÒÓΓ ` XtxÌÃÒÓÌÃÒÓΓ ` ∃xXÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓ45В этом выводе осталась нераскрытой одна ветка (в рамке).

Соответствующий вывод строитсяна той же аксиоме:∃yXyx ` ∃xX∃yXyx ` ∃yXyx → ∃xX∃yXyx ` ∃yXyxÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-124. ИСЧИСЛЕНИЕ ПРЕДИКАТОВ` ∀y(Xyx → ∃xX)` ∀y(Xyx → ∃xX) → (∃yXyx → ∃xX)` Xyx → ∃xXÔÍ-12Лемма 4.1. Пусть Γ — список формул X1 , X2 , . . . , Xm и Γ ` Y . Если для данной моделиM и данной оценки θ формул X1 , X2 , . . . , Xm , Y в M истинны X1 θ, X2 θ, . . . , Xm θ, то и Y θ вM истинна.ÔÍ-12Остановимся на вопросах непротиворечивости, полноты и разрешимости теории P .