И.А. Пушкарев логика
.pdf
|
|
131 |
|
|
|
является |
простой, а |
правило |
r1, Q; r2 , Q |
, соответственно, на |
правило |
|
|||||
|
|
|
r3 , Q |
|
P, r1 , Q; P, r2 , Q . Для правила (Е+) следует сделать исключение, записав его в
P, r3 , Q
виде P, p(x), Q, Eu p(u). P, Eu p(u ), Q
Заметим, что все сделанные модификации ещё не позволяют построить
дерево вывода однозначно: при применении правил(А+) и (Е+) приходится выбирать некоторую новую переменнуюх, и это можно сделать по-разному.
Для устранения этой трудности следует(в третьих J) упорядочить все переменные, не входящие ни вР, ни в Q. Для формулы Au q(u ) в качестве
переменной х будем брать в качестве новой переменной всегда первую ещё не
вошедшую |
свободно |
в |
секвенцию |
переменную. Для |
формулы Eu q(u ) |
||||
(внимание!!) |
сложнее: |
на |
очередном |
шаге |
обработки(такая |
формула |
|||
обрабатывается |
бесконечное |
число |
), размы |
будем |
выбирать |
первую |
|||
переменную, которая ещё не обрабатывалась вместе с этой формулой. |
|
|
|||||||
Дерево |
вывода |
некоторой фиксированной |
секвенции теперь |
строится |
|||||
почти тривиально. В качестве его корня берётся рассматриваемая секвенция. |
|||||||||
Она либо |
является |
аксиомой(тогда |
вывод |
закончился), либо |
простой |
секвенцией, которая аксиомой не является(тогда контрпример найден и секвенция не общезначима), либо результатом применения однозначно определённого правила вывода из одной или двух секвенций, которые и являются детьми этой вершины (вершинами первого уровня). Вершины первого уровня можно рассмотреть по той же схеме(аксиому можно дальше не рассматривать, оборвав ветку), получив, возможно, несколько вершин второго уровня и т.д. Вот теперь действительно всё: дерево вывода однозначно строится для любой исходной секвенции.
По построению, листом построенного дерева может служить только аксиома или простая секвенция.
|
|
|
132 |
|
|
|
|
Если |
получилось конечное |
дерево, каждый |
лист |
которого |
является |
||
аксиомой, |
то, во-первых, |
исходная |
секвенция |
есть |
теорема |
исчисления |
|
секвенций, |
и, во-вторых, к |
ней |
не |
существует |
контрпримера, поэтому она |
общезначима. Если получилось дерево, некоторые листья которого не являются
аксиомами (но являются простыми секвенциями), то контрпример построен и исходная секвенция не общезначима. При этом никакого другого дерева для этой формулы построить нельзя, поэтому формула не является и теоремой исчисления секвенций.
Осталось рассмотреть только случай, когда секвенции соответствует
бесконечное дерево, все листья которого, однако, являются аксиомами. В этом случае формула не является теоремой исчисления секвенций(доказательство должно быть конечно), поэтому в этом случае нужно показать, что исходная секвенция не общезначима. Для этого достаточно построить интерпретацию, в
которой все формулы рассматриваемой секвенции ложны(не забыли: слева,
там где ничего не осталось, должны стоять только истинные формулы, а справа
– только ложные, иначе это никакой не контрпример J).
Если |
дерево бесконечное, то в нём имеется бесконечная |
цепочка |
||
потомков. |
Действительно, пусть секвенция (хотя это неважно) |
S0 |
является |
|
корнем, S1 |
и S2 – его непосредственные потомки (второго может |
и |
не |
быть). |
Одно из одного или двух деревьев, корнями которого являются S1 и S2, должно быть бесконечно. Выберем его как следующую вершину цепи и т.д.
Множество всех формул, входящих в некоторую секвенцию построенной
бесконечной цепочки, обозначим Р. Рассмотрим интерпретацию j ,
предметным множеством которой являются свободные переменные формул,
входящих в Р, определённую своими |
значениями на атомарных |
формулах |
|||
посредством |
правила: для символа n-арного |
отношения r |
и переменных |
||
x1 , x2 , ..., xn |
(j(r ))(x1 , x2 , ..., xn )= 1 |
тогда |
и |
только, |
когдатогда |
Покажем теперь, что "p Î P j(p)= 0 .
133
Для атомарных формул это утверждение верно по определению.
Пусть |
формула р |
имеет видp = Øq(x1 , x2 , ..., xn ), |
где |
формула q |
атомарная. |
Если j(p)=1, |
то j(q)= 0 , то есть q Î P . Но и |
p Î P . |
Поскольку |
простые формулы из секвенций никуда пропасть не могут, найдётся вершина цепочки, в секвенцию, соответствующую которой входятр и q. Но тогда эта секвенция есть аксиома, что противоречит бесконечности цепочки.
Пусть формула р – не простая, но и не имеет вида Eu q(u ) (формулы вида
Au q(u ) тоже рассматриваются в этом пункте!). Формула р входит в некоторую секвенцию, которая не является ни простой секвенцией, – вершину цепочки, в
которой |
|
и |
обрабатывается(любая |
формула когда-то да обрабатывается |
|||
правилом вывода J). Пусть этой вершине соответствует, не умаляя общности, |
|||||||
правило |
|
P, r1 , Q; P, r2 , Q |
. Если j(p)=1, то j(r1 )= j(r2 )=1. Но одна из |
этих |
|||
|
|
P, p, Q |
|||||
|
|
|
|
|
|
||
формул наверняка входит в Р, и они проще формулы р. Противоречие. |
|
||||||
Пусть, |
наконец, p = Eu q(u ). Тогда (в нашей версии правил вывода) |
эта |
|||||
формула, как только до неё доходит очередь, выбрасывает из себя в секвенцию |
|||||||
более |
простую |
формулуq(v j ), и |
происходит это для всех переменных, |
||||
входящих в предметное множество. Следовательно "v j q(v j )Î P , j(q(v j ))= 0 , |
|||||||
что противоречит |
условиюj(p)=1, |
означающему, что $v :j(q(v))=1 . Тем |
самым, в построенной интерпретации все формулы, входящие в исходную секвенцию, ложны, и она не является общезначимой.
Получилась теорема адекватности для исчисления секвенций.
Теорема 14.1. Секвенция является теоремой тогда и только тогда, когда она общезначима.
QED
Замечание. Однозначность построения дерева не означает разрешимости проблемы общезначимости: если дерево ещё не достроилось, то невозможно узнать, будет ли оно конечно.
134
4. Теорема Эрбрана-Генцена
Тот факт, что, вообще говоря, невозможно узнать, конечно ли дерево вывода, не означает, что это невозможно узнать для любой секвенции(это и есть определение словосочетания «вообще говоря» J). Иногда как раз можно.
Определение 14.1. Секвенция называется предварённой, если все формулы, входящие в неё являются предварёнными(т.е. все кванторы в них находятся спереди, например, подойдут формулы, записанные как ПНФ).
Не будем незаслуженно упрощать себе жизнь. Естественно выглядит
первый формализм, а пользоваться при доказательстве теорем удобно вторым или третьим. Однако формально понятия предварённых секвенций в первом формализме и во втором и третьем друг другу не соответствуют: при переносе предварённой формулы слева направо, перед ней возникает отрицание, которое лишает её предварённой формы.
Однако эта трудность не является принципиальной. Для формулы Øs
символом *s обозначим формулу, которая из неё получается, если
«протащить» в Øs отрицание сквозь кванторы, последовательно заменяя Ø А
на Е Ø и, симметрично, ØЕ на АØ . Тогда предварённой «секвенции первого формализма» С = s1 ,..., sm ® t1 ,..., tn семантически эквивалентна предварённая
«секвенция третьего формализма» С * = (* s ,..., * s |
m |
, t ,..., t |
n |
). |
1 |
1 |
|
||
Предположим что предварённая секвенцияS * |
|
выводится в третьем |
||
формализме из бескванторной секвенции P* . Применения правил (А+) и (Е+) к |
формулам вида *si семантически равносильны применениям правил (Е–) и (А–
) соответственно для выводаS из Р. Тем самым, хотя классы предварённых секвенций для первого и третьего формализмов друг другу не соответствуют,
выводимость при помощи |
одних только кванторных правил в перво |
формализме равносильна такой |
же выводимости в третьем. |
135
Теорема 14.2. (Генцен) Для любой общезначимой предварённой секвенции S существует такая бескванторная общезначимая секвенция Р, что S
выводима из Р посредством только «кванторных» правил (А+), (А–), (Е+) и (Е–
).
Доказательство. Рассуждаем в терминах третьего формализма. Во-
первых, забудем о правилах (А*–) и (Е*–), которыми всё равно не собираемся пользоваться (о чём и рассуждали перед формулировкой теоремы). Во-вторых,
T
добавим к правилам вывода«правило забывания» (Х): . Этому правилу
T , U
соответствует принцип: при увеличении секвенции множество контрпримеров к ней увеличивается. Поэтому если трудно построить контрпример к большой секвенции, давайте построим к меньшей, большой он тоже сгодится J. Правда,
если контрпример к меньшей так и не построился, это не значит, что к большой его построить нельзя… Это правило позволяет нам (теоретически) «проскочить через аксиому, её не заметив», позабыв одну из двух противоположных формул, содержащихся в секвенции, но ведь оно не требует это обязательно делать! Зато теперь можно считать, что все аксиомы имеют вид (p, Ø p).
Пусть теперь S – общезначимая предварённая секвенция третьего формализма. По теореме адекватности из этого следует, что она имеет доказательство D (конечное дерево). Предположим, что нам удалось привести доказательство к виду, в котором правила (А+) и (Е+) применяются в самом конце, точнее – любое применение остальных («пропозициональных») правил вывода находится в этом дереве выше любого применения этих«кванторных» правил. Тем самым, дерево доказательства делится на «кванторное» поддерево,
и «пропозициональные» поддеревья, растущие из его листьев. Покажем, что в этом случае теорема доказана.
Заметим, что применения правил (А+) и (Е+) соответствуют вершинам, у
которых ровно один сын, поэтому кванторное поддерево представляет собой цепь, а пропозициональное дерево получается ровно одно, и растёт оно из основания этой цепи. Далее, эти правила сами по себе не позволяют вывести
|
|
|
|
|
136 |
|
|
|
|
предварённую |
секвенцию |
из |
непредварённой, поэтому |
все |
секвенции, |
|
|||
входящие в кванторную цепь, являются предварёнными. |
|
|
|
||||||
Пропозициональное поддерево не содержит кванторных правил, поэтому |
|
||||||||
все кванторы, которые присутствуют в его последней секвенции, содержатся в |
|
||||||||
исходных |
посылках, то |
есть – |
в аксиомах. Однако |
все аксиомы |
имеют вид |
|
|||
(p, Ø p). Заметим, что вторая формула секвенции не может быть предварённой, |
|
||||||||
если формула р |
содержит хотя |
бы один квантор. Следовательно, |
ни одна |
|
|||||
секвенция, входящая в пропозициональные поддеревья, не содержит никаких |
|
||||||||
кванторов, все они появляются только как результат применения кванторных |
|
||||||||
правил. |
Поэтому |
кванторная |
цепь |
представляет |
собой |
иско |
|||
(прямолинейный!) вывод предварённой секвенции из бескванторных. |
|
|
|||||||
Итак, осталось предъявить процедуру, позволяющую из произвольного |
|
||||||||
доказательства получить доказательство требуемого вида. Для построения |
|
||||||||
таковой процедуры достаточно построить один её шаг, то есть показать как |
|
||||||||
переместить |
применение |
|
кванторного |
правила |
под |
прим |
пропозиционального, если оно изначально находится над ним в дереве доказательства. Не умаляя общности, будем рассматривать пропозициональное правило «правилом с двумя посылками»:
T , q1 ; T , q2 .
T , q
В ином случае можно считать, что посылки совпадают: q1 = q2 .
Далее, не умаляя общности, будем считать, что левая посылка этого правила получена как результат применения кванторного правила, то есть в целом картина выглядит так:
|
U , p(x), q1 |
; U , Qu p(u ), q2 |
|
|
U , Qu p(u ), q1 |
, |
|||
|
||||
|
U , Qu p(u ), q |
|||
|
|
где Q – один (любой) из двух имеющихся в наличии кванторов.
Если вверху применяется правило(А+), то переменная x не должна входить как в q1 , так и ни в одну формулу набора U.
|
|
|
|
|
|
|
|
137 |
|
|
|
|
|
|
|
|
|
|
|
|
Рассматриваемый |
фрагмент |
вывода |
|
|
можно |
|
|
заменить |
на , |
друго |
||||||||||
делающий то же самое: |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||
|
|
|
|
|
U , p(x), q1 |
|
; |
|
U , p(x), q2 |
|
|
|
|
|
|
|||||
|
|
|
|
U , Qu p(u ), p x( , )q |
|
U , Qu p(u ), p x( , )q |
2 |
|
|
|
|
|
||||||||
|
|
|
|
|
|
|
|
1 |
|
|
|
|
|
|
. |
|
|
|
|
|
|
|
|
|
|
|
U , Qu p(u ), p x( , )q |
|
|
|
|
|
|
||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
||||||||
|
|
|
|
|
|
|
U , Qu p(u ), q |
|
|
|
|
|
|
|
|
|
||||
Две верхние дроби представляют собой применения правила(Х). Дробь в |
|
|||||||||||||||||||
знаменателе |
– |
применение |
того |
самого правила, которое применялось |
в |
|||||||||||||||
числителе (зависит от того, каков квантор Q). |
|
|
|
|
|
|
|
|
|
|||||||||||
Осталось убедиться с том, что если Q = A , то переменная х не входит в q |
|
|||||||||||||||||||
и ни в одну формулу, входящую в U. В U она не входит, поскольку раньше это |
|
|||||||||||||||||||
самое правило применялось в примерно той же ситуации(во всяком случае U |
|
|||||||||||||||||||
там было то же самоеJ). Для того же, чтобы x не входило вq, придётся |
|
|||||||||||||||||||
изменить часть доказательства, предшествующую |
появлению q |
с тем, чтобы |
|
|||||||||||||||||
изменить все вхождения переменнойx в q на вхождения другой переменной. |
|
|||||||||||||||||||
Это – стандартная процедура, мы её уже неоднократно применяли. |
|
|
|
|||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
QED |
|
Комментарий. Что |
получилось? |
Процедура «всплытия |
кванторов», |
|
||||||||||||||||
позволяющая |
превратить |
произвольную |
секвенцию |
|
|
в |
предварённую, не |
|||||||||||||
является |
частью |
исчисления |
секвенций, но |
характер |
имеет |
вполне |
||||||||||||||
синтаксический. В рамках третьего формализма построение кванторной цепи |
||||||||||||||||||||
также |
является |
|
чисто |
|
|
|
синтаксической |
. |
процедуройНаконец, |
|||||||||||
пропозициональное |
поддерево – |
оно |
и |
есть |
|
пропозициональное, |
||||||||||||||
соответствующая теория разрешима. Странно, надо подумать… |
|
|
|
138
5. Теорема Крэйга-Линдона
Она же – интерполяционная теорема. Любопытно, что её формулировка
интуитивно сравнительно прозрачна, однако она не имеет (не имела в 1966 J)
синтаксического |
|
доказательства, |
принципиально |
отличающегося |
от |
|||||||||
приведённого ниже. |
|
|
|
|
|
|
|
|
|
|
||||
|
Теорема 14.3. (Крэйг, Линдон) Пусть формулы р и q таковы, что |
p > q . |
||||||||||||
Тогда существует формулаm, |
содержащая только символы отношений, |
|||||||||||||
входящие как в р, так и в q, такая, что p > m > q . |
|
|
|
|
|
|||||||||
|
Доказательство. |
Сначала |
рассмотрим |
случай бескванторных и |
q. |
|||||||||
Поскольку речь идёт о семантике, можно (заменив, если необходимо, формулы |
||||||||||||||
на эквивалентные) считать, что формула р записана в виде ДНФ: |
p =V L pi, j , |
|||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
i |
j |
|
где pi, j |
– |
простые |
формулы, |
то есть либо атомарные, либо |
отрицания |
|||||||||
атомарных. |
Чуть |
посложнее, но |
столь |
же |
очевидно, что |
формулу q |
можно |
|||||||
записать в виде q = Ør , где r =V Lri, j |
– тоже ДНФ. |
|
|
|
|
|
||||||||
|
|
|
|
|
i |
j |
|
|
|
|
|
|
|
|
|
Положим m = V L¢ pi, j , где m получается изр |
удалением всех |
простых |
|||||||||||
|
|
|
|
i |
j |
|
|
|
|
|
|
|
|
|
подформул, содержащих символы отношений, |
не входящие в р или в q. Ясно, |
|||||||||||||
что |
p > m , так что осталось доказать только m > q . |
|
|
|
|
|
||||||||
|
Так |
как p > Ør , |
то p, r > O . Следовательно, |
любые |
две конъюнкции, |
|||||||||
входящие в р и r |
несовместны: "i, "h L pi, j , L rh,k > O . Это возможно, |
только |
||||||||||||
|
|
|
|
|
|
|
|
j |
k |
|
|
|
|
|
если "i, "h |
$j, $k : pi, j , rh,k > O . Вспоминая, что формулы pi, j и rh,k |
– простые, |
||||||||||||
заключаем, что они должны содержать один и тот же символ отношения, |
||||||||||||||
поэтому |
|
pi, j |
присутствует |
|
в |
формулеm. |
Следовательно, |
"i, "h |
||||||
L¢ pi, j , Lrh,k |
> O , откуда m, r > O , или, что то же самое, m > q . |
|
|
|
||||||||||
j |
k |
|
|
|
|
|
|
|
|
|
|
|
|
|
Перейдём к общему случаю (с кванторами).
|
|
139 |
|
Лемма 14.4. Пусть секвенция S ¢ a T ¢ выводима из секвенции S a T при |
|||
помощи одних только кванторных правил, m – произвольная формула. Тогда |
|||
найдётся формула m¢, |
такая, |
что секвенция S ¢ a m¢ выводима из секвенции |
|
S a m при помощи |
одних |
¢ |
¢ |
только кванторных правил и секвенцияm a T |
|
||
выводима из секвенции m a T при помощи одних только кванторных правил. |
|
||
Доказательство. |
Индукция по длине выводаS ¢ a T ¢ из S a T . База и |
||
одновременно переход – случай, когда длина вывода равна 1 (в более сложном |
случае можно пробежаться по всей цепочке). В отсутствие сложностей со
вхождением переменной, по которой применяется |
кванторное |
правило в |
||||||||||||||||||||||||||||||
формулу m для |
выводов |
S a m |
|
и |
|
m a T |
|
можно |
применить |
то |
же |
самое |
||||||||||||||||||||
S¢ a m |
|
m a T ¢ |
||||||||||||||||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||||||||
правило, что применяется в выводе |
|
S a T |
. Точнее – в одном случае правило |
|||||||||||||||||||||||||||||
|
S¢ a T ¢ |
|||||||||||||||||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||
будет |
тривиальное J. |
Следовательно, |
в |
|
|
таких |
ситуацияхm = m¢ |
и |
||||||||||||||||||||||||
доказываемое утверждение тривиально. Поэтому |
достаточно |
|
рассмотреть |
|||||||||||||||||||||||||||||
случай, |
когда |
рассматривается |
правило(А+) |
или |
(Е–) |
по |
переменной x, |
|||||||||||||||||||||||||
входящей в формулу m = m(x). |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|||||||||||||
|
|
В |
случае, |
например, |
если |
речь |
идёт |
|
о |
правиле(А+), T =U , p(x), и |
||||||||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
S a U , |
p(x) |
|
|
|
|
|
случаеm |
¢ |
= Aw m(w). |
||||||||||||
рассматриваемый вывод |
есть S a U , Aup(u ). |
В |
этом |
|||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||
Действительно, вывод |
S a m(x) |
|
|
|
при помощи правила (А+) законен, так как |
|||||||||||||||||||||||||||
S a Awm(w ) |
||||||||||||||||||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|||||||||
переменная |
x |
не |
входит |
свободно S. |
|
вС |
другой |
стороны, вывод |
||||||||||||||||||||||||
|
|
m(x)a U , p(x) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|||||
|
|
Aw m(w )aU , p(x ) |
|
состоит из |
|
|
|
правила(А–), |
которому всё |
равно и |
уже |
|||||||||||||||||||||
|
Aw m(w )aU , Aup(u ) |
|
|
|
||||||||||||||||||||||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||||||||
законного |
правила (А+), |
применяемого |
|
|
|
после |
того, как |
«неудобную» |
переменную х обобщили и заменили на w J. С правилом (Е–) можно обойтись аналогично.
QED
|
|
|
140 |
|
|
|
|
Теперь завершим доказательство теоремы14.3. Пусть |
p > q . |
Тогда |
|||
секвенция p a q общезначимая и можно считать что предварённая секвенция. |
||||||
По |
теорема |
Эрбрана-Генцена |
существует |
вывод |
этой |
секвенции |
общезначимой |
предварённой бескванторной секвенцииS a T |
при |
помощи |
одних только кванторных правил. Теорема для бескванторных формул уже доказана, поэтому существует такая формула m, что секвенции S a m и m a T
общезначимы, то есть L si |
> m и m >V t j , где S = (s1, ..., sk ), T = (t1, ..., tl ). По |
|
i |
|
j |
лемме 14.4. существует |
формула m¢, такая, что секвенции p a m¢ и m¢ a q |
выводятся, соответственно, из секвенций S a m и m a T при помощи одних только кванторных правил. Следовательно, секвенции p a m¢ и m¢ a q также общезначимы. Общезначимость этих секвенций означает, что p > m¢ и m¢ > q .
При этом кванторные правила, естественно, не меняют списка символов отношений. Поэтому отношения, входящие в S, входят и в р, а входящие в Т –
входят и в q. Следовательно, в m входят только символы отношений, которые входят и в р и в q, и в m¢входят в точности те же самые символы отношений.
QED