От Эвклида до Гёделя: аксиоматический метод в курсе математической логики в вузе

Формулами вформальной аксиоматической теории являются последовательности символов определенного вида, то есть не всякое слово (выражение) является формулой данной формальной аксиоматической теории.

Из множества формул выделяется некоторое подмножество формул, называемых аксиомами.

Задается конечное множество отношений между формулами, называемых правилами вывода.

Выводом в формальной аксиоматической теории называется конечная последовательность формул этой теории B₁, B₂, …, B_n, каждая из которых либо является аксиомой, либо выводится из одной или нескольких предыдущих формул этой последовательности по одному из правил вывода.

Формула Ф формальной аксиоматической теории называется теоремой, если существует вывод, последней формулой которого является Ф.

Простым примером формальной аксиоматической теории является исчисление высказываний.

Доказано, что исчисление высказываний является полной и непротиворечивой формальной аксиоматической теорией.

Для формализации рассуждений, которые не могут быть обоснованы в рамках исчисления высказываний, в математической логике используют исчисление предикатов.

Интерпретацией языка формальной аксиоматической теории называется соответствие, сопоставляющее каждому элементу языка теории единственный элемент некоторого множества D,называемого областью интерпретации.

Моделью формальной аксиоматической теории называетсяинтерпретация языка формальной аксиоматической теории, в которой истинны все аксиомы теории.

Например, моделью исчисления высказываний является алгебра высказываний.

Для формализации математических теорий в математической логике используют формальные аксиоматические теории первого порядка, в которых не допускаются предикаты, имеющие аргументами предикаты и функции, а также не допускаются кванторы по предикатам и функциям.

Язык формальной аксиоматической теории первого порядка совпадает с языком исчисления предикатов. Термы и формулы теории первого порядка определяются также как и в исчислении предикатов.

Аксиомы теории первого порядка разбивают на два класса: логические аксиомы исобственные (нелогические) аксиомы.

Перечни логических аксиом и правил вывода теорий первого порядка

Собственные аксиомы не могут быть сформулированы в общем случае и меняются от теории к теории.

Доказано, что исчисление предикатов первого порядка является полной и непротиворечивой теорией.

Моделью исчисления предикатов первого порядка является логика предикатов.

Формальная арифметика

Первое, полуаксиоматическое, построение арифметики было предложено в

1901 году Дедекиндом и стало известно под названием «система аксиом Пеано».

Аксиомы этой системы формулируются следующим образом:

1. 0 есть натуральное число.
2. Для любого натурального числа x существует другое натуральное число, обозначаемое x и называемое следующее за x.
3. 0  x для любого натурального числа x.
4. Если x = y, то x = y.
5. Если Q есть свойство, которым обладает натуральное число 0, и для всякого натурального числа x из того, что x обладает свойством Q, следует, что и натуральное число x обладает свойством Q, то свойством Q обладают все натуральные числа.

Пятую аксиому принято называть принципом индукции.

Этих аксиом достаточно для построения не только арифметики натуральных чисел, но и для построения теорий рациональных, вещественных и комплексных чисел.

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

Для вывода всех основных результатов элементарной арифметики была построена теория первого порядка S.

Теория S имеет следующие собственные аксиомы:

1. .
2. .
3. .
4. .
5. .
6. .
7. .
8. .
9. , где — произвольная формула теории S.

Девятую аксиому принято называть принципом математической индукции.

С помощью правила отделения из девятой аксиомы получается следующее правило индукции: из и выводится.

Рассмотрим интерпретацию теории S, в которой:

1. Множество всех неотрицательных чисел служит областью интерпретации.
2. Целое число 0 интерпретирует символ «0».
3. Прибавление единицы интерпретирует операцию взятия следующего.
4. Обычные сложение и умножение интерпретируют операции «+» и «∙».
5. Символ «=» интерпретируется как отношение тождества.

Если считать истинность аксиом теории S в этой интерпретации интуитивно очевидной, то эта интерпретация является моделью теории S. Эта модель называется стандартной моделью теории S.

Термы 0;0;0;0;…в теории S называют цифрами и обозначают соответственно 0; ; ; ;…, то есть 0 с nштрихами обозначают .

В теории S можно ввести отношение порядка и понятие делимости. Далее можно показать, что теоремы, доказываемые в курсах элементарной теории чисел можно перевести на язык теории S и построить вывод полученной теоремы.

Для сокращения утверждения: «A есть теорема теории S» применяют запись .

Арифметические функции иарифметические отношения

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

Арифметическими отношениями называются отношения, заданные на множестве натуральных чисел.

Арифметическое отношение R(x₁,…, x_n) называется выразимым в теории S, если существует формула A(x₁,…, x_n) теории S с n свободными переменными такая, что для любых натуральных чисел k₁,…, k_n выполняются условия: если R(k₁,…, k_n)истинно, то и если R(k₁,…, k_n)ложно, то.

В теориях первого порядка с равенством выражения вида «существует один и только один x такой, что A(x)» символически можно записать так: , для сокращения используют запись .

Арифметическая функция f(x₁,…, x_n) называется представимой в теории S, если существует формула A(x₁,…, x_n+1) теории S со свободными переменными x₁,…, x_n+1 такая, что для любых натуральных чисел k₁,…, k_n+1 выполняются условия:

1. Если f(k₁,…, k_n) = k_n+1, то .

2. .

Характеристической функцией отношения R(x₁,…, x_n) называется функция

C_R(x₁,…, x_n), которая равна 1, если отношение R(x₁,…, x_n) истинно, и равна 0, если отношение R(x₁,…, x_n) ложно.

При изучении представимости арифметических функций в теории S в качестве простейших функций выбраны следующие функции:

1. Нуль-функция: Z(x) = 0 при всех x.
2. Прибавление единицы: N(x) = x + 1 при всех x.
3. Проектирующие функции: при всех x₁,…, x_n, i = 1,…, n.

(-оператор).

Функция f(x₁,…, x_n)называется примитивно рекурсивной, если она может быть получена из исходных функций с помощью конечного числа суперпозиций функций и схем примитивной рекурсии.

Функция f(x₁,…, x_n)называется частично рекурсивной, если она может быть получена из исходных функций с помощью конечного числа суперпозиций функций, схем примитивной рекурсии и операций минимизации.

Функция f(x₁,…, x_n)называется общерекурсивной или рекурсивной, если она частично рекурсивна и всюду определена.

Доказано, что класс рекурсивных функций совпадает с классом функций представимых в теории S.

Отношение R(x₁,…, x_n)называется примитивно рекурсивным, если примитивно рекурсивной является его характеристическая функция C_R(x₁,…, x_n).

Отношение R(x₁,…, x_n)называется рекурсивным, если рекурсивной является его характеристическая функция C_R(x₁,…, x_n).

Теорема. Всякаярекурсивная функция представима в теории S.

Теорема. Всякоерекурсивное отношение выразимо в теории S.

Гёделева нумерация формул ивыводов вформальной арифметике

Каждому символу u произвольной теории первого порядка ставится в соответствие положительное число g(u), называемое гёделевым номером символа u, следующим образом:

g(() = 3; g()) = 5; g(,) = 7; g() = 9; g() = 11;

g(x_k) = 5 + 8k, где k = 1, 2, …;

g(a_k) = 7 + 8k, где k = 1, 2, …;

для k, n  1;

для k, n  1.

Гёделев номер выражения u₀u₁…u_r определяется следующим образом: , где p_i есть i-епростое число, при этом p₀ = 2.

Гёделев номер последовательности выражений e₀, e₁,…, e_r определяется следующим образом: , где p_i есть i-епростое число, при этом p₀ = 2.

Таким образом, функция g взаимно однозначно отображает множество всех символов, выражений и конечных последовательностей выражений в множество целых положительных чисел.

Теорема Гёделя онеполноте формальной арифметики

Доказано, что -непротиворечивая теория первого порядка является непротиворечивой.

Если признать стандартную интерпретацию теории S в качестве модели этой теории, то тогда теорию S следует признать -непротиворечивой.

Для доказательства неполноты формальной арифметики используется примитивно рекурсивное отношение W₁(u, y)=«u есть гёделев номер формулы A(x₁), содержащей свободную переменную x₁, и y есть гёделев номер вывода в S формулы » [5].

Так как отношение W₁(u, y) примитивно рекурсивно, то оно выразимо в теории S некоторой формулой V₁(x₁, x₂) с двумя свободными переменными x₁, x₂.

Рассмотрим формулу . Пусть m — гёделев номер этой формулы. Подставим в эту формулу вместо x₁, получим замкнутую формулу: .

Теорема (Гёдель, 1931 год). Если теория S непротиворечива, то формула невыводима в теории S,иесли теория S -непротиворечива, то формула невыводима в теории S. Доказательство смотри в [4].

Таким образом, в непротиворечивой теории S невыводимы как формула , так и ее отрицание .

Рассмотрим стандартную интерпретацию неразрешимого предложения .

Так как V₁ выражает в теории S отношение W₁, то, в соответствии со стандартной интерпретацией, формула утверждает, что отношение W₁(m, x₂) ложно для любого натурального числа x₂, а это означает, что не существует вывода формулы в теории S. Таким образом, формула утверждает свою собственную невыводимость в теории S.

Из теоремы Гёделя следует, что если теория S непротиворечива, то эта формула и в самом деле невыводима в теории S и поэтому истинна при стандартной интерпретации.

В теореме Гёделя содержится предположение о -непротиворечивости теорииS. Однако ценой некоторого усложнения доказательства можно ограничиться предположением об обычной непротиворечивости теории S. В этом случае необходимо будет воспользоваться примитивно рекурсивным отношением W₂(u, y) = «u есть гёделев номер формулы A(x₁), содержащей свободную переменную x₁, и y есть гёделев номер вывода в S формулы ».

Так как отношение W₂(u, y) примитивно рекурсивно, то оно выразимо в теории S некоторой формулой V₂(x₁, x₂) с двумя свободными переменными x₁, x₂. Значит, если W₂(k₁, k₂)истинно, то , и если W₂(k₁, k₂) ложно, то .

Рассмотрим формулу . Пусть n — гёделев номер этой формулы. Подставим в эту формулу вместо x₁ — получим замкнутую формулу: .

Теорема (Россер, 1936 год). Если теория S непротиворечива, то в ней невыводимы обе формулы и и, следовательно, существует неразрешимое предложение этой теории.

Эту теорему называют теоремой Гёделя в форме Россера.

Теорема Гёделя онепротиворечивости формальной арифметики

Для доказательства непротиворечивости формальной арифметики помимо отношений W₁(u, y) и W₂(u, y)используется примитивно рекурсивное отношение

Pf(y, x) = «y есть гёделев номер вывода в S формулы с гёделевым номером x»,выразимое в теории S с помощью некоторой формулы Pf(x₁, x₂).

Далее, если x — гёделев номер формулы A, то через Neg(x) обозначают гёделев номер формулы . Доказано, что функция Neg(x)рекурсивна и, следовательно, представима в теории S некоторой формулой Neg(x₁, x₂) [5].

Формула в стандартной интерпретации выражает невозможность вывода в теории S какой-либо формулы вместе с ее отрицанием и является истинной в том и только том случае, когда теория S непротиворечива. Иными словами, эту формулу можно интерпретировать как утверждение непротиворечивости теории S.

Другими словами, если теория S непротиворечива, то доказательство непротиворечивости теории S не может быть проведеносредствами самой теории S.

Литература:

1. Смилга В. П. В погоне за красотой. — М.: «Молодая гвардия», 1968. — 288 с.
2. Сухан И. В., Кравченко Г. Г., Иванисова О. В. К вопросу о методике изучения аксиоматического метода в курсе математической логики в вузе. // Педагогика высшей школы. — 2016. — № 3. — С. 125–128.
3. Сухан И. В., Кравченко Г. Г., Иванисова О. В. Аксиоматические теории в курсе математической логики // Педагогика высшей школы. — 2017. — № 3. — С. 28–38.
4. Сухан И. В., Кравченко Г. Г., Иванисова О. В. Построение формальной арифметики в рамках изучения аксиоматических теорий в вузе. // Педагогика высшей школы. — 2018. — № 1. — С. 00–00.
5. Мендельсон Э. Введение в математическую логику. — М.: Наука, 1976. — 320 с.