4 - Исчисление предикатов. Построение теории P. Правила естественного вывода. Глобальные свойства теории P (1075771)
Текст из файла
ÔÍ-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 .
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
