.Математическая.. логика,, алгебра, и.. теория., чисел
Волин Ю.М., кандидат технических наук Научно-исследовательского физико-химического института им. Л.Я. Карпова
О НОРМАЛЬНЫХ ВЫВОДАХ В АРИФМЕТИКЕ И ПРОБЛЕМЕ ПРОТИВОРЕЧИВОСТИ - 1
В статье вводится понятие нормализации вывода для формальной арифметики (обобщающее соответствующее понятие для исчислений Правица [1]) и обрисованы подходы к доказательству нормализации и слабой нормализации. Нормализация выводов позволяет доказать ряд важных свойств арифметической системы, имеющих прямое отношение к исследованию вопроса о возможной противоречивости арифметики. Отметим, что в работах [2-8] исследование проблемы противоречивости было выполнено применительно к теории множеств 2БС.
1. Формальная система и общие сведения.
Будем использовать формальную систему натурального вывода Правица [1] в ее интуиционистском варианте. Отметим специфические особенности этой системы. Наряду с индивидными переменными, имеющимися в счетном числе и обозначаемыми буквамих,у,2 (с индексами или без), система содержит также счетное число индивидных параметроа,Ъ,е. При этом термы не могут содержать переменных, а формулы не могут содержать переменных свободно (все вхождения переменных в формулу являются, таким образом, связанными, а все вхождения параметров свободными). В отличие от терма псевдотерм может содержать переменные, а псевдоформула может иметь свободные вхождения переменных. Областью действия кванторов V, 3 в формуле являются переменные, но если говорить о генетическом построении формулы, то надо иметь в виду, что в ходе построения могут делаться замены некоторых вхождений параметров на вхождения переменных. Так если имеется формула
А = А(а) , то, применив квантор V, можно получить формулу VxA'a, где А<а - псевдоформула, получаемая из формулы А в результате подстановки переменной X вместо всех вхож/ л ах „ ; дений параметра а (а Ахъ есть результат последовательной подстановки X вместо а и Ъ
вместо X ). Предполагается, что внутри действия Vx и 3х нет кванторов общности и существования с той же самой переменной х.
В системе Правица вводятся такие логические константы: пропозициональные связки &, V, з , кванторы V, 3 и пропозициональная константа для ложности (абсурда) Л . Символ для отрицания « —» является определяемым: по определению —А есть формула А зЛ (что, собственно говоря, ничего не меняет по существу, но имеет определенные удобства). Также определяемым является символ тождества «=»: А = В есть формула (А з В)&(В з А).
Степенью формулы называют А называют число вхождений логических констант (за исключением Л ) в нее.
Формулу без параметров называют предложением.
Вывод формулируется в виде дерева формул, в котором заключения правил заключения расположены непосредственно под посылками и для каждого закрываемого допущения указано, где оно закрывается. В самом верху расположены начальные формулы (допущения, незакрытые и закрытые, и аксиомы), а выводимая формула (конечная формула) расположена в самом низу. Если в выводе отсутствуют незакрытые (свободные) допущения, то вывод назы-
вают доказательством (конечной формулы вывода). Обозначение Г \ А дает характеристику вывода, указывая, что речь идет о выводе формулы А из множества незакрытых допущений Г. Соответственно, слова «П есть вывод Г |- А » говорят о том, что П есть вывод А из Г . Если используется обозначение |- А , то речь идет о доказательстве А (множество Г пусто). Далее мы немного модифицируем определение Г |- А (см. замечание 2).
Будем говорить также о закрываемых и незакрываемых допущениях (смысл этих терминов достаточно очевиден). Незакрытые допущения будем называть гипотезами вывода. Будем применять термин «гипотеза» также применительно к закрываемым допущениям, пока они еще не закрыты.
Исчисление предикатов первого порядка у Правица вводится, как вариант натурального вывода Генцена: формулируются не аксиомы исчисления, а правила заключения и правила вывода. Правила делятся на три категории: правила введения (I -правила), правила удаления (Е -правила) и Л -правила. I -правила и Е -правила вводятся для каждой пропозициональной связки и для каждого квантора, а Л -правила вводятся для символа абсурда. Правила заключения указывают, как одни формулы выводятся из других, а правила вывода определяют, кроме того, как закрываются допущения (точнее, как они могут быть закрыты), и таким образом дают полную характеристику системы натурального вывода. Ниже приведена система правил вывода для интуиционистского исчисления предикатов. Правила введения:
& I: <<Г1, А >,<Г2,В > / < Л = Г1 иГ2, А & В >>, VI: <<Г, А > / <Л = Г, А V В >>, << Г, В > / <А = Г, А V В >>, з I: <<Г, В > / <Л = Г- {А}, А з В >>,
VI: <<Г, А > / <Л = Г, УА% >>,
ЗI : <<Г, АХ > / <БхА >>, где Г, , Г, Л - множества незакрытых (свободных) допущений, ^ - терм, а в правиле VI предполагается, что параметр а не входит ни в одну из гипотез из Г , от которых зависит А . Л -правило в интуиционистской системе одно:
Л1: <<Г, Л > / <Л = Г, А >>.
Правила удаления:
& Е : << Г, А & В > / <Л = Г, А >>, << Г, А & В > / < Л = Г, В >>,
V Е:
«Г, А V В >, <Г2, С >, <Г3, С > / <Л = Г! и (Г2 - {А}) и (Г3 - {В}), С >>, з Е : «Г], А >, <Г2, А з В > / <Л = Гх иГ2, В >>,
VE : << Г, VxA > / < Л = Г, АХ >>,
ЗЕ : «Г], БхА >, <Г2, В > / Л =< иГ2 - {АХ }, В >>,
где в правиле ЗЕ предполагается, что параметр а не входит в ЗхА, в В и ни в одну из гипотез, входящих в Г2 - { Аах } , от которых зависит В .
Отметим, что классическое исчисление предикатов отличается от интуиционистского лишь добавлением еще одного Л -правила:
ЛС : <<Г,Л> / <Л = Г- {-А}, А >>
(при этом правило ЛI оказывается частным случаем этого правила), а известное правило для
символа отрицания — (позволяющее проводить доказательство от противного) есть просто частный случай правила з -введения (когда В = Л ).
Выводы, использующие введенные выше правила вывода, принято называть натуральными выводами.
Правила з I, V Е, 3Е VI и Лс называют правилами косвенного вывода, а остальные - правилами прямого вывода.
Для большей ясности дадим пояснение одному из правил, в качестве которого возьмем правило з -введения. Это правило утверждает, что если формула В выводится из допущений Г , то формула А з В выводится из допущений Г — {А} , т.е. из тех же допущений за вычетом допущения А . Таким образом, допущение А , если оно входило в Г , при применении этого правила закрывается (точнее, может закрываться). При этом говорят, что А закрывается на вхождении формулы В применением правила з I. Это означает, что дерево П( А з В), детерминированное вхождением формулы А з В (см. далее), не содержит А в качестве гипотезы.
Правила заключения отличаются от правил вывода тем, что в них отсутствуют множества допущений Г, Л, и, таким образом, они ничего не говорят о закрытии допущений. Например, правило заключения з I имеет вид (В / А з В) , а правило заключения з Е (то-ёшропепв) имеет вид (А, А з В / В) . Правило заключения V Е содержит три посылки, правила & I, з Е , 3Е - две, а остальные правила - одну посылку. Каждое правило имеет одно заключение.
В примере (А, А з В / В) правила з Е, примере (В V С, А, А / А) правила V Е и примере (3хВ, А / А) правила 3Е формулу А слева от черты «/» называют меньшей посылкой. Посылку, не являющуюся меньшей, называют большей. В случае правила V Е говорят о первой и второй меньших посылках.
Следует различать формулы, как таковые, и вхождения формул (в дерево вывода). Вхождение формулы есть единство формулы и ее места в дереве вывода (по другому: вхождение формулы - это вершина в дереве вывода). Саму формулу по отношению к ее вхождению будем при этом называть видом вхождения формулы. Иногда, если это ясно из контекста, будем для краткости говорить «формула» или «вхождение» вместо «вхождение формулы».
Следуя Правицу, будем использовать для формул, как таковых, и вхождений формул одни и те же обозначения, а отличие одних от других будет делаться по контексту.
Если А есть вхождение формулы в дерево П, то поддеревом П, детерминированным вхождением А, называют дерево, полученное из П удалением всех вхождений, кроме А и вхождений, расположенных выше А . При этом используют обозначение П( А) .
Понятие «вхождение формулы А находится выше (ниже) вхождения формулы В в выводе П » определяется естественным образом. Если начальная формула А находится выше В и остается гипотезой для П(В) , то говорят, что В зависит от А . Если А/, А^ - посылки в применении некоторого правила в выводе П, то говорят, что А/ находится в боковой связи с А^ .
Аналогично формулам будем различать выводы как таковые и вхождения выводов. В последнем случае речь идет о выводе, являющемся подвыводом некоторого вывода П , расположенном в определенном месте П .
Последовательность А1,А2,...,Ап вхождений формул в дерево вывода П называют нитью [1], если (1) А1 есть начальная формула П; (2) А/ находится непосредственно над А/+1 для любого / < п; (3) Ап есть конечная формула вывода П. Каждое А^ при 1 < / < п является как посылкой применения некоторого правила, так и заключением. А1 яв-
ляется только посылкой, а Ай - только заключением. Если сохраняется только требование (2), то будем говорить о правильной последовательности вхождений формул.
Ветвью будем называть последовательность, в которой выполняются требования (1) и (2), а требование (3) формулируется следующим образом: Ап есть конечная формула вывода
П или первое вхождение формулы, служащей меньшей посылкой применения з Е. Обычно понятие ветви применяется к последовательностям, не содержащим меньших посылок применения правил V -удаления и З -удаления.
В некоторых случаях удобно использовать правильные последовательности с обратной нумерацией элементов, от нижних формул вывода к верхним.
Параметр а в применении правила VI либо правила ЗЕ называют собственным пара-метромправила. Справедлива [1] следующая
Лемма 1 (лемма о чистых параметрах). Если имеется вывод П получения А из гипотез Г , то существует также такой вывод П] (получения А из Г ), что его собственные параметры чист
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.