1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 50
Текст из файла (страница 50)
А для обнаружения доказуемости бескванторной формулытребуются только пропозициональные (и структурные) правила.Более точно, пусть Ф-бескванторная формула, а\Jio, ... , Фп -всеразличные атомарные подформулы формулы Ф; тогда пропозициональной формой формулы Ф назовем формулу Фр исчисления высказываний, которая получается из Ф подстановкой всюду вместо подформулы\Jiiпропозициональной переменнойПредложениечисленииG6.4.23.Pi, i=О,...
, п.Бескванторная формула Ф доказуема в истогда и только тогда, когда ее пропозициональнаяформа Фр доказуема в исчислении высказываний.До к аз ат ел ь ст в о.Прямовытекает изсвойстваподформуль-ности.DУпражнение1.Доказать замечание6.4.14.(Указание. Рассмотреть последовательность формул, начинающуюся с исходной и удовлетворяющейусловиям(1 )-(3)из доказательства предложенияпользоваться упражнением4из§ 6.1.)6.4.2,и вос§ 6.5. Исчисления резольвент245Исчисления резольвент§ 6.5.Исчисления резольвент используются для поиска вывода в исчислениях высказываний ипредикатов.Начнем с пропозициональноговарианта.Формулами пропозициональных исчислений резольвент будут пропозициональные переменные или их отрицания.Если Фформула, то Ф* есть ~Ф, когда Ф-переменная, и есть Р, когда Ф=пропозициональная-~р.Основным синтаксическим понятием будет список формул.
Пустойсписок будем обозначать символом 0. Исчисления резольвент будутиметьодниими. Если Го;тежеправила... ; Г n -выводаиразличатьсятолькоаксиомасписки формул, то через Rр(Го; ... ; Г п) будемобозначать (пропозициональное) исчисление резольвент, аксиомамикоторого являются списки Го;... ; Г n·Правилами вывода исчислений резольвент будут:l. Г,Ф; 8,Ф*,2 _ Г,Ф,Ф,8'г,еЗ. Г,Ф,Ф_Г,Ф,Ф,8Г,ФПонятие доказательства (в виде дерева) определяется обычнымобразом. Если Гнепустой список формул, то через Л Г будем-обозначать конъюнкцию формул из Г.
Формула Л Г является формулойисчисления высказываний, но, вообще говоря, не является формулойисчисления резольвент.ЛеммаЕсли6.5.1.доказательствоDв Rр(Го; ... ; Г п) и Г n встречается на вершинеспискаГто для любогоD,списка Г' в Rр(Го; ... ; Гп-1; Г',Гп) доказуем список Г',Г.Д о к аз ат ель ст в опроводитсяD. Если D = Гп, то ГВ Rр(Го; ... ; Г n-1; Г', Г п).Do;DiпDусть=-Г--ииндукцией=дереваuпоследнииГпипочислуГ',Гпереход естьсписковдоказательствог 0 Ф· Г 1 Ф*'~Г,Г1',тогда0,по индукционному предположению существуют доказательства D D~в Rр(Го; ...
; Г n-1; Г', Г п) списков Г', 0 , Ф (или 0 , Ф, если Г n не встречается на вершине Do) и Г', Г 1 , Ф* (или Г 1 , Ф*, если Г n не встречаетсяrвD1)rсоответственно. Так как Г п встречается на вершинена вершинеD 1,Doилито по крайней мере одно из деревьевГ',r 0 , Г', Г 1 'есть доказательство вD 0;D~D 0;D~Г 1 ,Г 0 ,Г 1 'г 0 ,Г',Г 1Rp (Го; ... ; Г n-1; Г', Г п).Из заключительногосписка структурными правилами легко получается список Г', Г.246Гл.6.Теория доказательствЕсли последний переход дереваили3,осуществляется по правиламDто индукционный шаг очевиден.2DДокажем теперь утверждение, связывающее исчисление резольвентс доказуемостью в исчислении высказываний.Предложение6.5.2.Если Го;... ;Гп -непустые списки формулпV (/\ Гi)(исчисления резольвент), то формуладоказуема в ucчuci=Oлении высказываний тогда и только тогда, когда в исчисленииRр(Го; ...
; Г п) доказуем пустой список формул !о.До к аз ат ель ст в о.Пустьтакое дерево списков формул,D -что на вершинах стоят непустые списки формул80; ... ; ek,каждыйпереход есть переход по одному из правил вывода исчисления резольвент, азаключительный (быть может, пустой) список формул.8 -Докажем, что тогда в исчислении высказываний доказуема секвенцияk8 1-V (/\ 8i)-Доказывать будем индукцией по числу списков формулi=Oв деревеD.D состоит из единственного (непустоrо) списка 8, тогдасеквенция 8 1- /\ 8, очевидно, доказуема в исчислении высказывании.Do; D, .
90., ••• ., 90ko - списки, стоящиепусть дерево D имеет вид -~--,Пусть0на вершинах деревадереваDo; 86; ... ; 8k 1-списки, стоящие на вершинахПусть заключительный переход естьD,.80,Ф;е,, Ф*е(тогда 8 = 80, 8 1). По индукционному предположению в исчислениивысказываний доказуемы секвенции 80, Ф 1- Ф 0 и 8 1, Ф* 1- Ф 1 , где Ф 0 =ko=V(/\ е?)k1V(/\ е}).и Ф1 =i=OТогда деревоi=O1-ФVФ*;80, Ф 1- Ф 081, Ф* 1- Ф 18о,Ф!-Ф 0 vФ 1 ;81,Ф*!-Ф 0 vФ 180, 81 1- Ф 0 V Ф 1есть квазивывод нужной секвенции для дереваследний переход в деревеили3,очевиден.DD.Случаи, когда посоответствует структурным правиламИз доказанного утверждения вытекает,пв Rр(Го; ...
; Г п) доказуем пустой список формул, то формуладоказуема в исчислении высказываний.2что еслиV (/\ Гi)i=O247§ 6.5. Исчисления резольвентДлядоказательстваобратногопропозициональный вариантGрутвержденияисчисленияG.будемиспользоватьИндукцией по числусимволов конъюнкций в секвенции(6.7)покажем, что если эта секвенция доказуема вGp, то в Rp(0o; ... ; ek)доказуем пустой список.Пусть секвенцияимеет видФо,f-(6.
7) не содержит знака конъюнкции. Тогда... , Фk, где Фi - пропозициональные переменныеих отрицания. Такая секвенция доказуема вслучае, когда существуют~i, jkGртакие, что Фiонаилив том и только в том= ФJ,тогдаФj;ФJ!оесть доказательство в Rр(Фо;Пусть для секвенций... ; Фk)вида (6.7) счислом знаков Л, меньшим п,утверждение справедливо. Пусть секвенцияи ek= 02, 0l,где 02 и 0l -(6. 7)имеет п знаков Лнепустые списки формул. По свойствуобратимости, если секвенция(6.7) доказуема, то доказуемы и секвенции f- Л 80, ...
, Л ek-1, Л 02 и f- Л 80, ... , Л ek-1, Л 0l. По индукционному предположению в Rp(80; ... ;8k-1;02) и Rp(80; ... ;8k-1;8l)доказуем пустой список 1о. Пусть Do и D1 - соответствующие доказательства. Если el не встречается на вершинах дерева D1, тоD1 - доказательство (списка 0) в Rp(0o; ... ; 8k-1) и тем болеев Rp(0o; ... ; ek_ 1; ek).
Если же 0l встречается на вершинах дереваD1, то по лемме 6.5.1 в Rp(80; ... ;ek-1;8k = 02,el) существует доказательство D 0 спискаПодставляя в Do на место всехвершин вида 02 дерево Dв Rp(0o; ... ; 0k).02.0, получимдоказательство пустого спискаВозвращаемся к доказательству нужного утверждения. По свойствупобратимости формулаV (ЛГi)i=Oкогда доказуема секвенцияf-доказуема вЛ Го,... , Л Г n·Gp тогда и только тогда,По только что доказанно-му утверждению из доказуемости секвенциичто в Rр(Го;f- Л Го, ...
, Л Г п следует,... ; Г п) доказуем пустой список формул !о.DПерейдем теперь к изучению исчислений резольвент для исчисления предикатов.Формулами исчисления резольвент будут атомарные формулы исчисленияGили их отрицания. Для формулы Ф обозначение Ф* определяется, как выше. Правилами вывода будут правилаг4. (Г)f'1, 2, 3и правило248Гл.где х= х,, ... , Xk6.Теория доказательствсписок различных переменных, аt = t,, ... , tkсписок термов.Исчисления резольвент различаются аксиомами. Исчисление резольвент с аксиомами (списками) Го;...
; Г побозначается R(Го;... ; Г п)Связь исчисления резольвент с доказуемостью в исчислении предикатов устанавливается следующим утверждением.Предложение-6.5.3.Предположим, чтозамкнутая формула исчисления предикатов, а Гi,i=О,... , п,непустые списки атомарных формул или их отрицаний. Формула Фдоказуема в исчислении предикатов тогда и только тогда, когдав исчислении резольвент R(Го;... ; Г п) доказуем пустой списокформул.До к аз ат ель ст в о. Пусть Ф - доказуемая в G формула,по предложению 6.4.22 существуют такие наборы термов t 1 =. . . , tfn; ... ; = tf, ... ,t~, что доказуема секвенцияt:тогдаtl, ...Доказуемость этой секвенции равносильна доказуемости формулыПо предложению 6.4.23 формула Ф' доказуема тогда и только тогда,когда доказуема пропозициональная формула Ф~.
Используя предложение6.5.2, из доказуемости формулы Ф~ в исчислении высказыванииполучаем, что в исчислении резольвент R ( ... ; (Гi)i,; ... ) доказуем пустой список с использованием только правил1-3.(Для этого в доказательстве пустого списка в пропозициональном исчислении резольвент,связанном с формулой Ф~, нужно сделать обратную замену пропозициональных переменных на соответствующие элементарные формулы.)Но так как списки (Гi)i, получаются из списков Гi по правилу 4, тополучаем, что в R(Го;Для6.5.2,... ; Г п) доказуем пустой список.доказательства обратного утверждения,будем доказывать такое утверждение: есликак вD -предложениидоказательство§ 6.5.спискав R(Го;0249Исчисления резольвент...
; Г п) и х=х1, ... , Xm -список всех переменныхиз формул списков Го; ... ; Г n, то существуют такие наборы термов-i-i-i.tt 1 , ..• , tm, i1, ... , k, что в исчислении G доказуема секвенция==с У.(~ (Nг,)i)).0Доказательство проводится индукцией по числу списков в доказательствеВ случае, когдаD.есть просто список Гi, следующееDдерево будет квазивыводом нужной секвенции:Гi f-- /\ГikV (/\ rj)ri f--j=IПусть доказательствое'8 ,где0 = (0')f.наборов термовDимеет видD'8 ,а последний переход естьПо индукционному предположению для некоторых-1-kt , ...
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
