Об устранимости аксиомы индукции
( About eliminating of induction axiom
Preprint, Inst. Appl. Math., the Russian Academy of Science)

Введение. Рассматривается формальная арифметика S, содержащая константу 0, числовые переменные, равенство, функциональные символы + (сложения), × (умножения) и ¢ (прибавления 1) и логические связки. Термы строятся из константы 0 и переменных с помощью функциональных символов.  В  частности,  натуральные  числа изображаются термами  вида

0¢¢ ^… ¢. Атомарные формулы – это равенства термов; остальные формулы строятся с помощью логических связок и кванторов.

Исчисление базируется на классическом исчислении предикатов и включает  следующие дополнительные аксиомы: x¢ = y¢ É x = y; Ø( x¢ = 0); x = y É .x = z É y = z; x = y É x¢ = y¢; x + 0 = x; x + y¢ = (x = y)¢; x 0 = 0; x y = (x y) + x и схему индукции (АИ): A(0) É ."x(A(x) É A(x¢) É "xA(x). Логическое исчисление первого порядка выглядит не совсем обычно, что объясняется требованием выделить характерные свойства выводов, которые позволяют сформулировать основной результат работы, состоящий в том, что при доказательстве фундаментальных формул (т.е. формул без переменных) можно обойтись без АИ.

Формулы первого порядка строятся над базисом  É, f, ". Для наглядности, формулы вида X₁ É .X₂ É . ... É .X_n É X,  n ³ 0 представляются  в  виде Г ® Х, используя знак ® в качестве многоместной импликации. При этом порядок посылок Г = {X₁, X₂, ..., X_n} несущественен.

Единственная  аксиомная  схема  логического  исчисления  имеет вид: Х É Х. При этом формула Х  называется заключением аксиомы. Правила исчисления следующие:

обобщенное правило modus ponens

Г₁ ® .Х É Y       Г₂ ®  Х       (здесь Г = Г₁ È Г₂)

           Г ®  Y

снятие двойного отрицания

    Г ® .(Х É f) É f

         Г ®  X

положительное кванторное правило

     Г ® Х(a)                 (переменная а не входит в Г) 

   Г ® "xX(x)

отрицательное кванторное правило

     Г ® .(D® "yХ(y)) É. (D® Х(t)) É  Y         (t - произвольный терм)

               Г ® . (D®"yХ(y)) É  Y

Достаточно просто показать, что это исчисление совпадает с классическим.

1. Определение синтаксического дерева. Определим более компактную форму вывода в приведенном исчислении (т.н. синтаксическое дерево), что позволит установить ряд свойств выводов, которые трудно заметить при обычном определении.

Синтаксическим деревом (с.д.) D_U  для формулы U называется однокорневое, растущее вверх дерево, которое построено следующим образом:

1. Корню с.д. D_U  приписана формула U, висячим узлам - аксиомы, остальным узлам формулы, вид которых определяется типом узлов, которым они приписаны. В аксиоме Х É Х обе формулы Х называются двойственными.

2. Каждый  не висячий узел D_U  является либо В-узлом, либо З-узлом, либо положительным кванторным узлом, либо отрицательным кванторным узлом.

В-узлом называется следующая конструкция.

Самому В-узлу приписана формула Г ® .(Х₁É .Х₂É . ... É .Х_n É Х) É Х, а непосредственно выше расположены в точности n узлов, каждому из которых приписана  единственная  формула, полученная из Г ® .(Х₁ É .Х₂ É. ... .Х_n  É Х) É Х_i, i = 1, 2, ..., n отбрасыванием некоторых посылок. При этом для данного В-узла формула Х называется изменяемой, а Х₁É .Х₂É. ... .Х_n É Х - используемой. Два вхождения формулы Х – заключение используемой формулы и изменяемая формула, называются двойственными.

З-узлом называется следующая конструкция.

Самому З-узлу приписана формула Г ® Х, а непосредственно выше расположен в точности один узел, которому приписана формула, полученная выбрасыванием некоторых посылок из Г ® .(Х É f) É f. При этом формула Х называется запоминаемой.

Положительным кванторным узлом (обозначается "⁺) называется следующая конструкция.

Самому "⁺-узлу приписана формула Г ® "xX(x), а непосредственно выше расположен единственный узел, которому приписана формула, полученная из Г ® Х(a) выбрасыванием некоторого числа ее посылок. При этом переменная а (собственная переменная этого узла) не входит в Г. 

Отрицательным кванторным узлом (обозначается "^-) называется следующая конструкция.

Самому "^--узлу приписана формула Г ® .(D®"yХ(y)) É  Y, а непосредственно выше расположен единственный узел, которому приписана формула, полученная из формулы 

Г ® .(D® "yХ(y)) É. (D® Х(t)) É Y

выбрасыванием некоторого числа посылок. При этом терм t называется собственным для этого узла.

Будем представлять синтаксические деревья в виде, который обычно принят при изображении выводов в виде деревьев. Так, если формулы А₁, А₂, …, А_n располагаются непосредственно выше формулы В, то будем представлять это так:

А₁, А₂, …, А_n

В

Справедлива

Теорема 1.1. Формула U общезначима тогда и только тогда, когда для нее существует с.д. D_U.

Доказательство следует из сопоставления узлов с.д. и приведенных правил вывода.

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

Лемма 2.1. Всякое с.д. может быть преобразовано в такое, в котором формулы запоминаемые, изменяемые и заключительные в аксиомах суть атомарные.

Доказательство. Пусть D_U есть с.д., в котором В-узлу N приписана формула

V = Г ® .(Х₁É .Х₂É . ... É .Х_n É Х) É Х,

Х = A₁ É .A₂ É. ... .A_m  É B есть изменяемая формула и главная связка формулы B не импликация. Заменим этот узел следующим. Ему приписана та же формула, используемая формула остается прежней, а изменяемой формулой является B. В результате, непосредственно выше к присутствующим узлам добавляются m новых, которым приписаны аксиомы A_i É A_i, i = 1, 2, …, m. Последние возникают из того, что как в самой формуле V имеются посылки A_i, так и в изменяемой формуле присутствуют те же посылки. Следовательно, после замены исходного В-узла на новый, получим с.д. формулы U.

Пусть теперь в с.д. D_U В-узлу N приписана формула

V = Г ® .(Х₁É .Х₂É . ... É .Х_n É "xХ(x)) É "xХ(x),

и a – это индивидная переменная, которая не встречается в этом с.д.  Заменим В-узел N следующими тремя узлами. Сам узел N превращается в "⁺-узел с собственной переменной a. Непосредственно выше располагается "^--узел с собственным термом a. Наконец, третьим узлом является В-узел с изменяемой формулой Х(a) и используемой Х₁É .Х₂É . ... É .Х_n É Х(a). Очевидно, что такое преобразование превращает исходное с.д. в новое с.д. для формулы U.

Легко увидеть, что, используя подобные преобразования, каждое с.д. можно привести к такому с.д., в котором изменяемые формулы В-узлов суть атомарные.

Доказательство леммы для двойственных формул аксиом и запоминаемых формул осуществляется по аналогичной схеме.

Лемма доказана.

Лемма 2.2. Всякое с.д. может быть преобразовано к следующему виду: если некоторая посылка какой-либо формулы выступает в качестве используемого выражения в В-узле, то нигде выше эта формула не используемая в другом В-узле.

Доказательство. Пусть некоторому В-узлу N с.д. D_U  приписана формула

V = Г ® .(Х₁É .Х₂É . ... É .Х_n É Х) É Х,

и его используемая формула Х₁É .Х₂É . ... É .Х_n É Х также используется выше в В-узле N₁, которому приписана формула

V₁ = Г₁ ® .(Х₁É .Х₂É . ... É .Х_n É Х) É Х.

В силу леммы 2.1 полагаем, что Х есть атомарная формула. Непосредственно выше N расположены n узлов N¹, N², …, Nⁿ, которым приписаны формулы соответственно D₁ ® X₁, D₂ ® X₂, …, D_n ® X_n. Пусть узел N₁ расположен выше узла Nⁱ, i Î {1, 2, …, n} и непосредственно выше узла N₁ расположены n узлов N₁¹, N₁², …, N₁ⁿ с приписанными формулами соответственно Q₁ ® X₁, Q₂ ® X₂, …, Q_n ® X_n.

Превратим узел Nⁱ в З-узел с запоминаемой формулой X_i. В результате появится новая посылка X_i É f. Теперь нетрудно увидеть, что можно построить с.д., в котором эта посылка будет встречаться везде выше узла Nⁱ вплоть до узла N₁, который мы заменяем следующим образом. Если Х есть константа f, то N₁ становится В-узлом с используемой формулой X_i É f. Если X есть атомарная формула, отличная от константы, то этот узел превращается в З-узел N₁¢, выше которого расположен В-узел N₁² с приписанной формулой

Г₁ ® .(Х₁É .Х₂É . ... É .Х_n É Х) É .X_i É f É. ХÉ f É f.

и используемой формулой X_i É f. В результате получается импликация с заключением X_i, посылки которой включают все посылки формулы V₁.

Из этих преобразований очевидно, как построить с.д. выше этой формулы, основываясь на исходном с.д.

Лемма доказана.

Лемма 2.3. Всякое с.д. может быть преобразовано к следующему виду: если в последнем "^--узел с собственным термом t расположен ниже "⁺-узла с собственной переменной а, то терм t не содержит переменной а.

Доказательство. Пусть в с.д. D_U "^--узел N с собственным термом t(a) расположен ниже "⁺-узла N₁ с собственной переменной a. По определению "⁺-узла формула, приписанная узлу N₁ не содержит переменной a. Поэтому заменим в поддереве с корнем N₁ все вхождения переменной a на новую переменную b, не встречающуюся в исходном с.д. В результате получим новое с.д. для формулы U. Проделав подобные преобразования со всем с.д. получим искомое с.д.

Лемма доказана.

Следствие 1. Если формула U не содержит свободных переменных, и в с.д. D_U "^--узел с собственным термом t расположен ниже любого "⁺-узла, то терм t фундаментальный (т.е. не содержит переменных).

Следствие 2. Если формула U не содержит положительных кванторов, то в с.д. D_U  все собственные термы "^--узлов фундаментальные.

На множестве термов с.д. введем частичный порядок: будем говорить, что некоторый терм зависит от собственной переменной положительного кванторного узла, если он ее содержит. Если терм есть собственный терм отрицательного кванторного узла, то будем говорить о зависимости между кванторными узлами: назовем "^--узел зависимым от "⁺-узла с собственной переменной а, если собственный терм "^--узла содержит а.

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

Лемма 2.4. Всякое с.д. может быть преобразовано к следующему виду: все собственные переменные положительных кванторных правил попарно различны, и собственная переменная любого "⁺-узла встречается лишь в поддереве с корнем в этом "⁺-узле.

Доказательство следует из того, что если N есть "⁺-узел с собственной переменной a, то a не входит в формулу, приписанную этому  узлу. Поэтому, заменив везде в поддереве с корнем N переменную a на новую переменную, которая не встречается в исходном с.д., получим также с.д. для исходной формулы.

Лемма доказана.

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

Доказательство. Все "⁺-узлы с.д. имеют различные собственные переменные, которые встречаются только выше этих узлов. Поэтому, если собственная переменная a "⁺-узла N входит в собственный терм t(a) "^--узла N₁, то N располагается ниже N₁.

Следствие доказано.

Замечание. Обратное, в общем случае, неверно. Собственный терм отрицательного кванторного узла может не зависеть от положительного кванторного узла, выше которого он располагается.

Из последних рассуждений вытекает, что для замкнутой формулы U в с.д. D_U собственные термы отрицательных кванторных узлов суть суперпозиции функциональных символов и собственных переменных положительных кванторных узлов. При этом суперпозиция определяется видом двойственных выражений, т.к. в этом случае требуется полное совпадение двух формул, что предполагает совпадение соответствующих термов. Из определения с.д. видно, что глубина суперпозиции, главным образом, определяется числом В-узлов, которые встречаются в одной ветви с.д.

Нас интересует возможность вхождения в один собственный терм отрицательного кванторного узла собственных переменных положительных кванторных узлов.

Введем следующие определения.

Пусть N₁ и N₂ – два положительных кванторных узла, элиминирующие кванторы, соответственно, "x и "y. Тогда эти узлы зависимы, если один из этих кванторов в выводимой формуле управляет другим. В противном случае узлы независимые.

Пусть в с.д. D_U каждый положительный кванторный узел имеет свою уникальную собственную переменную, и N₁ и N₂ – два независимых положительных кванторных узла, устраняющие кванторы соответственно "x и "y, причем узел N₂ расположен выше N₁, и собственными переменными узлов N₁ и N₂ являются соответственно a и b. При устранении квантора "x узлом N₁ могут появиться термы лишь вида t₁(a), а узлом N₂ - вида t₂(b). Но не могут появиться  термы, зависящие сразу от двух переменных a и b, так как кванторы "x и "y не зависимы. И поэтому после появления собственной переменной a, порожденной узлом N₁, она никак не может встречаться в подформуле, начинающейся с квантора "y. Покажем, что в этом случае можно ограничиться рассмотрением лишь с.д., в которых отсутствуют термы вида t(a, b).

Справедлива

Теорема 2.5. Всякое с.д. можно преобразовать так, что собственные термы любого отрицательного кванторного узла не зависят ни от каких двух независимых положительных кванторных узлов.

Доказательство. Пусть в с.д. N есть отрицательный кванторный узел с собственным термом t(a,b), где a и b суть собственные переменные независимых положительных кванторных узлов. Если терм t(a,b) не встречается в двойственных формулах, то собственный терм узла N можно заменить на терм t(a,а), не содержащий переменную b. Легко увидеть, что при такой замене мы вновь получим с.д.

В противном случае в с.д. встречаются двойственные пары, включающие терм t(a,b). Если оба соответствующие терма каждой такой двойственной пары суть собственные термы узла N, то их также можно заменить на терм t(a,а), не содержащий переменную b. Легко увидеть, что при такой замене вновь получим с.д.

Если в с.д. встречается двойственная пара X(t(a,b)), X(t(a,b)) и в одной из этих формул (пусть первой) терм t(a,b) является собственным для узла N, а во второй – нет, то рассмотрим предшественников этого терма во второй формуле. По условию a и b суть собственные переменные независимых положительных кванторных узлов. Поэтому рассматриваемый терм t(a,b) в с.д. мог возникнуть лишь как собственный терм некоторого отрицательного кванторного узла. Но тогда, выделив все такие отрицательные кванторные узлы, в которых t(a,b) есть собственный терм, можно везде в них заменить t(a,b) на t(a,а), не содержащий переменную b. Легко увидеть, что при такой замене вновь получим с.д.

Разобраны все случаи. Теорема доказана.

Следствие. Собственный терм отрицательного кванторного узла может зависеть от двух различных собственных переменных положительных кванторных узлов лишь, когда один из этих кванторов управляет другим.

Лемма 2.6. Всякое с.д. может быть преобразовано к следующему виду: если его некоторому узлу приписана формула Г ® "xX(x), то это "⁺-узел.

Доказательство. Пусть узлу N с.д. приписана формула Г ® "xX(x), и этот узел не является "⁺-узлом. По лемме 2.1 этот узел может быть лишь "^--узлом с собственным термом t. Этот терм не содержит собственной переменной a того "⁺-узла, в котором снимается квантор "x. Следовательно, если переставить эти узлы, то также получится с.д. Проделав подобные преобразования со всем с.д. получим искомое с.д.

Лемма доказана.

Следствие. Если в с.д. имеется "⁺-узел, котором приписана формула Г ® "xX(x), то выводима любая формула Г ® Х(t), где t - произвольный терм. При этом с.д. для формулы Г ® Х(t) получается из поддерева с корнем в узле, расположенном непосредственно выше "⁺-узла, простой заменой собственной переменной  указанного "⁺-узла на терм t.

Таким образом, с.д. для формулы Г ® Х(t) не содержит новых дополнительных термов, по сравнению с с.д. для формулы Г ® "xX(x), за исключением t.

Следствие (аналог теоремы о средней формуле). Пусть U есть формула, в которой каждая посылка и заключение находятся в предваренной форме. Тогда существует с.д. D_U, в котором присутствует формула, ниже которой расположены лишь кванторные узлы, а выше лишь В-узлы и З-узлы. (Эта формула называется средней для с.д. D_U).

3. Преобразования синтаксических деревьев. В этом разделе опишем схемы преобразований синтаксических деревьев, которые позволяют получить новые с.д. Это позволит в дальнейшем получать с.д. с определенными  свойствами.

Лемма 3.1. Пусть

U₁ = Г₁ ®. Х É Y, U₂ = Г₂ ® Х, U = Г ® Y, где Г = Г₁ È Г₂

и D_U1, D_U2 суть с.д. Тогда существует с.д. D_U, полученное перестройкой двух предыдущих конечным числом локальных преобразований. (Обозначим перестройку указанных с.д. в искомое с.д. через Г₁ ®.Х É Y  +   Г₂ ® Х.)

Доказательство состоит в том, что приводится система схем преобразований с.д., которая позволяет с.д. D_U1, D_U2 преобразовать в искомое. Полнота системы вытекает из того, что осуществляется разбор всех случаев, которые могут встречаться в результате подобной перестройки. Смысл преобразований легко понять из их вида. Эти преобразования аналогичны преобразованиям секвенциальных выводов при устранении правила сечения. 

1.  Х É Х     +     D ® Х          ~               D ® Х   

2.      

D₁₁ ®. Х É Y₁  ...   D_1h ®. Х É Y_h

         D₁ ®. Х É Y                              +        D₂ ®  Х                    ~

                      D₁₁ ®. Х É Y₁   +    D₂ ®  Х   ...   D_1h ®. Х É Y_h   +   D₂ ®  Х

                                                                 D ®  Y

где D = D₁₁ È ...  È D_1h È D₂.

3.     

D₁ ®.(Y₁  É ... É .Y_h É Х ) É Y₁ ... D₁ ®.(Y₁  É ... É .Y_h É Х ) É Y_h

        D₁ ®.(Y₁  É ... É .Y_h É Х ) É X                 

                                                 +    D₂ ®.Y₁ É...É.Y_h É Х         ~

D₂ ®.Y₁É...É.Y_hÉХ + {D₁ ®.(Y₁ É... É.Y_hÉХ)ÉY₁  ...  D₁®.(Y₁É...É.Y_hÉХ)ÉY_h}

                                               D ® X

где D = D₁ È D₂.

4.     

D₁ ®.(Q ®  "xХ(x)) É . (Q ® Х(t) ) É Y

   D₁ ® .(Q ®  "xХ(x)) É Y                          +        D₂ ® .Q ® "xХ(x)           ~   

D₁®.(Q®"xХ(x)) É. (Q ® Х(t)) É Y  + {D₂ ® .Q ® "xХ(x), D₂ ® .Q ® Х(t)}  

                                                    D ® Y

где D = D₁ È D₂. Здесь с.д. для формулы D₂ ® .Q ® Х(t) получается   из  с.д. для формулы D₂ ® .Q ® "xХ(x), т.к. самым нижним узлом последнего является положительный кванторный, которому предшествует с.д. для формулы D₂ ®. Q ® Х(с). Такое с.д. легко перестроить в искомое, устранив нижний положительный кванторный узел и заменив его собственную переменную с на терм t.

Разобраны все случаи. Лемма доказана.

4. Некоторые свойства арифметических термов. Числом n называется терм 0²^...¢, содержащий n штрихов. Говорим, что фундаментальный терм равен числу, если они равны в стандартной арифметической модели.

В последующих рассуждениях мы обозначим Е совокупность четырех формул: правило подстановки: x = y É t(x) = t(y), аксиомы рефлексивности: х = х, коммутативности: х = у É y =  x и транзитивности: х = у É .y = z É x = z.

Глубина арифметического терма t, обозначается d(t), вычисляется следующим образом.

1.     Если t есть переменная или константа 0, то d(t) = 0.

2.     Если t = (t₁)¢, то d(t) = d(t₁) +1.

3.     Если t = t₁ + t₂ или t = t₁ t₂ то d(t) = max{d(t₁), d(t₂)} +1.

Лемма 4.1. Если терм t равен числу n, то равенство t = n выводимо из Е без АИ.

Доказательство индукцией по глубине терма t.

Базис индукции. Терм t есть константа 0. Тогда равенство 0 = 0 элементарно следует из аксиомы рефлексивности.

Индукционный переход. Разберем все возможные случаи для внешнего функционального символа терма t.

Если это символ ¢, то случай легко сводится к индукционной гипотезе, используя аксиому x = y É x¢ = y¢.

Допустим, что t имеет вид t₁ + t₂, и по индукционной гипотезе равенства t₁  =  n₁ и t₂ =  n₂ доказуемы без использования АИ.

В силу рефлексивности имеем t = t₁ + t₂. Далее, используя два раза правило подстановки с посылками t₁  = n₁ и t₂ = n₂, получаем t =  n₁ + n₂. Затем, используя n₂ раз аксиому x + y¢ = (x + y)¢, и единственный раз  аксиому x + 0 = x, получаем равенство t =  n.

Случай, когда t имеет вид t₁ × t₂, разбирается аналогично с использованием аксиом x × y¢ = (x × y) + у и x × 0 = 0.

Разобраны все случаи. Лемма доказана.

Лемма 4.2. Если А есть арифметическая формула, терм t равен числу n, то импликации А(t) É А(n) и А(n) É А(t) выводимы в исчислении первого порядка из E и равенства t = n.

Доказательство. Структуры формул А(t) и А(n) подобны. Поэтому для каждой из приведенных импликаций можно построить конструкцию наподобие с.д., висячими узлами которой служат либо аксиомы вида Х É Х, либо выражения вида:

а) t = х É n = х;

б) х = t  É х = n,

в) n = х É t = х;

г) х = n É х = t.

В каждом из этих выражений в точности одно вхождение переменной х есть собственная переменная некоторого положительного кванторного правила, а другое – отрицательного. Любое из них выводимо в исчислении первого порядка из посылок E и t = n.

Лемма доказана.

Следствие 1. Если А есть арифметическая формула, терм t равен n, то для формул Е ®. t = n É .А(t) É А(n) и Е ® .t = n É .А(n) É А(t) существуют с.д., множества термов которых содержат помимо индивидных переменных лишь термы собственно формулы А и пару термов t и n.

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

Следствие 2. Если А есть арифметическая формула, терм t равен n, и имеется с.д. для формулы А(n) (А(t)), то для формулы Е ® .t = n É А(t)  (Е ®. t = n  É А(n)) существует с.д., множество термов которого содержит помимо индивидных переменных лишь термы с.д. для формулы А(n) (А(t)), термы  формулы А и пару термов t и n .

5. Некоторые свойства арифметических выводов. Пусть фундаментальная формула R выводима в арифметике. Тогда имеется с.д. D_U для формулы U, которая имеет вид Â ® R, где Â есть совокупность арифметических аксиом. В силу конечности с.д. D_U  уместно допустить, что оно содержит конечное число различных термов. Определим на множестве термов этого с.д. частичный порядок, как это определено в разд.2. Этот порядок индуцирует следующий частичный порядок на множестве АИ, используемых в с.д.

Пусть посылка вида А(0) É ."x(А(х) É А(х¢)) É А(t) есть пример АИ, полученный в результате отрицательного кванторного узла, причем терм t содержит переменную с, которая является собственной для расположенного ниже положительного кванторного узла вида

Г ® В(с) É В(с¢))

Г ® "x(В(х) É В(х¢))

и заключение "x(В(х) É В(х¢)) появилось в результате использования ниже в В-узле примера АИ В(0) É ."x(В(х) É В(х¢)) É В(t₁). (Это пояснено на рис.5.1.) Согласно ранее введенного частичного порядка терм t  зависит от переменной с. Будем говорить, что в этом случае пример В(0) É ."x(В(х) É В(х¢)) É В(t₁) предшествует примеру А(0) É ."x(А(х) É А(х¢)) É А(t).

В силу Теоремы 2.6 всякий пример АИ может предшествовать нескольким примерам АИ, но одному примеру АИ предшествует не более одного примера АИ.

Изобразим отношение предшествования, определенное на множестве примеров АИ в любом с.д. в виде растущего вверх дерева зависимостей. Для простоты полагаем, что оно однокорневое и связное, его корень не помечен никак, а каждый оставшийся узел помечен единственным примером АИ. Очевидно, что каждый узел, расположенный непосредственно над корнем, помечен тем примером АИ, который не зависит ни от какого другого примера АИ.

Из преобразований разд.3 вытекает

Теорема 5.1. Всякое преобразование, описанное в разд.3, не приводит к появлению новых зависимостей между примерами АИ. Т.е. глубина дерева зависимостей результирующего с.д. не превосходит глубины дерева зависимостей исходного с.д.

Доказательство осуществляется простой проверкой каждого из преобразований. 

6. Устранение АИ из выводов фундаментальных формул. В этом разделе мы покажем, что вывод всякой фундаментальной арифметической формулы может быть получен без использования АИ, но с использованием правила подстановки.

Справедлива

Теорема 6.1. Пусть фундаментальная формула R выводима в системе S. Тогда существует ее вывод в S, в котором используется правило подстановки, но отсутствуют АИ.

Доказательство. Так как R выводима в арифметике, то в исчислении первого порядка выводима формула U вида Â ® R, где Â есть некоторая совокупность аксиом арифметики. Полагаем, что Â также содержит законы рефлексивности, коммутативности и транзитивности для равенства. Тем самым для этой формулы существует с.д. D_U. В силу конечности с.д. D_U  уместно допустить, что оно содержит конечное число различных термов.

Полагаем, что отношение предшествования, определенное на множестве примеров АИ в с.д. D_U представимо в виде растущего вверх дерева зависимостей. Дальнейшее доказательство состоит в том, что мы покажем, как перестроить исходный вывод, чтобы результирующий не включал АИ. Перестройка на каждом шаге приводит к уменьшению длины ветвей дерева зависимостей с одновременным увеличением его ширины. Поэтому доказательство проводим индукцией по числу различных примеров АИ, присутствующих в дереве зависимостей.

Базис индукции, когда в с.д. D_U нет примеров АИ, элементарен.

Индукционный шаг. Выделим в с.д. D_U  самый нижний В-узел N, в котором используемым выражением служит пример АИ. В этом случае фрагмент с.д. D_U  с узлом N в качестве корня имеет такой вид, как на рис.6.1.

                                                     .  .  .

                                                     Г ® .(А(0) É ."x(А(х) É А(х¢)) É А(t)) É D(t)

                                  Г ® .(А(0) É ."x(А(х) É А(х¢)) É А(t)) É "x(А(х) É А(х¢))

           Г ® .(А(0) É ."x(А(х) É А(х¢)) É А(t)) É А(0)

Г ® .(А(0) É ."x(А(х) É А(х¢)) É А(t)) É А*(t)

Рис. 6.1.

Здесь для простоты предполагается, что А(t) = D(t) É А*(t), где А*(t) – это атомарная фундаментальная формула, т.к. ниже рассматриваемого В-узла нет положительных кванторных узлов.

Обратим внимание на следующее.

1.     Поддеревья

D_{Г ® .(А(0) É ."x(А(х) É А(х¢)) É А(t)) É А(0)},

D_{Г ® .(А(0) É ."x(А(х) É А(х¢)) É А(t)) É "x(А(х) É А(х¢))} ,

D_{Г ® .(А(0) É ."x(А(х) É А(х¢)) É А(t)) É D(t)}

не содержат формулу (А(0) É ."x(А(х) É А(х¢)) É А(t)) в качестве используемой в каком-либо своем В-узле. Следовательно, эти поддеревья, простым вычеркиванием посылки (А(0) É ."x(А(х) É А(х¢)) É А(t)) во всех формулах превращаются в с.д. соответственно

D_{Г ® А(0)},

D_{Г ® "x(А(х) É А(х¢))} ,

D_{Г ® D(t)}

Дальнейшее доказательство состоит в том, что мы некоторым образом преобразовываем эти поддеревья. В итоге с.д.

D_{Г ®.(А(0) É ."x(А(х) É А(х¢)) É А(t)) É А*(t)}

будет преобразовано в с.д. D_{Г ® А*(t)}.

2. Так как R - фундаментальная формула, то между корнем исходного с.д. и узлом N нет положительных кванторных узлов. Следовательно, t есть фундаментальный терм, так как получается в результате суперпозиции собственных термов отрицательных кванторных узлов, ни одно из которых не зависит от положительного узла.

3. Из фундаментальности терма t вытекает, что он равен некоторому числу n, и равенство n = t доказуемо без АИ.

4. Из существования с.д. для формулы

Г ® "x(А(х) É А(х¢))

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

Г ®.А(с) É А(с¢)

Г ® "x(А(х) É А(х¢))

Рассматриваемый пример А(0) É."x(А(х) É А(х¢)) É А(t) АИ является тем, который приписан узлу дерева зависимостей, расположенному непосредственно над корнем. Следовательно, в с.д. D_U имеются h ³ 0 различных примеров АИ, которые зависят от выделенного. Каждый из них в собственном терме, полученном снятием отрицательного квантора, во-первых, содержит переменную с и, во-вторых, не содержит никакой другой собственной переменной, полученной в результате снятия положительного квантора, порожденного другим примером АИ.

5. Из выводимости формулы

Г ®.А(с) É А(с¢)

следует выводимость любой формулы

Г ® .А(i) É А(i¢),

где i - произвольное число. И с.д. для каждой такой формулы получается простой перестройкой с.д. для формулы

Г ® .А(с) É А(с¢).

После замены собственной переменной с на число i получаем с.д. для формулы

Г ®.А(i) É А(i¢),

которое не содержит пример А(0) É ."x(А(х) É А(х¢)) É А(t) АИ. Поэтому дерево зависимостей для с.д.

D_{Г ® .А(i) É А(i¢)}

имеет во всех своих ветвях на один ярус меньше, чем соответствующее поддерево дерева зависимостей для с.д.

D_{Г ® (А(0) É ."x(А(х) É А(х¢)) É А(t)) É .А(с) É А(с¢)}.

При этом в с.д.

D _{Г ® .А(i) É А(i¢)}

множество термов по сравнению с множеством термов в с.д.

D _{Г ® .(А(0) É ."x(А(х) É А(х¢)) É А(t)) É .А(с) É А(с¢)}

отличается в точности тем, что во всех термах переменная с заменена числом i, i = 0, 1, …, n.

6. Из этого вытекает существование первопорядкового вывода формулы

Г ® А(n)

из формул

Г ® А(0)

Г ® .А(0) É А(1),

...

Г ® .А(n-1) É А(n).

Этот вывод имеет вид, как на рис.6.2.

Г ® .А(0)É А(1)                  Г®А(0)

                                         Г ® .А(1)É А(2)                 Г® А(1)

.    .    .

Г ® .А(n-1)É А(n)                 Г® А(n-1)

                                                       Г ® А(n)

Рис. 6.2.

С.д. для каждой из формул

Г ® .А(0)É А(1)

Г ® .А(1)É А(2)

.    .    .

Г ® .А(n-1)É А(n)

определяет дерево зависимостей, которое совпадает с деревом зависимостей, определенного с.д. для формулы

Г ® .А(с) É А(с¢).

Дерево зависимостей, определяемое с.д. для формулы

Г® А(0),

такое же, как для соответствующего поддерева исходного с.д.

Поэтому дерево зависимостей, которое определяется выводом на рис.6.1 для формулы

Г® А(n)

шире, чем исходное, но оно имеет более короткие ветви в тех поддеревьях, которые имеют своими самым нижними узлами, узлы, помеченные выделенным примером АИ.

7. Формула

Е ® .t= n É .А(n) É А(t)

выводима в исчислении первого порядка, причем множество термов ее вывода, помимо переменных, которые служат собственными термами кванторных правил, и термов собственно формулы А, включает лишь два: t и n. Теперь, используя полученный вывод формулы

Г ® А(n),

получаем вывод формулы

Г ® .Е ® .t = n É А(t),

который содержит множество термов, состоящее из множества термов вывода формулы

Г ® А(n).

Для этого вывода дерево зависимостей совпадает с деревом зависимостей поддерева из п.6, т.к. вывод формулы

Е ® .t= n É .А(n) É А(t)

не содержит АИ.

8. Для дальнейшего доказательства полагаем, что D(t) есть формула. Тогда   по   Следствиям   из  леммы  4.2 следует,  выводимость  формулы  Е ® .t= n É .D(t) É D(n). Напомним, что А(t) = D(t) É А*(t), поэтому А(n) = D(n) É А*(n)  и  Г ® А(n) = Г ® .D(n) É А*(n).

9. Теперь вывод формулы Г ® . Е ® .t = n É А*(t) выглядит, как на рис. 6.3.

Е ® .t= n É .D(t) É D(n)   Г ® D(t),.

Г ® .D(n) É А*(n)     Г ® .Е ® .t= n É D(n)

Е ® .t= n É .А*(n) É А*(t)  Г ® .Е ® .t= n É А*(n)

                                      Г ® . Е ®t = n É А*(t)

Рис. 6.3.

Результирующий вывод определяет дерево зависимостей, которое выглядит как на рис.6.4.

                                             T₀    T₁    T₂   …   T_n    T_D   

                                                            Рис.6.4

Здесь T₀ – это дерево зависимостей, определяемое с.д. формулы

Г®А(0),

T_i ‑ это дерево зависимостей, определяемое результирующим выводом формулы

Г ® А(i),

i = 1, 2, …, n, T_D ‑ это дерево зависимостей, определяемое с.д. для формулы

Г ® D(t).

Как видно, каждая из посылок результирующего вывода имеет в заключении фундаментальную формулу, а дерево зависимостей содержит на один пример АИ меньше, чем дерево зависимостей исходного с.д. Следовательно, для результирующего вывода выполняется индукционная гипотеза.

Так как множество Г посылок включает аксиомы для равенства, то получаем, что если расширить множество посылок исходной формулы посылкой t = n, то получим с.д. для формулы Г ® .t = n É А*(t), которое не содержит выделенного примера АИ. Кроме того, исходный вывод перестраивается таким образом, что к нему применима индукционная гипотеза.

Тем самым, мы показали, что для формулы, получаемой из Â ® R за счет исключения всех АИ и добавления конечного множества t₁ = n₁, t₂ = n₂, ..., t_q = n_q посылок, где t₁, t₂, ..., t_q суть фундаментальные термы исходного вывода, и n₁, n₂, ...,  n_q - равные им числа, существует первопорядковый вывод. Но тогда формула R выводима без АИ лишь с правилом подстановки.

Теорема доказана.

Следствие. Система S непротиворечива.

Доказательство. Допустим противное. Тогда в S имеется вывод формулы R вида  0 = 1. Элиминируем АИ из доказательства формулы Â ® R. В итоге получится первопорядковый вывод формулы t₁ = n₁, t₂ = n₂, ..., t_q = n_q, Â^* ® R, где Â^* отличается от Â лишь отсутствием АИ. Из существования для этой формулы с.д. со средней секвенцией следует, что имеется пропозициональный вывод формулы t₁ = n₁, t₂ = n₂, ..., t_q = n_q, Â^** ® R, где Â^** есть совокупность фундаментальных примеров аксиом системы S за исключением АИ.

Но каждый из примеров этих аксиом, так же, как и равенства t₁ = n₁, t₂ = n₂, ..., t_q = n_q истины в стандартной интерпретации, а 0 = 1 - ложна. Противоречие.

Следствие доказано.