Чаще всего неавтономные теории строятся на основе погружения в более широкую теорию, степень формализации которой может быть различной. Такое погружение – это не просто интерпретация теории Т₁ в языке теории Т₂, но “погружение с усилением”, приводящее к возможности выражения в Т₁ тех или иных требований к моделям Т₁. Попытка представления такой конструкции средствами автономной формализации приводит в этом случае к исчезновению неавтономности теории и невозможности выразить такого рода объект этими средствами. С другой стороны, неавтономная теория Т₁ – это и не просто фрагмент более широкой теории Т₂. Разного рода неавтономные теории рассматриваются математиками как достаточно самостоятельные объекты. Таким образом, распространенная сегодня для прояснения “парадокса” категоричности отсылка к различию формальных и содержательных теорий оказывается в данной ситуации следствием отождествления в классической метаматематике понятий “формального” и “автономного”. С нашей точки зрения, неавтономность теории не является в общем случае непереходимым препятствием к ее формализации, но специфический статус неавтономной теории еще не получил, по нашему мнению, своего адекватного выражения в метаматематике и требует расширения представлений о понятии “формальная теория”.

В нашей небольшой работе мы хотели бы кратко коснуться одной по-видимости парадоксальной ситуации, связанной с вопросами категоричности теорий первого порядка. Пусть Т – теория первого порядка, т.е. язык первого порядка, в котором определена логика в рамках исчисления предикатов первого порядка и выделено множество нелогических аксиом. Модель М теории Т – это математическая структура, в которой все предикаты и функции находят свое выражение в рамках символов языка L(T) теории Т и в которой истинны все нелогические аксиомы теории Т. Тогда теория Т называется категоричной, если все модели этой теории изоморфны. В математической логике известна теорема (см. напр. [4, с.123]) о том, что теория первого порядка, имеющая модели с бесконечным числом индивидов (бесконечные модели), не категорична, т.е. имеет неизоморфные модели. Таковы, например, теории первого порядка, формализующие элементарную арифметику с аксиомами Пеано, теорию действительных чисел, геометрию с гильбертовской аксиоматикой. С другой стороны, во многих учебниках по математике приводятся в качестве классических результатов разного рода доказательства категоричности для аксиом Пеано, системы аксиом действительного числа или системы геометрических аксиом по Гильберту. Мы хотели бы еще раз привлечь внимание математиков к этой казалось бы парадоксальной ситуации и отметить возможность принципиально иного ее толкования, чем это обычно принято.

В рамках самой математической логики подобная парадоксальность не раз обсуждалась и получила следующее объяснение: в первом случае мы имеем дело с формальными теориями, во втором – с неформальными, содержательными, теориями; в рамках формальных теорий не удается вполне выразить конструкции содержательных теорий, именно это и приводит к разным результатам относительно категоричности. Например, аксиома индукции в рамках содержательного подхода к аксиоматике Пеано предполагает свою применимость по отношению к несчетному числу предикатов, в то время как формализация этой аксиомы в теории первого порядка превращает ее в схему аксиом только для счетного числа предикатов. Например, Клини пишет: “Система аксиом Пеано для натуральных чисел считается обычно категоричной… Кажущееся противоречие между теоремой Скулема (о некатегоричности формальной арифметики –В.М. и Б.С.) и категоричностью аксиом Пеано объясняется следующим образом. Пятая аксиома Пеано (аксиома индукции в рассматриваемой Клини аксиоматизации элементарной арифметики – В.М. и Б.С.) утверждает, что принцип математической индукции справедлив для всех свойств (т.е. 1-местных предикатов) натуральных чисел; таких свойств существует 2^{А 0}. Так как схема аксиом 13 (схема аксиом индукции в некоторой формализации N аксиоматики Пеано – В.М. и Б.С.) обеспечивает индукцию только для А ₀ свойств, выразимых формулами А(х) системы N, то пятая аксиома Пеано формализована в N неполностью” [1, с.392].

Ту же точку зрения на связь формальности и некатегоричности мы видим и в следующем замечании Скулема, цитируемом Клини: “… числовой ряд полностью характеризуется, например, аксиомами Пеано, если рассматривать понятие “множества” или “пропозициональной функции” как нечто наперед заданное и имеющее абсолютное значение независимо от принципов порождения или аксиом (т.е. если находиться в рамках содержательного подхода – В.М. и Б.С.). Но если бы мы проводили аксиоматическую точку зрения принципиально, так что и рассуждения о множествах и пропозициональных функциях также были аксиоматизированы (т.е. был бы принят формальный подход – В.М. и Б.С.), то, как мы видели, единственность, или полная характеризация, числового ряда невозможна” (цитата по [1, с.392-393]).

(S, F₁, … , F_k, W₁, … , W_р, a₁, … , a_m), где

F₁, … , F_k – операции на S, относительно которых S замкнуто,

W₁, … , W_р – отношения в S,

a₁, … , a_m – некоторые выделенные элементы из S.

1. Sc(х) № 1 для всех х О Р,
2. Для всех x, y О P из Sc(x) = Sc(y) следует x = y.
3. Если А Н Р, 1 О А и А обладает тем свойством, что из х О А следует Sc(х)О А, то А = Р.

Пусть (P, Sc, 1) и (Pў , Scў , 1ў ) – две системы Пеано. Они называются изоморфными, если существует такая функция F, что

1. F – биекция,
2. D(F) = Р и R(F) = Рў ,
3. F(1) = 1ў ,
4. F(Sc(x)) = Scў (F(x)) для любого х О Р.

1. D(F) = P и R(F)Н Pў ,
2. F(1) = 1ў ,
3. F(Sc(x)) = Scў (F(x)) для всех х из Р.

Остается показать, что F – сюръекция и инъекция. Например, для доказательства сюръективности F нужно показать, что R(F) = Pў . Т.к. R(F)Н Pў , то здесь достаточно показать, что R(F) – индуктивное множество для Pў -индукции (т.е. для аксиомы (iii) системы Пеано (Pў , Scў , 1ў )). Тогда, в силу свойства R(F)Н Pў , получаем, что R(F) = Pў . Т.о. мы видим, что ключевую роль в этом доказательстве играет формулировка аксиомы индукции в терминах минимальности (т.е. множество Рў в системе Пеано (Pў , Scў , 1ў ) минимально по отношению ко всем индуктивным множествам). Аналогичное использование минимальной формулировки аксиомы индукции, но только уже по отношению к множеству Р системы Пеано (P, Sc, 1), мы находим в случае доказательства инъективности отображения F (см. [2, c.84-85]).

Но “минимальная индуктивность” есть то же, что “финитность” для натуральных чисел, и таким образом именно предикат “финитный” позволяет в этом случае доказать категоричность содержательной теории. Если этого не удается сделать для формальных теорий первого порядка, то в них не могут быть выражены предикаты типа “финитности”, т.е., по мнению Клини и Сколема, именно такого рода предикаты должны попадать в дополнение от 2^{А 0} предикатов содержательной теории до А ₀ предикатов формальной теории, что и не позволяет доказать категоричность последней.

Итак, в содержательных теориях могут существовать такие конструкции, которые теряются при формализации этих теорий – такова причина различия в результатах о категоричности для содержательных и формальных теорий. Если это так, то необходимо, по-видимому, расширить средства формализации. Однако, в цитированных выше рассуждениях известных логиков слышится оттенок неизбежности подобных потерь, связанных с процедурой формализации вообще. Если допустить, что мы расширили средства формализации, оставаясь в рамках теории первого порядка (например, арифметика второго порядка может быть построена средствами теории первого порядка – см.[4,c.25,334]), то, коль скоро моделью этой теории может быть множество, включающее в себя множество натуральных чисел, эта теория уже не может быть категоричной. Такая ситуация предполагает неизбежность потерь ряда конструкций, например, предикатов типа “финитный”, при переходе от содержательных теорий к формальным. Однако, в отличие от общепринятой точки зрения, наша позиция заключается в том, что дело в данном случае не вообще в различии “содержательного” и “формального”, но в таком их понимании, при котором за этим различием маскируется различие теорий по другому признаку. Этот признак мы называем “автономностью” теории. Иной подход трактовки “парадокса” категоричности, подчеркиваемый нами, основан на различении “автономных” и “неавтономных” теорий. Этот подход пытается объяснить “парадокс” категоричности не на основе степени формализации теории, но в рамках предположения существования двух типов теорий, степень формализации которых не влияет на результаты о категоричности. “Автономные” теории – это чисто синтаксические объекты, не включающие в себя свои семантические отношения. Придание значения, определение модели – всё это внешние процедуры для “автономной” теории, совершаемые после ее построения и никак не влияющие на ее определение. “Неавтономные” теории не ограничиваются при своем построении рамками только языковых средств – рамками синтаксиса. Те или иные семантические отношения, например, условия на модели теории, существенны для построения “неавтономной” теории, что делает ее уже не чисто синтаксическим образованием, но смешанным семантико-синтаксическим объектом. Понятие “автономной теории” совпадает в современной метаматематике с понятием “формальной теории”, что и создает иллюзию объяснения “парадокса” категоричности за счет различения “формального” и “содержательного”. Реально же, по нашему мнению, дихотомия “формального-содержательного” лишь маскирует дихотомию “автономного-неавтономного”, в связи с чем “парадокс” категоричности получает принципиально иную трактовку, независимую от степени формализации теории. Например, как было показано выше, существенным для доказательства категоричности системы Пеано оказывается требование минимальности модели этой системы, т.е. семантическое отношение, включаемое в формулировку аксиомы индукции. Такого рода отношение конечно не может быть выражено в рамках “автономной” теории, выстраиваемой независимо от своих моделей. Именно в этом и следует видеть невозможность выражения предикатов типа “финитный” в рамках “автономных” теорий. Но дело в данном случае не в некоторой мистической содержательности этого предиката, но лишь в отождествлении понятий “формального” и “автономного”, что по определению предполагает заведомое отнесение всех проявлений “неавтономности” к сфере “содержательного”.

“Неавтономные” теории также могут быть формализованы, но средства этой формализации должны выйти за рамки представлений о формальной теории в классической метаматематике. Такую позицию можно найти, например, в [3], где автор рассматривает категоричность теорий с бесконечными моделями как результат использования в языке этих теорий так называемых “допущений экстремальности”. Требование минимальности множества натуральных чисел равносильно архимедовости этого множества, т.е. выполнению аксиомы Архимеда для него, элиминирующей бесконечно-удаленные элементы (нестандартные модели элементарной арифметики). Автор пишет: “Аксиома Архимеда – это своего рода допущение минимальности: она требует, чтобы не было бесконечно удаленных точек или линий… Допущения максимальности и минимальности называются допущениями экстремальности. Очевидно, они могут быть чрезвычайно важны, однако, как мы видели, эти допущения нельзя выразить посредством явных первопорядковых аксиом.

В связи с этим, неважно, в какой именно автономной теории будут пытаться выражать допущения экстремальности. В той мере, в какой идея автономной теории предполагает невозможность выражения в своем языке отношений со своими моделями, в той мере в ней одинаково невыразимы допущения экстремальности. Если же мы попытаемся выразить эти допущения в качестве принадлежащих только метатеории, средствами которой мы можем выразить допущения экстремальности (например, это теория множеств в рассмотренном выше доказательстве категоричности для систем Пеано), то вновь не добъемся нужного результата, т.к. допущения экстремальности принадлежат все же объектной теории, регулируя ее отношения со своими моделями. В связи с этим необходимо осознать тот факт, что даже представление неавтономной теории Т₁ в рамках более обширной теории Т₂ (которая, кстати, может быть и автономной теорией) еще не лишает первую статуса отдельной теории, хотя и предполагает неавтономность этой теории в рамках чисто синтаксических определений. В частности, допущения экстремальности, будучи выраженными на языке теории множеств, все же должны рассматриваться в приведенном выше примере принадлежащими не теории множеств, но неавтономной теории арифметики Пеано (являясь неотъемлемой частью формулировки аксиомы индукции (iii) этой теории). С другой стороны, неавтономную теорию невозможно сформулировать и как автономную теорию, т.к. в этом случае категоричность будет потеряна. Вот этот промежуточный статус теории между автономной теорией первого порядка и ее интерпретацией в рамках более широкой теории и образует феномен “неавтономной теории”. В случае неавтономной теории Т₁ мы имеем дело не просто с погружением теории Т₁ в более широкую теорию Т₂, но с “погружением с усилением”, приводящим к возникновению ряда конструкций в теории Т₁ именно за счет такого погружения (такими конструкциями являются, например, допущения экстремальности). В случае обычной интерпретации одной формальной теории в языке другой формальной теории мы не получаем дедуктивного усиления первой теории, но лишь переводим ее на другой язык.

По-видимому, в первой трети нашего столетия в математике еще господствовало представление о математической теории как неавтономной теории, особенно в форме “теория – стандартная модель теории”. Термина “категоричность” в это время вообще не было, т.к. все наиболее важные теории считались категоричными (в силу указанных причин). Теория называлась “полной” (отсюда – название гильбертовской “аксиомы полноты”), если в ней можно было выразить все основные факты стандартной модели, тесно связанной с данной теорией. Положение начинает меняться после открытий Сколема, Гёделя в математической логике, показавших неполноту формальной арифметики и существование неизоморфных моделей в теории множеств. Расширение сферы влияния математической логики и гёделевское направление ограничения теорий рамками только автономных теорий привели к “автономизации” представлений и самих математиков, что, по-видимому, выразилось в усилении дихотомии “формального” и “содержательного” и использовании идеологии полимодельности (некатегоричности) всякой достаточно сильной теории. В связи с этим, продолжавшие существовать проявления разного рода неавтономности теорий, связанные, в частности, с сохраняющимися доказательствами категоричности, отчасти стали приписываться неуловимому призраку неформализуемой содержательности, отчасти привели к попыткам более формального и строгого выражения этого феномена средствами погружения языка теории в более мощные языковые средства теории множеств. Однако, последовательное проведение этой методологии должно, по мнению Хинтикка, привести к построению нестандартной теории моделей.

Таким образом, можно говорить по крайней мере о тенденции отождествления в рамках классической метаматематики (использующей обычные определения теории, модели и т.д.) понятий “формального” и “автономного”. В связи с этим, категоричность элементарной арифметики объясняется ее содержательностью. С нашей точки зрения, это верно лишь относительно классической точки зрения на формальную теорию как автономную теорию. В общем случае можно говорить о некотором новом измерении аксиоматических теорий, связанным с понятиями “автономного” и “неавтономного”, и именно в различии положения аксиоматической теории на этом измерении следует, по нашему мнению, видеть причину различий в категоричности теорий элементарной арифметики и других подобных теорий.