Cтраница 2
Если такое исследование продвинуто достаточно далеко и, в частности, найдены формальные признаки, характеризующие выводимые предложения, то для доказательства непротиворечивости аксиоматики остается лишь доказать, что не существует предложения, обладающего этими признаками одновременно с его отрицанием. [16]
Интересно заметить, что, как и в случае генценовского доказательства непротиворечивости с помощью трансфинитной индукции до е0, анализ рассматриваемого нами доказательства непротиворечивости показывает, что оно в единственном его неэлементарном шаге зависит от использования предиката, определяемого посредством индукции, в индукционный шаг которой входят кванторы обоих родов, а именно, речь идет здесь о предикате истинности для арифметических формул. Мы сейчас определим этот предикат. [17]
Как мы уже неоднократно указывали, вопрос о непротиворечивости любого из рассматриваемых нами исчислений равносилен вопросу о существовании в нем невыводимой формулы. Для доказательства непротиворечивости достаточно в таком случае доказать существование в рассматриваемом исчислении невыводимой формулы. Мы докажем, что в ограниченной арифметике формула 0 0 невыводима. В самом деле, если бы эта формула была выводима в ограниченной арифметике, то в силу замечания, сделанного нами в конце § 9, она была бы слабо регулярной. Но так как эта формула примитивна, то она тогда должна быть примитивно истинной в слабом смысле. Итак, формула 0 0, не будучи слабо регулярной, не может быть выводима в ограниченной арифметике. [18]
Теоремы Геделя, указывая на предел возможностей финитизма, направили значит, часть последовавших за ними исследований по новому пути: не отказываясь от осн. Шютте ( 1951) для доказательства непротиворечивости классич. Еще раньше Гедель ( 1932 - 33) показал непротиворечивость классич. [19]
IV без правил образования и аксиом для могут быть даны метаматематические доказательства непротиворечивости и полноты, а также разрешающая процедура. Пресбургер рассматривает некоторую классическую систему арифметики натуральных чисел. [20]
Так же как трансфинитная индукция до ш8, может быть сведена к обыкновенной индукции и индукция до е 1) - это было проделано формально Гильбертом и Бернайсом [ 1939, стр. В последней своей статье [1943] Генцен доказывает несводимость индукции до е0 прямо, а не косвенно с помощью теоремы Геделя и своего доказательства непротиворечивости. [21]
Для того чтобы теория могла приносить такого рода пользу, содержащиеся в ней действительные предложения должны быть истинными. Прежде математики считали, что это обеспечивается истинностью тех теорем, которые мы теперь воспринимаем как идеальные; мы же теперь надеемся обеспечить это посредством доказательства непротиворечивости. [22]
Правда, мы знаем, что до сих пор противоречия не встречались. Доказательства непротиворечивости в математике всегда относительны; когда речь идет о сравнительно сложных областях, то непротиворечивость в одной области сводится к непротиворечивости в другой. [23]
Брауэр ( 1908) выступил против применения правил его отрицание - ] А. Д. Гильберт предложил представить классич. Тогда для доказательства непротиворечивости достаточно ностей. Допуская существование сколь угодно больших установить невыводимость в рассматриваемой теории натуральных чисел, интуиционисты выступают против нек-рых утверждений. Они считают, что в математике всякое доказа - новится предметом изучения нек-рой математич. Особой смысленными образованиями понятий, к-рые в моей критике со стороны интуиционистов подвергается иеклю - теории доказательств исключаются сами собой... [24]
Первый результат, по существу, означает, что окончательная формализация науч. Второй результат показывает, что такой проблемой является непротиворечивость теории S, и для ее доказательства требуются неарифметич. С помощью дополнительных принципов были получены доказательства непротиворечивости арифметики, анализа и ряда др. теорий. Была усилена теорема Геделя о неполноте: найдены ариф-метич. [25]
Зависимость какого-нибудь предложения t от других высказываний какой-либо системы аксиом является установленной, поскольку a in соп - creto доказано на основании этих высказываний. Для установления же независимости нужно показать, что ни одна сколь угодно далеко проведенная комбинация умозаключений не приведет к предложению а. Для достижения этой цели мы располагаем тремя методами; согласно сказанному выше каждый из них служит также и для доказательства непротиворечивости системы аксиом. [26]
Условие на теорию Т в теореме - это условие типа непротиворечивости, которое может быть конструктивно понимаемо. Если говорить описательно, оно означает, что арифметика содержится в Т достаточно естественно. Хорошо известны, например, естественные погружения арифметики в теоретико-множественные теории, такие, как теория Цермело-Френкеля, New Foundations Куайна и теория типов. До сих пор неизвестны финитные доказательства непротиворечивости этих теорий, а тем более Тк-непротиворечивости. Но обнаружение Тк - противоречия в одной из этих теорий свидетельствовало бы, по-видимому, о столь же неблагополучном положении вещей, как и обнаружение просто противоречия. С другой стороны, для некоторых теорий Г, например для ZQ [8] и предикативного анализа [10], Ти-непротиворечивость может быть конструктивно установлена. [27]
Вероятно, нет такой науки, в которой логика применялась бы в большей мере, чем в математике. Все предложения, если они не приняты за аксиомы, строго доказываются. Самый выбор аксиом также логически обосновывается: ищутся доказательства непротиворечивости, полноты, часто и независимости аксиом. [28]
Аккерману удалось о использованием индукции до первого е-числа довести рассмотренный в гл. II ( с, 124 - 161) метод, исходящий из первоначального гильбертовского подхода и не ведущий финитными средствами к искомому результату, до доказательства непротиворечивости арифметического формализма. [29]
Klein, 1871) проективная модель неевклидовой геометрии Лобачевского сводит вопрос о непротиворечивости геометрии Лобачевского к непротиворечивости евклидовой геометрии. Однако не видно было, какими средствами можно строить модели анализа и арифметики для доказательства их непротиворечивости. Гильберта состоит в том, что он указал прямой путь для исследования этого вопроса. Тогда для доказательства непротиворечивости достаточно установить невыводимость в рассматриваемой теории нск-рых утверждений. [30]