5 - Исчисление предикатов . Построение теории P. Правила естественного вывода. Глобальные свойства теории P (1059975)
Текст из файла
Московский государственный технический университетимени Н.Э. БауманаÌÃÒÓФакультет «Фундаментальные науки»Кафедра «Математическое моделирование»À.Í. ÊàíàòíèêîâÄÈÑÊÐÅÒÍÀßÌÀÒÅÌÀÒÈÊÀÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÊîíñïåêò ëåêöèéÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÄëÿ ñòóäåíòîâ ñïåöèàëüíîñòè<Ïðèêëàäíàÿ ìàòåìàòèêà>ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12Москва2006ÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓ5. ИСЧИСЛЕНИЕ ПРЕДИКАТОВ7)8)9)10)11)Y →X ∨Y;X → Z → (Y → Z → (X ∨ Y → Z));X → Y → (¬Y → ¬X);¬¬X → X;X → ¬¬X.ÔÍ-12Еще четыре схемы связаны с кванторами (ниже Xtx — правильная подстановка терма tвместо переменной x, Y не содержит свободных вхождений переменной x):12) ∀x X → Xtx ;13) ∀x (Y → X(x)) → (Y → ∀x X(x));14) Xtx → ∃x X;15) ∀x (X(x) → Y ) → (∃x X(x) → Y ).В дополнение к правилу modus ponens добавляется правило обобщения:X, X → Y;1∗YX2∗.∀x X51ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12X → (Y → X);X → Y → (X → (Y → Z) → (X → Z));X ∧ Y → X;X ∧Y →Y;(X → Y ) → ((X → Z) → (X → Y ∧ Z));X →X ∨Y;ÌÃÒÓ1)2)3)4)5)6)ÔÍ-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ÌÃÒÓÌÃÒÓ5.1. Построение теории PÌÃÒÓТеорема о дедукции. Правила естественного вывода исчисления высказываний. Новые правила:Γ`XXp2) Γ`∀xp1) Γ`∀yX x (введение общности);Γ`X x (удаление общности);ÌÃÒÓÔÍ-12yΓ`XtxΓ`∃x XÔÍ-125.2. Правила естественного выводаÌÃÒÓПример 5.1. Пусть переменная y не имеет свободных вхождений в X. Тогда ` ∀x X →→ ∀y (Xyx ). Действительно:1) ∀x X → Xyx (схема аксиом 14);2) ∀y (∀x X → Xyx ) (по правилу обобщения из 1);3) ∀y (∀x X → Xyx ) → (∀x X → ∀y Xyx ) (схема аксиом 12);4) ∀x X → ∀y Xyx (по правилу модус поненс из 3 и 4);ÔÍ-12ÌÃÒÓÌÃÒÓ52Как и в исчислении высказываний выводом называем последовательность формул языка, вкоторой каждая формула либо аксиома, либо получена по одному из правил вывода из предшествующих формул.
Также вводим понятие вывода из гипотез Γ, в котором в последовательностиформул могут находиться формулы из списка Γ. Однако для вывода из гипотез введем дополнительное структурное требование: если формула ∀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 выводима из гипотез Γ.
Эту записьназываем секвенцией.p3)t(введение существования);p4)Γ,X`YΓ,∃y Xyx `Y(удаление существования).Пример: ∃x X → ¬∀x(¬X).Как и в случае исчисления высказываний, на практике вывод строится с помощью правилестественного вывода. Сохраняются структурные правила естественного вывода, так как онине связаны с сутью самого вывода. Сохраняется теорема о дедукции. Однако в доказательствоэтой теоремы необходимо внести некоторые коррективы.ÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-125. ИСЧИСЛЕНИЕ ПРЕДИКАТОВJ Доказательство теоремы, как и в исчислении высказываний, проводится индукцией по построению формулы. Рассуждения в основном повторяют доказательство теоремы из исчислениявысказываний.
Дополнительно надо лишь рассмотреть случай, когда конечная формула выводаполучена по правилу обобщения.Итак, пусть в выводе X1 , X2 , . . . , Xi = X, . . . , Xj , . . . , Xn конечная формула имеет видXn = ∀xXj . Предположим в выводе формулы Xj формула X не используется. Тогда Γ ` Xj иÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12Теорема 5.1.
Если Γ, X ` Y , то Γ ` X → Y .ÌÃÒÓТеорема о дедукции позволяет без изменений перенести в исчисление предикатов все восемь логических правил естественного вывода, а вслед за ними и дополнительные правилаестественного вывода: доказательства этих правил не используют правила обобщения. Крометого, добавляются следующие четыре правила с кванторами (в этих правилах x не имеет свободных вхождений в формулы списка Γ и Y ; если y отлично от x, то y не входит свободнов X):Γ`X(введение общности);Γ ` ∀y XyxΓ ` ∀x X(удаление общности);p2)Γ ` XtxΓ ` Xtx(введение существования);Γ ` ∃x XΓ, X ` Yp4)(удаление существования).Γ, ∃y Xyx ` Yp3)При выводе формулы p1 учтем, что формулы списка Γ не содержат переменной x:Γ ` ∀yXyxΓ ` ∀xX → ∀yXyxΓ ` ∀xXΓ ` ∀y(∀xX → Xyx )` ∀y(∀xX → Xyx )` ∀xX → XyxФормула p2 непосредственно следует из аксиомы 12:ÌÃÒÓ` ∀y(∀xX → Xyx ) → (∀xX → ∀yXyx )Γ`XÔÍ-12ÔÍ-12ÌÃÒÓ53Γ ` ∀x Xj .
С помощью аксиомы ∀x Xj → (X → ∀x Xj с помощью правила заключения получаемΓ ` 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 . Ip1)ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-125. ИСЧИСЛЕНИЕ ПРЕДИКАТОВ` ∀xX → XtxАналогично выводится и формула p3:Γ ` ∃xX` Xtx → ∃xXΓ ` XtxΓ, ∃yXyx ` YΓ, ∃yXyx ` ∃yXyxΓ, ∃yXyx ` ∃yXyx → YΓ ` ∃yXyx → Y` ∀y(Xyx → Y ) → (∃yXyx → Y )Γ ` ∀x(X → Y )∀x(X → Y ) ` ∀y(Xyx → Y )Γ`X →Y∀x(X → Y ) ` Xyx → Y∀x(X → Y ) ` ∀x(X → Y )ÌÃÒÓΓ, X ` Y` ∀x(X → Y ) → (X → Y )xyÔÍ-12Γ ` ∀y(Xyx → Y )ÔÍ-12ÔÍ-12ÔÍ-12Наиболее длинный вывод получается для правила p4:ÌÃÒÓΓ ` ∀xXÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12Γ ` XtxÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓ54Использование правил естественного вывода такое же, как и в случае исчисления высказываний.Пример 5.2.
Выведем ∃x X → ¬∀x(¬X). Имеем цепочку преобразований снизу вверх“:”∃x X → ¬∀x(¬X) ⇐ ∃x X ` ¬∀x(¬X) ⇐ Xyx ` ¬∀x(¬X) ⇐ ∀x(¬X) ` ¬Xyx .ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-125. ИСЧИСЛЕНИЕ ПРЕДИКАТОВÔÍ-12Введенное нами понятие вывода из гипотез сохраняет истинность формул при фиксированной модели и фиксированной оценке.Лемма 5.1. Пусть Γ — список формул X1 , X2 , . .
. , Xm и Γ ` Y . Если для данной моделиM и данной оценки θ формул X1 , X2 , . . . , Xm , Y в M истинны X1 θ, X2 θ, . . . , Xm θ, то и Y θ вM истинна.ÌÃÒÓÌÃÒÓÔÍ-12Следствие 5.1. Если Γ ` X и все формулы в Γ являются логическими законами, то и Xесть логический закон. В частности, если ` X, то X — логический закон.ÔÍ-12J Доказательство проводится индукцией по длине вывода. Утверждение очевидно, если выводсодержит одну формулу, которая в этом случае есть либо аксиома (являющаяся логическимзаконом), либо гипотеза Xj . Но тогда Y θ и Xj θ — одно и то же.Предположим утверждение доказано для всех выводов длины менее k.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
