Аксиоматические теории в курсе математической логики

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

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

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

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

Замечание. Любая аксиома является теоремой — вывод состоит из одной формулы.

При построении формальных аксиоматических теорий используется понятие эффективной процедуры (или эффективного алгоритма).

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

Для формальной аксиоматической теории должны выполняться следующие требования:

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

− понятие аксиомы должно быть эффективным, то есть должна существовать эффективная процедура, позволяющая для произвольной формулы решить, является ли она аксиомой;

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

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

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

Алфавит исчисления высказываний содержит:

1. Символы: ¬, →, (,).
2. Буквы и буквы с нижним индексом: A,B,C, …, A₁, B₁, C₁….

Формулы исчисления высказываний определяются следующим образом:

1. A, B, C, …, A₁, B₁, C₁… — формулы.
2. Если A формула, то ¬(A) — формула.
3. Если A иBформулы, то (A) → (B) — формула.
4. Строчка символов является формулой, только если она удовлетворяет условиям 1–3.

Аксиомы исчисления высказываний.

Для любых формул A, B и C следующие формулы являются аксиомами:

1) (A → (B → A)).

2) ((A → (B → C)) → ((A → B) → (A → C)).

3) ((¬B → ¬A) → ((¬B → A) → B)).

Правило вывода: из A и A → B следует B.

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

Язык исчисления предикатов содержит:

1. Конечное или счетное множество предметных постоянных {a₁, a₂, …}.
2. Конечное или счетное множество предметных переменных {x_1, x₂, …}.
3. Конечное или счетное множество предикатных букв
4. Конечное или счетное множество функциональных букв
5. Логические связки ¬, →, символ квантора ∀, скобки (,) и запятую.

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

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

Термы определяются следующим образом:

1. Предметная переменная или предметная постоянная — терм.
2. Если t₁, t₂, …, t_n — термы, то — терм.
3. Строчка символов является термом, только если она удовлетворяет условиям 1 и 2.

Аргументами предикатных букв являются термы. Результатом применения предикатных букв являются элементарные формулы: если — предикатная буква, а t₁, t₂,…,t_n — термы, то — элементарная формула.

Формулы исчисления предикатов определяются следующим образом:

1. Любая элементарная формула —формула.
2. Если A формула, то ¬(A) — формула.
3. Если A иBформулы, то (A) → (B) — формула.
4. Если A — формула, а x — предметная переменная, то ∀x A — формула. При этом формула A называется областью действия квантора ∀x.
5. Строчка символов является формулой, только если она удовлетворяет условиям 1–4.

Вхождение переменной x в формулу называется связанным, если x является переменной входящего в эту формулу квантора ∀xили находится в области действия входящего в эту формулу квантора ∀x,впротивном случае вхождение переменной x в данную формулу называется свободным.

Переменная называется свободной переменной вформуле, если существуют свободные ее вхождения в эту формулу.

Переменная называется связанной переменной вформуле, если существуют связанные ее вхождения в эту формулу.

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

Пример. Терм свободен для x₁в , но несвободен для x₁в .

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

При этом каждой предикатной букве соответствует некоторое n-местное отношение в D, каждой функциональной букве — некоторая n-местная операция в D(то есть функция, отображающая DⁿвD), каждой предметной постоянной a_i — некоторый элемент из D.

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

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

Пример. Если в качестве области интерпретации взять множество целых положительных чисел, а формулу интерпретировать как отношение x₁ ≤ x₂, то истинно для всех упорядоченных пар (a, b) целых положительных чисел таких, что a ≤ b.

В этой интерпретации формула представляет собой свойство (то есть отношение с одним аргументом) «для каждого целого положительного x₂: x₁ ≤ x₂» которое выполняется только для числа 1, а формула является истинным высказыванием, утверждающим существование наименьшего целого положительного числа, то есть 1.

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

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

Формальные аксиоматические теории первого порядка.

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

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

Перечни логических аксиом и правил вывода теорий первого порядка это дополненные соответствующие перечни исчисления высказываний.

Логические аксиомы теории первого порядка.

Для любых формул A, B и C следующие формулы являются аксиомами:

1. (A → (B → A)).
2. ((A → (B → C)) → ((A → B) → (A → C)).
3. ((¬B → ¬A) → ((¬B → A) → B)).
4. ∀x_i A(x_i) → A(t),гдеt — терм, свободный для x_iвформуле A(x_i).
5. ∀x_i (A → B) → (A → ∀x_i B),если формула A не содержит свободных вхождений x_i.

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

Правила вывода:

1. Из A и A → B следует B.
2. Из A следует ∀x_i (A).

Теория первого порядка, не содержащая собственных аксиом, называется исчислением предикатов первого порядка.

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

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

Теория имеет одну предикатную букву , одну функциональную букву и одну предметную константу a₁.

В соответствии с общепринятыми обозначениями будем писать t = s вместо , t + s вместо и 0вместо a₁.

Собственными аксиомами теории являются формулы:

1. ∀x₁∀x₂∀x₃ (x₁ + (x₂ + x₃) = (x₁ + x₂) + x₃).
2. ∀x₁ (0 + x₁ = x₁).
3. ∀x₁∃x₂ (x₂ + x₁ = 0).
4. ∀x₁(x₁ = x₁).
5. ∀x₁∀x₂ ((x₁ = x₂) → (x₂ = x₁))
6. «x₁«x₂«x₃ ((x₁ = x₂) → ((x₂ = x₃) → (x₁ = x₃))).
7. «x₁«x₂«x₃ ((x₂ = x₃) → ((x₁ + x₂ = x₁ + x₃)  (x₂ + x₁ = x₃ + x₁))).

Всякая модель этой теории называется группой.

Если в группе истинна формула ∀x₁∀x₂ (x₁ +x₂ = x₂ + x₁), то группа называется абелевой, или коммутативной.

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

− множество целых чисел с операцией сложения и числом 0 в качестве 0;

− множество R⁺ = (0; +∞) с операцией умножения и числом 1 в качестве 0;

− множество всех подмножеств любого непустого множества с операцией симметрической разности и множеством ∅вкачестве 0.

Метаматематика.

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

В качестве метаязыка можно использовать некоторый узкий фрагмент какого-либо национального языка, например, русского. Если разрешить использовать в качестве метаязыка весь национальный язык, то возникает опасность вывода парадоксов — например, парадокса Рассела.

Теоремы, описывающие какие-либо свойства формальной аксиоматической теории, называются метатеоремами.

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

Например, A → A — теорема исчисления высказываний, а «Исчисление высказываний непротиворечиво» — метатеорема.

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

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

Заинтересованный читатель может глубже ознакомиться с этими вопросами, обратившись к [2, 3, 4, 5, 6].

Литература:

1. Сухан И. В., Кравченко Г. Г., Иванисова О. В. К вопросу о методике изучения аксиоматического метода в курсе математической логики в вузе. // Педагогика высшей школы. — 2016. — № 3. — С. 125–128.
2. Успенский В. А., Верещагин Н. К., Плиско В. Е. Вводный курс математической логики. — М.: Физматлит, 2007. — 128 с.
3. Игошин В. И. Математическая логика и теория алгоритмов. — М.: Издательский центр «Академия», 2010. — 448 с.
4. Колмогоров А. Н., Драгалин А. Г. Введение в математическую логику. — М.: Издательство Московского университета, 1982. — 120 с.
5. Мендельсон Э. Введение в математическую логику. — М.: Наука, 1976. — 320 с.
6. Столл Р. Р. Множества. Логика. Аксиоматические теории. — М.: Просвещение, 1968. — 232 с.