И.А. Пушкарев логика

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 ) в качестве

переменной х будем брать в качестве новой переменной всегда первую ещё не

секвенцией, которая аксиомой не является(тогда контрпример найден и секвенция не общезначима), либо результатом применения однозначно определённого правила вывода из одной или двух секвенций, которые и являются детьми этой вершины (вершинами первого уровня). Вершины первого уровня можно рассмотреть по той же схеме(аксиому можно дальше не рассматривать, оборвав ветку), получив, возможно, несколько вершин второго уровня и т.д. Вот теперь действительно всё: дерево вывода однозначно строится для любой исходной секвенции.

По построению, листом построенного дерева может служить только аксиома или простая секвенция.

133

Для атомарных формул это утверждение верно по определению.

простые формулы из секвенций никуда пропасть не могут, найдётся вершина цепочки, в секвенцию, соответствующую которой входятр и q. Но тогда эта секвенция есть аксиома, что противоречит бесконечности цепочки.

Пусть формула р – не простая, но и не имеет вида Eu q(u ) (формулы вида

Au q(u ) тоже рассматриваются в этом пункте!). Формула р входит в некоторую секвенцию, которая не является ни простой секвенцией, – вершину цепочки, в

самым, в построенной интерпретации все формулы, входящие в исходную секвенцию, ложны, и она не является общезначимой.

Получилась теорема адекватности для исчисления секвенций.

Теорема 14.1. Секвенция является теоремой тогда и только тогда, когда она общезначима.

QED

Замечание. Однозначность построения дерева не означает разрешимости проблемы общезначимости: если дерево ещё не достроилось, то невозможно узнать, будет ли оно конечно.

134

4. Теорема Эрбрана-Генцена

Тот факт, что, вообще говоря, невозможно узнать, конечно ли дерево вывода, не означает, что это невозможно узнать для любой секвенции(это и есть определение словосочетания «вообще говоря» J). Иногда как раз можно.

Определение 14.1. Секвенция называется предварённой, если все формулы, входящие в неё являются предварёнными(т.е. все кванторы в них находятся спереди, например, подойдут формулы, записанные как ПНФ).

Не будем незаслуженно упрощать себе жизнь. Естественно выглядит

первый формализм, а пользоваться при доказательстве теорем удобно вторым или третьим. Однако формально понятия предварённых секвенций в первом формализме и во втором и третьем друг другу не соответствуют: при переносе предварённой формулы слева направо, перед ней возникает отрицание, которое лишает её предварённой формы.

Однако эта трудность не является принципиальной. Для формулы Øs

символом *s обозначим формулу, которая из неё получается, если

«протащить» в Øs отрицание сквозь кванторы, последовательно заменяя Ø А

на Е Ø и, симметрично, ØЕ на АØ . Тогда предварённой «секвенции первого формализма» С = s1 ,..., sm ® t1 ,..., tn семантически эквивалентна предварённая

формулам вида *si семантически равносильны применениям правил (Е–) и (А–

) соответственно для выводаS из Р. Тем самым, хотя классы предварённых секвенций для первого и третьего формализмов друг другу не соответствуют,

135

Теорема 14.2. (Генцен) Для любой общезначимой предварённой секвенции S существует такая бескванторная общезначимая секвенция Р, что S

выводима из Р посредством только «кванторных» правил (А+), (А–), (Е+) и (Е–

).

Доказательство. Рассуждаем в терминах третьего формализма. Во-

первых, забудем о правилах (А*–) и (Е*–), которыми всё равно не собираемся пользоваться (о чём и рассуждали перед формулировкой теоремы). Во-вторых,

T

добавим к правилам вывода«правило забывания» (Х): . Этому правилу

T , U

соответствует принцип: при увеличении секвенции множество контрпримеров к ней увеличивается. Поэтому если трудно построить контрпример к большой секвенции, давайте построим к меньшей, большой он тоже сгодится J. Правда,

если контрпример к меньшей так и не построился, это не значит, что к большой его построить нельзя… Это правило позволяет нам (теоретически) «проскочить через аксиому, её не заметив», позабыв одну из двух противоположных формул, содержащихся в секвенции, но ведь оно не требует это обязательно делать! Зато теперь можно считать, что все аксиомы имеют вид (p, Ø p).

Пусть теперь S – общезначимая предварённая секвенция третьего формализма. По теореме адекватности из этого следует, что она имеет доказательство D (конечное дерево). Предположим, что нам удалось привести доказательство к виду, в котором правила (А+) и (Е+) применяются в самом конце, точнее – любое применение остальных («пропозициональных») правил вывода находится в этом дереве выше любого применения этих«кванторных» правил. Тем самым, дерево доказательства делится на «кванторное» поддерево,

и «пропозициональные» поддеревья, растущие из его листьев. Покажем, что в этом случае теорема доказана.

Заметим, что применения правил (А+) и (Е+) соответствуют вершинам, у

которых ровно один сын, поэтому кванторное поддерево представляет собой цепь, а пропозициональное дерево получается ровно одно, и растёт оно из основания этой цепи. Далее, эти правила сами по себе не позволяют вывести

пропозиционального, если оно изначально находится над ним в дереве доказательства. Не умаляя общности, будем рассматривать пропозициональное правило «правилом с двумя посылками»:

T , q1 ; T , q2 .

T , q

В ином случае можно считать, что посылки совпадают: q1 = q2 .

Далее, не умаляя общности, будем считать, что левая посылка этого правила получена как результат применения кванторного правила, то есть в целом картина выглядит так:

где Q – один (любой) из двух имеющихся в наличии кванторов.

Если вверху применяется правило(А+), то переменная x не должна входить как в q1 , так и ни в одну формулу набора U.

138

5. Теорема Крэйга-Линдона

Она же – интерполяционная теорема. Любопытно, что её формулировка

интуитивно сравнительно прозрачна, однако она не имеет (не имела в 1966 J)

Перейдём к общему случаю (с кванторами).

случае можно пробежаться по всей цепочке). В отсутствие сложностей со

переменную х обобщили и заменили на w J. С правилом (Е–) можно обойтись аналогично.

QED

одних только кванторных правил. Теорема для бескванторных формул уже доказана, поэтому существует такая формула m, что секвенции S a m и m a T

выводятся, соответственно, из секвенций S a m и m a T при помощи одних только кванторных правил. Следовательно, секвенции p a m¢ и m¢ a q также общезначимы. Общезначимость этих секвенций означает, что p > m¢ и m¢ > q .

При этом кванторные правила, естественно, не меняют списка символов отношений. Поэтому отношения, входящие в S, входят и в р, а входящие в Т –

входят и в q. Следовательно, в m входят только символы отношений, которые входят и в р и в q, и в m¢входят в точности те же самые символы отношений.

QED