ИНФОРМАТИКА

УДК 510.64


А. А. Чубарян, О.Р. Болибекян

О секвенциальных системах слабых арифметик

(Представленно чл.-кор. НАН РА И. Д. Заславским 26/V 2002)

     Известно, что при автоматическом поиске доказательства теорем предпочтительнее работать с секвенциальными системами. В настоящее время существует множество таких систем. Однако авторам настоящей работы не удалось найти в имеющейся литературе секвенциального аналога минимального исчисления. В данной статье определяется секвенциальный аналог исчисления минимальной арифметики Робинсона гильбертовского типа. Учитывая то обстоятельство, что доказательства без сечений обладают более простой стратегией поиска выводов, в работе также определяется исчисление минимальной арифметики Робинсона без правила сечения.
    Далее мы будем придерживаться общепринятых определений переменной, терма, формулы, секвенции и подстановки, введенных в [1].
    Приведем список схем аксиом, собственных аксиом и правил вывода исчисления минимальной арифметики Робинсона гильбертовского типа RM. В 1-9, 25 A, B, C - формулы, в 10, 11, 26, 27 x - переменная, A(x) - формула, C(x) - формула, не содержащая свободно x, t - терм, свободный для x в A(x), в 12-24 a, b и c - предметные переменные, а 0 - индивидуальная константа.
   Схемы аксиом:
      1. A Й (B Й A)
      2. (A Й B) Й ((A Й (B Й C)) Й (A Й C))
      3. A Й (B Й A & B)
      4. A& B Й A
      5. A& B Й B
      6. A Й A Ъ B
      7. B Й A Ъ B
      8. (A Й C) Й ((B Й C) Й (A Ъ B Й C))
      9. (A Й B) Й ((A Й Ш B) Й Ш A)
      10. "xA(x) Й A(t)
      11. A(t) Й $ xA(x)

   Собственные аксиомы:
      12. a = a
      13. a = b Й b = a
      14. a = b Й (b = c Й a = c)
      15. a = b Й aў = bў
      16. a = b Й (a + c = b + c  &  c + a = c + b)
      17. a = b Й (a · c = b · c   &   c · a = c · b)
      18. aў = bў Й a = b
      19. aў = 0 Й 0ў = 0
      20. a = 0 Ъ $ b (bў = a)
      21. a + 0 = a
      22. a + bў = (a + b)ў
      23. a · 0 = 0
      24. a  ·bў = a · b + a

   Правила вывода:

      25. [(A, A Й B)/B]
      26. [(C Й A(x))/(C Й "xA(x))]
      27. [(A(x) Й C)/($ xA(x) Й C)]

   Перейдем теперь к определению системы минимальной арифметики Робинсона генценовского типа SRM. В рамках этой системы предполагается, что A, B, C и D - произвольные формулы; G и D - конечные (возможно, пустые) последовательности формул, q - пустая последовательность формул или последовательность, состоящая из одной формулы; a, b, c и x - переменные; 0 - индивидуальная константа; A(x) - формула; t - терм, свободный для x в A(x), d - переменная, свободная для x в A(x).
   Аксиоматика системы SRM состоит из схемы аксиом вида C ® C, где C - произвольная формула, и арифметических аксиом вида ®Г, где Г - одна из собственных аксиом системы RM. Приведем также правила вывода исчисления SRM.
   Логические правила вывода:

A, G ® B
G ® A Й B
                        D ® A   и  B, G ® q
A Й B, D, G ® q

G ® A   и  G ® B
G ® A & B
                   A, G ® q
A&B, G ® q
     B,G ® q
A&B, G ® q

G ® A
G ® A Ъ B
     G ® B
G ® A Ъ B
                   A, G ® q  и  B, G ® q
A Ъ B, G ® q

A, G ®
G ® ШA
                     G ® A
Ш A, G ®

G ® A(d)   *
G®"xA(x)
              A(t),G ® q
"xA(x), G ® q
  

G ® A(t)
G®$ xA(x)
           A(d), G ® q   *
$ xA(x), G® q

   *    Переменная d постулата не входит свободно в его заключение. (Если A(x) не содержит x свободно, то A(d) есть A(x), какова бы ни была переменная d; в таких случаях мы условимся выбирать для анализа в качестве d переменную, не входящую свободно в заключение, так что ограничение будет соблюдаться.)

    Структурные правила вывода:

        Утончение      [(G ® q)/(C, G ® q)]

        Сокращение        [(C, C, G ® q)/(C, G ® q)]

        Перестановка        [(D, D, C, G ® q)/(D, C ,D, G ® q)]

        Сечение     [(D ® C  и C, G ® q)/(D, G ® q)]

    Следуя [1], правила, стоящие в левом столбце, будем называть сукцедентными правилами и обозначать их через "® Й ", "® &", "® Ъ", "® Ш", "® "", "® $" соответственно. Правила, стоящие в правом столбце, будем называть антецедентными правилами и обозначать через " Й ®", "& ®" и т.д. Отметим, что в исчислении SRМ нет "® У", "® C", "® P" правил, а в правиле "Ш ®" сукцедент заключения пуст.
   Теорема 1. Если формула F выводима в RM и все переменные остаются фиксированными, то секвенция ® F выводима в SRM. Если секвенция ® F выводима в SRM, то формула F выводима в RM и все переменные являются фиксированными.
   Доказательство первой части теоремы аналогично доказательству теоремы 46 ([1], §77), т.е. доказывается, что каждая аксиома исчисления RM выводима в SRM, а каждое правило вывода RM моделируется в SRM. В случае аксиом выводимость очевидна. Перейдем к рассмотрению правил вывода RM. Для правила вывода вида [R/Q] , где R и Q - формулы, нужно доказать, что из выводимости секвенции ® R в исчислении SRM следует выводимость секвенции ® Q в этом исчислении. В случае правила вывода вида [R и S/Q] нужно показать, что в SRM из выводимости секвенций ® R и ® S следует выводимость секвенции ® Q (R, S, и Q - формулы). При этом нетрудно убедиться, что ни в одном из подслучаев нет необходимости применения сукцедентных структурных правил.
   Доказательство второй части теоремы аналогично доказательству теоремы 47 ([1], §77). Чтобы доказать, что каждая секвенция, выводимая в SRM, выводима также и в RM, введем понятие формульного образа секвенции G® q следующим образом. Пусть G - последовательность формул A1,A2,...,An (n і 1), а q - формула B или пусто. Формульным образом секвенции G® q назовем формулу Й q*, где = A1&(A2&...&(An-1& An))...) и

q*= м
н
о
B, если  q  есть  B
Ш(G Й G), если  q  пусто

(G) - некоторая фиксированная замкнутая формула). В случае n = 0 формульным образом секвенции ® q является формула q*, где

q*= м
н
о
B, если  q  есть  B
Ш(G Й G), если  q  пусто

Для завершения доказательства теоремы остается рассмотреть следующие четыре случая:
   1. Формульным образом секвенции вида C® C является формула C Й C. В системе RM выводимость последней очевидна.
   2. Рассматриваемая секвенция - одна из арифметических аксиом системы SRM. В этом случае формульным образом соответсвующей секвенции будет одна из собственных аксиом RM.
   3. Для правила вывода вида [(G1® q1)/(G® q)] нетрудно убедиться, что формула (1) Й q1*) Й
(Й q*) выводима в RM.
   4. В случае правила вывода вида [(G1® q1  и  G2® q2)/(G® q)] легко доказать, что формула (1 Й q1*) Й ((2 Й q2*) Й (Й q*)) выводима в RM.
    Замечание. Структурное правило "® У" необходимо при выводе интуиционистской аксиомы вида Ш A Й (A Й B) . Однако она не является аксиомой ни одной из систем, рассмотренных в данной статье.
   Перейдем к определению секвенциального исчисления SR-M без правила сечения. Определим это исчисление как интуиционистское исчисление G3 (см. [1], §80) с добавлением арифметических аксиом исчисления SR-M со следующим ограничением: в правиле "Ш ®" q должно быть пусто.
   Теорема 2. Если формула F выводима в RM и все переменные остаются фиксированными, то секвенция å ® F выводима в SR-M. Если секвенция å ® F выводима в SR-M, то формула F выводима в RM и все переменные являются фиксированными. (В обеих частях теоремы å - список замкнутых формул, составленных из собственных аксиом исчисления RM).
    Доказательство теоремы основано на эквивалентности RM и SRM, а также на устранении сечений (смешений) в исчислении SRM (аналогично теореме 48 в [1], §78). Заметим, что устранение смешений проводится рассмотрением случаев, указанных в теореме 48 ([1]), учитывая, что
   1. в случае 1а сукцедентные структурные правила не рассматриваются;
   2. случай 2а выпадает из рассмотрения;
   3. в остальных случаях при понижении степени смешения нет необходимости применения сукцедентных структурных правил (в случае 6 сукцедент пуст).

   Ереванский государственный университет


Литература

   1. Клини С. К. Введение в метаматематику, М. ИЛ. 1957.