Cтраница 2
Помимо указанных свойств исходного нормированного доказательства и рассматриваемого нами формализма мы еще должны четко представлять себе, что заключительная формула доказательства должна обладать определенными свойствами. [16]
Однако эту процедуру легко модифицировать таким образом, чтобы она давала результат и в том случае, когда в заключительной формуле содержатся е-термы. [17]
Таким образом, в результате применения операции устранения квантора существования порядковое число формулы уменьшится, и это уменьшение продолжится вплоть до заключительной формулы всего нашего вывода. Следовательно, в результате этой операции уменьшится и порядковое число нашего вывода в целом. Итак, мы можем констатировать, что операции устранения индукции и квантора существования, будучи применены к какому-либо выводу, уменьшают его порядковое число. [18]
Тем самым будет показано, что заключительная формула первоначального вывода тоже является истинной, так как при производимых нами операциях устранения индукции и квантора существования заключительная формула не меняется вообще, а при вычислении нумерических термов в концевом фрагменте хотя эта формула сама и может измениться, но ее истинностное значение останется без изменений. [19]
В дальнейшем, когда будет говориться об устранении критических формул или об устранении формул е-равенства, всегда будет иметься в виду устранение такого типа, при котором заключительная формула рассматриваемого нормированного доказательства либо остается без изменений вообще, либо подвергается одному только дизъюнктивному расщеплению. [20]
Если бы в рассмотренном нами примере выделить, скажем, формулу 2 как заключительную, то процесс оборвался бы уже после 3-го шага, поскольку на этом шаге была бы применена заключительная формула. [21]
В том частном случае, когда в исходном выводе нет кванторов существования, можно с помощью рассуждения, аналогичного тому, которое было проведено при рассмотрении рекурсивной арифметики), показать, что заключительная формула данного вывода является верифицируемой, а поскольку она является нумерической, - то и истинной. Таким образом, в рассматриваемом частном случае доказательство закончено. [22]
Таким образом, в результате устранения рассматриваемой схемы индукции порядковое число формулы 31 ( t), которая является одной из исходных формул концевого фрагмента вывода, уменьшится, и это уменьшение распространится по нити вывода, ведущей от формулы 31 ( t), лежащей в концевом фрагменте, к заключительной формуле всего нашего вывода сквозь следующие друг за другом заключения ( других схем в концевом фрагменте нет. [23]
В самом деле, основная идея генценовского доказательства связана не с тем, что в рассматриваемом формализме имеется какая-либо возможность исключать трансфинитные средства, а только с тем, что, с одной стороны, выводы данного формализма в известной мере могут быть вполне упорядочены по степени их сложности и что, с другой стороны, для таких выводов, заключительные формулы которых изображают нечто в элементарном смысле ложное, может быть определена редукция, в результате однократного применения которой к заданному выводу, так сказать, исключается некоторый шаг этого вывода и порядковое число вывода при этом уменьшается. [24]
В деловой переписке принята определенная форма завершения письма. Обычно заключительная формула помещается прямо под основным текстом письма справа. [25]
Затем высоту какой-либо формулы g из нашего вывода мы определим как максимальную из степеней формул той совокупности, которая получается в результате последовательного, начинающегося с формулы % процесса присоединения к каждой формуле всех формул, стоящих рядом с ней и непосредственно под ней. Заключительная формула вывода, являющаяся нумерической, имеет степень и высоту, равную нулю. [26]
Если теперь сократить концевой фрагмент, взяв в качестве исходных формул не сами аксиомы для квантора существования, а результаты их полного вычисления ( и, значит, опустив стоящие над ними формулы), то получится фигура вывода, все исходные формулы которой будут истинными ( формул равенства здесь в качестве исходных формул не будет. Следовательно, заключительная формула нашего вывода должна быть истинной в смысле нового определения. Но так как она является нумерической, то она будет истинной и в прежнем смысле. Таким образом, в данном случае поставленная цель оказывается достигнутой. [27]
Этим определением каждой формуле любого вывода, произведенного по правилам рассмотренного нами формализма, однозначно сопоставляется некоторое порядковое число. Порядковое число заключительной формулы вывода объявляется порядковым числом самого этого вывода. [28]
Метод состоит в том, что символ D можно считать комплексным параметром и решать задачу Коши для ПД уравнения с частными производными как задачу Коши для обыкновенного дифференциального уравнения. Бели в заключительных формулах символу D придать вновь смысл символа дифференцирования, то получим решение исходной задачи. [29]
Собственные аксиомы формализма ( в том числе и специальные аксиомы равенства), а также тождественно истинные формулы исчисления высказываний обладают тем свойством, что любые получающиеся из них в результате подстановки формулы без переменных при естественном распределении истинностных значений являются истинными формулами. Отсюда привычным рассуждением мы получаем, что заключительная формула любого нормированного доказательства, если в ней не встречаются е-сим-волы, при естественном распределении истинностных значений тоже является истинной формулой. [30]