Новиков Ф.А. Дискретная математика для программистов (860615), страница 31
Текст из файла (страница 31)
Тогда 1(A) = Т и С' = С, А' = А = В - С.Имеем:. . , А'пС, \~л С —• ( Б —• С) (аксиома А\ с подстановкой {С/А}),следовательно, А'х,..., А'п\- л В —> С = А'.Пусть теперь / ( Б ) = Т и 1(C) = F. Тогда А' = ->А = - ( Б - С), В' = В иС' = - С . Имеем: А[,..., А'п Ь £ Б,. . . , А'п Ь £ -«С, Ь £ Б(-.С - - ( Б - С))по теореме 4.3.7, е. Следовательно, А[,..., А'п Ь,с - ( Б —> С) = А'.•ТЕОРЕМАТеоремами теории L являются общезначимые формулы и только они:|-£ А «=>> А — тавтология.ДОКАЗАТЕЛЬСТВО[ 4 = ] Пусть А — тавтология. Тогда А\,..., А'пА в любой интерпретации.Таким образом, имеется 2П различных выводимостей А'х,..., А'п 1-£ А.
Среди нихесть две, которые различаются в А'п: А'х,..., А'п_х, ап\-цАиА[,...,А'п_1, -*ап \~лА.По теореме дедукции А\,..., А'п_1 \~л ап —> А и А[,...,1-£ ->ап —> А. Но1~£ (а п —> А) —• ((-an —> Л) —> А) по теореме 4.3.7, ж, с подстановкой ап//А,160Глава 4. Логические исчисленияА//В, следовательно, А\,...имеем he А.,A'n_lА. Повторив этот процесс ещё п — 1 раз,[ =Ф> ] Аксиомы Ai, А 2 , АЗ суть тавтологии. Правило Modus ponens сохраняеттавтологичпость (см.
4.1.3), следовательно, теоремы теории & суть тавтологии. •СЛЕДСТВИЕТеория Я формально непротиворечива.Все теоремы £ суть тавтологии. Отрицание тавтологии не естьтавтология. Следовательно, в £ нет теоремы и её отрицания.•ДОКАЗАТЕЛЬСТВО4.3.9. Другие аксиоматизации исчисления высказыванийТеория L не является единственной возможной аксиоматизацией исчислениявысказываний. Её основное достоинство — лаконичность при сохранении определённой наглядности. Действительно, в теории £ всего две связки, три схемыаксиом и одно правило. Известны и многие другие аксиоматизации исчислениявысказываний, предложенные различными авторами.1. Гильберт1 и Аккерман2, 1938.Связки:Аксиомы:лvвПравило:2. Россер3, 1953.Связки:Аксиомы:Правило:3.
Клини\ 1952.Связки:Аксиомы:Def, -i;(Л —> В = -^ЛЛ V Л ^ А,Л ^ А V В,VVВ -> ЛVС).Def(Л -> В = - ( Л к-В)).Л ^ Л к л,А к ВЛ,(ЛВ)( - ( В & С) —> -ч(С & Л)).Modus ponens.Л _> (В - Л),(Л(В - С)) - ((Л —> В) —>• (Л —> С)),Л —> (В —• (Л &; В)),Л(Л V В),1В).в v л,{ВС)(ЛModus ponens.л & в -> л,л & в —• в,оVДавид Гильберт ( 1 8 6 2 - 1 9 4 3 ) .Вильгельм Аккерман ( 1 8 9 6 - 1 9 6 2 ) .3Д ж о и Беркли Россер ( 1 9 0 7 - 1 9 8 9 ) .4Стефан Клини ( 1 9 0 9 - 1 9 9 4 ) .1614.4.
Исчисление предикатовВ —>• (Л V В),( А ^ С ) ^ ((В -» С) -> ((A V B ) - » С)),(Л —• В)((Л - - В ) -> -.А),—I—«А -> А.Modus ponens.Правило:Никод 1 , 1917.Связка:Аксиома:|;(А | В = ->А V -.В).(Л | (В | С)) | ((£> | (D \ D)) \| ((Е | В) | ((Л \ Е ) \ ( А \ Е)))).А,А\(В\С)СПравило:4.4. Исчисление предикатовОписание формальной теории исчисления предикатов в этом разделе носит конспективный характер, в частности, многие технически сложные доказательстваопущены.
В то же время уделено внимание прагматическим аспектам теории, тоесть ответу на вопрос, что выразимо и что невыразимо в исчислении предикатов.4.4.1. Определения(Чистое) исчисление предикатов (первого порядка) — это формальная теория ОС,в которой определены следующие компоненты: алфавит, формулы, аксиомы иправила вывода.1. Алфавит:связкиосновныедополнительныеслужебные символы—>&, V( , )кванторывсеобщностисуществованияконстантыпеременныепредметныепредметныепредикатыфункциональные символыV3а, Ъ,..., а\,х, у,..., х\,Ь\,...у\,...P,Q,...f,g,...С каждым предикатом и функциональным символом связано некоторое натуральное число п, которое называется арностью, местностью или вместимостью.2.
Формулы имеют следующий синтаксис:(формула)1:: =Жаи Никод ( 1 8 9 3 - 1 9 2 4 ) .(атом) |-•(формула) |((формула) —» (формула)) |V (переменная) ((формула)) |162(атом)(список термов)(терм)Глава 4. Логические исчисления3 (переменная) ((формула))(предикат)((список термов))(терм) | (терм), (список термов)(константа) |(переменная) |(функциональный символ)((список термов))При этом должны быть выполнены следующие контекстные условия: в термеf(ti,... ,tn) функциональный символ / должен быть n-местным. В атоме (илиатомарной формуле) P(ti,..., tn) предикат Р должен быть п-местным.Вхождения переменных в атомарную формулу называются свободными.
Свободные вхождения переменных в формулах А и В по определению считаютсясвободными в формулах ->А и А —• В. В формулах Vx (Л) и За; (А) формулаА, как правило, имеет свободные вхождения переменной х. Вхождения переменной х в формулы Vx (А) и Зх (А) называются связанными. Вхождения другихпеременных (отличных от х), которые были свободными в формуле А, по определению считаются свободными и в формулах \/х (А) и Зх (А).
Одна и таже переменная может иметь в одной и той же формуле как свободные, так исвязанные вхождения. Если все вхождения переменной в формулу связаны, топеременная называется связанной (в данной формуле). Формула, не содержащаясвободных вхождений переменных, называется замкнутой.
В замкнутой формулевсе переменные связаны.Пример Рассмотрим формулу Vx ((Р(х) —» Зу (Q(x,y)))) и её подформулы.В подформулу 3 у (Q(x, у)) переменная х входит свободно, а все вхождения переменной у связаны (квантором существования). Таким образом, эта подформулане замкнута. С другой стороны, то же самое вхождение переменной х в подформулу Q{x,y) является связанным в формуле Vx (Р(х) —> Зу (Q(x,y))).
В этойформуле все вхождения всех переменных связаны, а потому формула замкнута.ЗАМЕЧАНИЕЯзык теории L не содержит кванторов, поэтому понятия свободного и связанного вхождения переменных не применимы непосредственно. Можно расширить исчисление высказываний, допуская замкнутые формулы исчисления предикатов наравне с пропозициональными переменными. В таком случае для удобства обычно полагают, что все формулытеории L замкнуты.Формулы вида А и ->Д где А — атом, называются литеральными формулами(или литералами).В формулах Vx (А) и Зх (Л) подформула А называется областью действияквантора по х.Обычно связки и кванторы упорядочивают по приоритету следующим образом:-л, V, 3, & , V, —>.
Лишние скобки при этом иногда опускают.1634.4. Исчисление предикатовТерм t называется свободным для переменной ж в формуле А,бодное вхождение переменной х в формулу А не лежит вникакого квантора по переменной у, входящей в терм t. Всвободен для любой переменной в формуле А, если никакаяне является связанной переменной формулы А.если никакое свообласти действиячастности, терм tпеременная термаПример Терм у свободен для переменной х в формуле Р{х), но тот же терм уне свободен для переменной х в формуле У у (Р(х)). Терм /(ж, z) свободен дляпеременной х в формуле My (Р(ж, у) —> Q(x)), но тот же терм /(ж, z) не свободендля переменной х в формуле 3z (My (Р(х,у) —> Q(x))).3.
Аксиомы (логические): любая система аксиом исчисления высказываний плюсPi:МхР2:A(t)^3x(A(x)^A(t)),(А(х)),где терм t свободен для переменной х в формуле А.4. Правила вывода:А, АВ— Р —,(M°d u S Р0ПеП8)'В —• А(х)В - У ж (Л(ж)),w+,(VА(х)->ВЗ ж ( Л ( ж ) ) - В < 3+ >'где формула А содержит свободные вхождения переменной ж, а формула В ихне содержит.Исчисление предикатов, которое не содержит предметных констант, функциональных символов, предикатов и собственных аксиом, называется чистым.
Исчисление предикатов, которое содержит предметные константы и/или функциональные символы и/или предикаты и связывающие их собственные аксиомы,называется прикладным.Исчисление предикатов, в котором кванторы могут связывать только предметныепеременные, но не могут связывать функциональные символы или предикаты,называется исчислением первого порядка. Исчисления, в которых кванторы могутсвязывать не только предметные переменные, но и функциональные символы,предикаты или иные множества объектов, называются исчислениями высшихпорядков.Практика показывает, что прикладного исчисления предикатов первого порядка оказывается достаточно для формализации содержательных теорий во всехразумных случаях.4.4.2.
ИнтерпретацияИнтерпретация I (прикладного) исчисления предикатов % с областью интерпретации (или носителем) М — это набор функций, которые сопоставляют:1) каждой предметной константе а элемент носителя 1(a), 1(a) € М;2) каждому n-местпому функциональному символу / операцию 1 ( f ) на носителе, 1(f): Мп — М;164Глава 4. Логические исчисления3) каждому п-местному предикату Р отношение 1(Р) на носителе, 1(Р) сМп.Пусть х — ( x i , .
. . ) — набор (последовательность) переменных (входящих в формулу), a s = ( s i , . . . ) — набор значений из М. Тогда всякий терм f(t\,...,tn)имеет значение на s (из области М), то есть существует функция s*: {£} —» М,определяемая следующим образом:s*{a)^I{a),з*(хг)8*(f(t1,...,tn))1£l(f)(a*(t1),...,s*{tn)).Всякий атом P(t\,... ,tn) имеет на s истинностное значение s*(P), определяемоеследующим образом:s*(P(tь ..., tn)) ^(s*(ti), • • •, S*(tn)) G I(P).Если s*(P) = T, то говорят, что формула Р выполнена па s.Формула -IJ4 выполнена на s тогда и только тогда, когда формула А не выполненапа s.Формула А —> В выполнена на s тогда и только тогда, когда формула А невыполнена па s или формула В выполнена па s.Формула Ух^ (Л) выполнена на s тогда и только тогда, когда формула А выполнена на любом наборе s', отличающемся от s, возможно, только г-м компонентом.Формула 3x,i (Л) выполнена на s тогда и только тогда, когда формула А выполнена па каком-либо наборе s', отличающемся от s, возможно, только г-мкомпонентом.Формула называется истинной в данной интерпретации /, если она выполнена на любом наборе s элементов М.
Формула называется ложной в даннойинтерпретации I, если она не выполнена пи на одном наборе s элементов М.Интерпретация называется моделью множества формул Г, если все формулы изГ истинны в данной интерпретации.Всякая замкнутая формула истинна или ложна в дайной интерпретации. Открытая (то есть не замкнутая) формула A(x,y,z,...)истинна в данной интерпретации тогда и только тогда, когда её замыкание Vx (V?/ (V2 • • • А(х,y,z,...)))истинно в данной интерпретации.ЗАМЕЧАНИЕЭто обстоятельство объясняет, почему собственные аксиомы прикладных теорий обычнопишутся в открытой форме.4.4.3.
ОбщезначимостьФормула (исчисления предикатов) общезначима, если она истинна в любой интерпретации.ТЕОРЕМА Формула^ х (А(х)) —> A(t), где терм t свободен для переменной х в формуле А, общезначима.1654.4. Исчисление предикатовРассмотрим произвольную интерпретацию I, произвольную последовательность значений из области интерпретации s и соответствующую функцию s*. Заметим следующее. Пусть t\ — терм и s*(ti) = а\. Пусть t{x) — некоторый другой терм, a t': = t(... х ... ){t\//x}.Тогда s*(t) = s*(£')> где s 1 имеетзначение ai па месте х. Пусть теперь А(х) — формула, а терм t свободен для хв А.