Cтраница 2
Впрочем, эта общая формулировка теоремы Эрбрана несущественно превосходит ее формулировку для случая квазипредварен-ных формул. Даваемый ею критерий выводимости формулы эквивалентен критерию, получающемуся преобразованием формулы произвольного вида в квазипредваренную формулу2) и применением к этой последней теоремы Эрбрана для квазипредваренных формул. [16]
Во втором томе подробно излагаются и обсуждаются результаты теории доказательств, относящиеся к логическим исчислениям и к формализованной арифметике. Это известная теорема Эрбрана, дающая важный критерий выводимости формул в исчислении предикатов, теорема Черча о невозможности алгоритма, распознающего выводимые формулы исчисления предикатов, теорема Геделя о неполноте арифметических исчислений и различные доказательства непротиворечивости формализованной арифметики. Особую ценность представляет подробное обсуждение используемых при доказательстве непротиворечивости арифметики средств, выходящих за рамки первоначальной финитной точки зрения Гильберта. [17]
Первое очевидно ( и посылка А не нужна), второе равносильно выводимости формулы ( А Л т) - В, которая нам дана по условию леммы. [18]
Обратим внимание, что это утверждение по своему характеру отличается от утверждений о том, что из основных схем формализма ( 3) выводимы те или иные схемы формул. Выводимая схема формул остается применимой и в том случае, когда к формализму добавляются какие-либо новые символы, в то время как наше утверждение о выводимости формул вида 11 91 - - 51 существенным образом связано со способом построения рассматриваемых формул 21 и перестает быть применимым, если мы, например, включим в формализм ( 3) символ дизъюнкции. [19]
Если мы примем во внимание, что во всех утверждениях 1 - 4 речь идет о выводимости формул без формульных переменных, то у нас получится еще один результат, касающийся сферы действия этих утверждений. В самом деле, замену общей аксиомы равенства ( J2) соответствующими специальными аксиомами при переходе от системы ( Z) к системе ( Z) мы с самого начала произвели с учетом того, что при исследовании вопроса о непротиворечивости эта замена не накладывает на результат никаких ограничений, так как по отношению к выводимости формул без формульных переменных общие аксиомы равенства равносильны этим специальным. [20]
Мы докажем, что верно и обратное: всякая непротиворечивая пара совместна. В частности, когда В состоит из единственной формулы, получается утверждение теоремы о полноте. Мы предполагаем, как это обычно делается, что конъюнкция пустого множества формул есть тождественно истинная формула, а дизъюнкция - тождественно ложная. Заметим кстати, что противоречивость пары ( р 0) означает выводимость формулы - чр. [21]