Cтраница 1
Применения правила V-удаления в дальнейшем часто будут описываться на языке случаев ( ср. Применения правила формальной индукции часто будут, с использованием терминологии, принятой для содержательной индукции ( § 7), излагаться следующим образом: Базис. На этом месте заканчивается индукционный шаг и А ( х) перестает быть исходной формулой. [1]
Действительно, ( II) получается из ( I) путем V-удалений и - введений. Обратно, ( I) получается из ( II) путем V-введений и - удалений. [2]
В следующем примере 2 шаг 1 является выводом из исходной формулы Ъ Ф 0 с фиксированной Ь, так что - введение здесь применимо. В примере 3 -введение не применимо, потому что Ъ варьировалась, хотя оно и становится применимым после V-удаления. В примере 4 показывается, как при нарушении упомянутого ограничения может получиться ложный ( в арифметической интерпретации) результат. [3]
Далее продолжаем таким же образом. После каждого 3-удал, ( примененного к некоторому у, встречающемуся в одной из исходных формул правее остальных переменных и отличному от всех остальных переменных, указанных в какой-либо из исходных формул) и 74 применяем V-удаление к тем х, которые не покрыты этим 3-удалением, и затем опускаем полученную исходную формулу, если она дублирует какую-нибудь другую, так что те у, которые будут стоять правее остальных на следующей стадии, опять будут отличаться друг от друга. [4]