Имея в виду эту схему, определим операцию "t свертывания кванторсш, перерабатывающую любую предваренную формулу (Хв мулу 01/ вида
3uVir3zM , (2)
где M - бескванторная. Операция % передвигает кванторы 3 из сочетаний V3 вперед по схеме CT (добавляя к бескванторной части конъюнктивные члены 3zTCi,t^,H)), затем выносит всеЗ^ ред, а затем склеивает все соседние одноименные кванторы в один. Например,
{ Зщ\1м , 3\1 , % H'(u,,'ü',,u^2^)=0) =
=3uVij3zCTau ) , ^üvu ) jA [ TCCii\^^
Здесь (Х\ - показатель, с которым входит i-e простое число р^ в разложение X на простые множители.
Если обозначить через НА формальную систему гейтинговской арифметики с иддукцией лишь по бескванторным формулам, то для бой предваренной (А/
Hk - ^CJy - d^d (3)
причем импликация слева направо выводима даже в H А•
Теперь зафиксируем определение истинности для трехквантор- ных формул. Это - формула Т вида (2) с единственной свободной переменной d , причем для любой формулы А вида (2)
Доказательство соотношения (4) можно найти, например, в [^8].
Для любой позитивной формулы 01 обозначим через 0|г ренную формулу формулы 01 , получаемую из 01 каким-йибудь етайдар- тным методом. Пусть X - элементарная функция, дающая по любому номеру Û предваренной формулы 01 номер формулы 01 • Положим
С помощью (3),(4у получается доказательство (Î) в НА +СТ
Вместо ^['"А J будем в дальнейшем писать ^ А .
Мы будем пользоваться также тш, что при стандартном выборе преобразований Т , Si , формулы Т^ и т^.д. формула ^ тна относительно логических операций и равенства: если M - менная для бескванторных формул » А , ß " переменные для ных формул, то в НА + ОТ выводимо:
55