Cтраница 1
Формальная арифметическая система с аксиомами 1 - 24 неполна в том смысле, что в ней существуют постоянные высказывания ( формулы, не содержащие свободных переменных), которые нельзя ни доказать, ни опровергнуть средствами этой системы. [1]
Формальная арифметическая система предыдущих глав дает нам пример того, как может быть проведена формализация. Оетаэим в стороне тонкости и рассмотрим только голый скелет того, что должно содержаться в формальной системе, если она пригодна для тех целей, в которых вводится. [2]
Для формальной арифметической системы, если F не содержит логических символов, кроме гэ, &, - ч, V ( в частности, если F есть Е для некоторой формулы Е), то - - i - i F гэ F ( и, следовательно, - - ч - I F-F) интуиционистски. [3]
Формулы строящейся нами формальной арифметической системы исчерпываются формулами, которые можно построить из элементарных формул с помощью операций ( узкого) исчисления предикатов. [4]
Построенная в предыдущем параграфе формальная арифметическая система представляет собой пример формализации математической теории на базе исчисления предикатов. Подобная формализация позволяет разложить на точно определенные элементарные составные части процесс доказательства всех доказуемых в рамках данной теории предложений. [5]
Более полное обсуждение этого вопроса имеется у Клини [1945], где расширение неусиленной интуиционистской формальной арифметической Системы 5 до усиленной интуиционистской системы S, которая расходится с классической системой Sc, предлагается в виде отождествления истинности с реализуемостью. [6]
Как видно из приведенного доказательства, для установления недоказуемости построенной нами формулы достаточно предположения о простой непротиворечивости формальной арифметической системы, а предположение об ш-непротиворечивости системы используется лишь при доказательстве неопровержимости этой формулы. [7]
Для правильного понимания выписанных соотношений необходимо заметить, что в целях экономии скобок в формулах построен -, ной нами формальной арифметической системы устанавливается определенный порядок старшинства операций: все арифметические операции ( непосредственное следование, умножение и сложение) являются старшими по отношению к равенству, а последнее старше всех логических операций. [8]
Оказывается, что при некоторых дополнительных пред-положениях из указанного свойства формулы Vy iA p, у) вытекает ее неразрешимость, что и доказывает неполноту построенной нами формальной арифметической системы. Дополнительное предположение, о котором здесь идет речь, сводится к тому, что формальная арифметика предполагается со-непротиворечивой. [9]
В содержательном понимании арифметический предикат представляет собой произвольный ( не обязательно конструктивно определенный) предикат на множестве всех целых неотрицательных чисел. Построенная нами формальная арифметическая система дает способ конструктивного задания некоторых арифметических предикатов. [10]
Так, для доказательства непротиворечивости приходится выходит ь за рамки строго финитных методов. Полнота же вообще не имеет места для построенной нами формальной арифметической системы. В этом состоит смысл знаменитой теоремы Геделя о неполноте арифметики, заставившей по-новому взглянуть на всю проблему обоснования математики и автоматизации ( на базе полной формализации) процесса вывода новых теорем в дедуктивно строящихся теориях. [11]
Поскольку это противоречит теореме 5, то формула 91 не может быть доказуемой в системе 5, что и показывает невозможность доказательства непротиворечивости формальной арифметической системы средствами самой этой системы. [12]
Формулы, обладающие подобным свойством, принято называть нумерически. Проверка истинности предиката, нумерически выражаемого такой формулой, при любом наборе значений предметных переменных может быть проведена, в силу сказанного, конструктивным путем. В построенной нами формальной арифметической системе каждая формула без переменных является разрешимой, а каждая формула без кванторов - нумерически разрешимой формулой. [13]
Легко видеть, что геделевский номер всякой неэлементарной вещи непременно четный. Имея в виду этот факт, а также однозначность разложения всякого натурального числа на простые множители, нетрудно понять, что по геделевскому номеру можно однозначно восстановить соответствующую ему формулу. Это означает, что соответствие между формулами рассматриваемой нами формальной арифметической системы и их геделевскими номерами является взаимно однозначным. [14]
Предположим сначала, что формула Vy iA p, у) доказуема. Обозначим через k геделевский номер доказательства этой формулы. Но тогда, в силу сделанного вначале предположения, рассматриваемая нами формальная арифметическая система будет ( просто) противоречивой, что исключается в силу условия ее ю-непротиворечивости. [15]