Cтраница 4
Результаты 3.5 - 3.7 показывают, что FA интерпретируется в НА, причем в ЕА и в НА доказуемы одни и те же негативные формулы. Можно сказать и так, что все, что доказуемо классически, доказуемо и интуиционистски, только связки V и 3 следует понимать при этом классически ( изменение, несущественное с классической точки зрения. Система НА только по видимости слабее FA, фактически, она способна выразить все возможности FA и, кроме того, имеет дополнительные логические связки V и 3, позволяющие выражать конструктивное существование. Классические связки Vc и 3 с не являются необходимыми и выражаются через остальные. Значение полученной интерпретации выходит далеко за рамки формальной арифметики. Современное исследование показывает, что интуиционистские теории гораздо более разнообразно и гибко изучают эффективность в математике, чем их классические аналоги. Многие классические понятия нетривиально разветвляются в интуиционистской теории на несколько неэквивалентных ( ср. В то же время классические теории часто содержатся в соответствующих интуиционистских в качестве некоторого негативного фрагмента. Принципиальное значение имеет рассматриваемая интерпретация и для теории доказательств. Так, если считать непротиворечивость НА надежно установленной, непротиворечивость классической теории ЕА уже может быть установлена с помощью финитного рассуждения пп. [46]
И обратно, только множество, подобное натуральному ряду, удовлетворяет написанной системе аксиом. Таким образом, если трактовать аксиомы содержательным образом, то система аксиом VI, VII, VIII равносильна той системе, которую мы уже рассматривали в § 8 главы III. Она, следовательно, интерпретируема и полна с точностью до изоморфизма. Однако теперь мы не рассматриваем систему аксиом VI, VII, VIII в духе главы III. Она совместно с аксиомами и правилами вывода исчисления предикатов представляет собой формализм, определенный на основе принципов финитизма. Поэтому приведенная выше содержательная трактовка этих аксиом может иметь только эвристическое значение для решения вопросов, возникающих при изучении данного формализма. Аксиомы VI, VII, VIII не исчерпывают формальной арифметики, они не содержат описания арифметических действий. В дальнейшем мы еще расширим это исчисление. Но предварительно мы рассмотрим систему аксиом VI, VII, VIII более детально. [47]
ГЕДЕЛЯ ТЕОРЕМА О ПОЛНОТЕ - утверждение о полноте классического исчисления предикатов: всякая предикатная формула, истинная на всех моделях, выводима ( по формальным правилам классич. А, невыводимой в Генцена формальной системе без сечения. Имеются также доказательства, основанные на расширениях систем формул до максимальных, а также доказательства, использующие ал-гебраич. Теорема вместе с доказательством обобщается на исчисление с равенством. Геделовское доказательство дает для непротиворечивого множества формул модель, элементами к-рой являются термы. Такие модели составляют исходный пункт во многих исследованиях по метаматематике теории множеств. Другое приложение моделей из термов - теорема Левенхей - м а - С к о л е м а: если счетное множество формул имеет какую-то модель, то оно имеет счетную модель. A) выводима в формальной арифметике; здесь Рг ( А) - арифметич. [48]
Согласно гильбертовской программе обоснования математики содержательные математические теории следует оформлять в виде формальных аксиоматических теорий. При этом обычным способам рассуждения в математике соответствуют точно сформулированные правила преобразования объектов формальной теории. Задача обоснования содержательной математической теории сводится, таким образом, к установлению непротиворечивости формальной теории, то есть к выяснению невозможности выведения в данной формальной теории некоторых формул. Допустим, что данная формальная теория Т непротиворечива. При этом, однако, возникает вопрос: насколько можно доверять доказанным в ней теоремам. Иначе говоря, если теорема А доказана в непротиворечивой теории Т, можно ли считать А истинной при достаточно эффективном понимании истинности. Если теорема А содержит упоминание о таких объектах, то невозможно даже непосредственное ее конструктивное истолкование. Допустим даже, что в А упоминаются лишь конструктивные объекты; например, А - формула формальной арифметики. Можно ли рассматривать теорему А теории Т как истинное в том или ином смысле утверждение. От ответа на этот вопрос зависит до некоторой степени содержательная ценность всей программы обоснования математики. В этой заметке показано, что если теория Т достаточно хорошо согласована с классической арифметикой и теорема А теории Т носит отрицательный характер и не содержит конструктивной задачи, то А необходимо конструктивно истинна. [49]