АРИФМЕТИЗАЦИЯ МАТЕМАТИКИ

— метод, разработанный австр. математиком К. Гёделем (р. 1906) в связи с изучением дедуктивных возможностей формальных систем. С помощью А. м. можно воспроизвести в рамках элементарной арифметики различные матем. рассуждения об объектах произвольной формальной системы (т. е. о формулах, доказательствах и т. п.). Все такие объекты можно рассматривать как слова определенного вида в подходящем конечном алфавите, который должен содержать логич. и матем. символы, обозначения для переменных, а также некоторые вспомогательные буквы. Пусть выбрана какая-нибудь нумерация всех слов в алфавите данной формальной системы 2. Тогда метаматем. отношениям, определенным для объектов системы 2, соответствуют числовые предикаты, заданные на номерах этих объектов. Т. о., изучение свойств системы 2 становится частью арифметики. Приведем примеры предикатов, рассматриваемых в связи с описанием данной формальной системы.

Упомянутую выше нумерацию объектов системы 2 можно выбрать так, чтобы перечисленные предикаты (а также другие отношения подобного рода, представляющие интерес для метаматематики) отобразились в результате этой нумерации в примитивно-рекурсивные числовые предикаты. Все примитивно-рекурсивные предикаты выразимы в языке элементарной арифметики (см. Арифметика формальная). Поэтому каждому из перечисленных выше метаматем. предикатов можно поставить в соответствие арифм. формулу, описывающую этот предикат (в терминах выбранной нумерации объектов системы 2). Напр., можно построить следующие формулы:

Отсюда следует, что. в языке элементарной арифметики можно записывать разнообразные утверждения о системе 2. Важными примерами таких утверждений являются:

Первая из этих формул выражает предикат: «г есть номер формулы, доказуемой в 2», вторая формула утверждает, что система 2 непротиворечива.

Допустим теперь, что зафиксирована какая-нибудь достаточно сильная формальная система А для элементарной арифметики. Тогда некоторые формулы, описывающие метаматематику рассматриваемой системы 2, могут быть доказаны в А. Т. о., в рамках системы А можно доказывать теоремы о свойствах самой системы А, а также более сильных систем. Обычно в качестве А берется система, основанная аксиоматике Пеано. От выбора системы А

зависит то, насколько широким будет класс доказуемых метаматем. утверждений. Итак, А. м. заключается в следующем: формулировки метаматем. теорем переводятся на язык арифметики; доказательства этих теорем осуществляются средствами заданной формальной системы А.

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

При использовании метода арифметизации необходимо иметь в виду, что класс метаматем. теорем, коды которых (т. е. соответствующие арифметические формулы) доказуемы в системе А, зависит не только от выбора этой системы А, но и от способа кодирования. Дело в том, что упомянутые выше формулы, выражающие на арифм. языке осн. метаматем. предикаты (формулы и т. д.), были определены неоднозначно. От них требовалось только, чтобы они в самом деле описывали соответствующие предикаты (так что, например, любая формула , область истинности которой совпадает с мн-вом номеров формул системы 2, могла бы быть выбрана в качестве ). Между тем, две содержательно равносильные формулы могут не быть дедуктивно эквивалентными относительно данной системы А. В связи с этим обычно выдвигается дополнительное требование, чтобы арифметизация была, в некотором смысле, естественной. Это требование можно уточнить так: примитивнорекурсивные описания осн. метаматем. предикатов должны копировать определения этих предикатов, даваемые при содержательном изложении метаматематики, а формулы, выражающие эти предикаты, должны иметь ту же структуру, что и соответствующие примитивнорекурсивные описания. Последнее условие заведомо выполняется, если для построения нужных формул используют т. н. процедуру Гёделя. С помощью арифметизации были получены фундаментальные результаты по основаниям математики. В частности, было показано, что ни в какой формальной системе нельзя вывести все истинные формулы арифм. языка (см. Гёделя теоремы о неполноте). Вместе с тем, метод арифметизации показывает, что возможности формальных систем весьма широки. Укажем здесь один характерный пример, иллюстрирующий эти возможности. Пусть, как и выше, А есть достаточно сильная арифм. формальная система. Тогда для некоторой формулы может оказаться, что в А выводим:

где номер формулы в заданной нумерации объектов системы А. Это значит, что независима от аксиом А. Если присоединить к А в качестве новой аксиомы, то получится более сильная формальная система. Существенным моментом здесь является то, что независимость была установлена самой системой А. Очевидно, что этот путь ведет к рассмотрению «самосовершенствующихся» формальных систем. Подобные рассмотрения представляют значительный интерес как для оснований математики, так и для автоматов теории. Лит.: Клини С. К. Математическая логика. Пер. с англ. М., 1973 [библиогр. с. 451-465]; Fefer-m a n S. Arithetization of metamathematics in a general setting. «Fundamenta mathematical», 1960, v. 49.

H. В. Белякин.