Теории первого порядка. Формальная арифметика

Исчисление предикатов, рассмотренное в предыдущем пункте, называют чистым. Этим подчеркивают его исключительно логический характер. При формализации конкретных математических теорий, таких как теория множеств или арифметика, применяют прикладные исчисления предикатов. В прикладных исчислениях используются специфические для соответствующей предметной области предикаты, константы, функциональные символы. Важнейший класс формальных языков, на которых происходит формализация математических теорий, – языки первого порядка (слова «первого порядка» отражают тот факт, что в этих теориях связывать кванторами можно только предметные переменные; применять кванторы к предикатам недопустимо). Теории, формализованные с использованием языков первого порядка, называют теориями первого порядка. Мы дадим описание языков первого порядка и параллельно, в качестве иллюстрации, опишем два важных языка: язык теории множеств Цермело–Френкеля и язык арифметики Пеано, и укажем аксиомы арифметики в рамках формальной теории.

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

Знаки логических операций:, ∧, ∨, →, ∀, ∃.

Переменные: x, y, ….(возможно с индексами).

Скобки: (,).

Эти знаки являются общими для всех языков первого порядка.

Константы: a, b, … (возможно с индексами). В языке теории множеств имеется одна константа ∅ (пустое множество).

В языке арифметики имеются две константы: 0 и 1.

Операции: f, g, … (возможно с индексами) с указанием числа аргументов.

В языке теории множеств операций нет.

В языке арифметики имеются две двухместные операции: сложение "+" и умножение "⋅".

Предикаты: P, Q, … (возможно с индексами) с указанием числа аргументов.

В языке теории множеств имеются: два двухместных предиката: ∈ (быть элементом) и = (равенство).

В языке арифметики имеется один двухместный предикат = (равенство).

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

Множество термов – это наименьшее подмножество выражений, удовлетворяющее двум условиям:

1) переменные и константы являются термами (атомарными);

2) если f – n-местная операция, а t₁, t₂, …, t_n – термы, то f(t₁,t₂,…,t_n) – терм.

В языке теории множеств неатомарных термов нет; термами являются знаки переменных и ∅. Для записи арифметических термов будет использоваться общепринятая форма: вместо +(11) мы будем писать 1+1 и аналогично в других случаях. Кроме того вводятся производные константы, которые служат сокращениями некоторых термов: знак 2 служит сокращением для 1+1; знак 3 – сокращением для 2+1, и т.д.. Далее, x² служит сокращением для x⋅x; x³ – сокращением для x⋅x⋅x и т. д. С учетом этих обозначений термами в языке арифметики являются стандартно понимаемые арифметические выражения.

Множество формул – это наименьшее подмножество выражений, удовлетворяющее двум условиям:

если P – n-местный предикат, а t₁, t₂, …, t_n – термы, то P(t₁,t₂,…,t_n) – формула (атомарная);

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

Примеры атомарных формул в языке теории множеств: x∈y, x=y, x∈∅ (естественно, мы пишем x∈y вместо ∈(xy)). Формула

∀z(z∈x→z∈y)

при неформальной интерпретации означает, что множество x является подмножеством множества y. Для этой формулы используется сокращенная запись x⊂y. Формула

∀x∀y∃u∀z(((z∈x ∨ z∈y) → z∈u)∧ (z∈u→ (z∈x ∨ z∈y)))

при неформальной интерпретации означает, что, каковы бы ни были множества x и y, существует множество u, являющееся их объединением. Используя X↔Y как сокращение для (X→Y)∧(Y→X), эту формулу можно переписать так:

∀x∀y∃u∀z((z∈x ∨ z∈y) ↔ z∈u).

Примеры формул в языке арифметики: 2+2=4, 2⋅2=5, x+y=x+z. Формула

∀x∀y((2x+y=0 ∧ x+2y=0) ↔ (x=0 ∧ y=0))

при неформальной интерпретации означает, что система уравнений 2x+y=0; x+2y=0 имеет единственное решение x=0, y=0.

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

К числу аксиом относятся, во-первых, все аксиомы исчисления предикатов. При этом в аксиомы (P1) и (P2) вносится поправка и они принимают следующий вид:

(P1’) ∀xU(x)→U(t);

(P2’) U(t)→∃xU(x),

где U(t) получается в результате подстановки в формулу U терма t вместо всех свободных вхождений переменной x, при этом терм t не должен содержать переменных, связанных кванторами в формуле U.

Далее, если язык первого порядка содержит предикат равенства, то в число аксиом включатся аксиомы равенства:

(E1) ∀x(x=x);

(E2) ∀x(x=y)→(U(x,x)→U(x,y)), где U – произвольная формула, а через U(x,y) обозначена формула, полученная из U заменой некоторых свободных вхождений x на y (при условии, что вхождение y остается свободным).

На самом деле (E2) представляет собой не одну аксиому, а схему аксиом (по одной для каждой формулы). В теории первого порядка с равенством несложно установить стандартные свойства равенства. Выводимы следующие формулы:

x=y → y=x;

(x=y ∧ y=z) → x=z.

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

Приведем один из вариантов системы специальных аксиом арифметики.

Аксиомы сложения:

x+0=x; x+y = y+x; (x+y)+z = x+(y+z); x+z = y+z → x=y.

Аксиомы умножения:

x⋅0=0; x⋅1=x; x⋅y = y⋅x; (x⋅y)⋅z = x⋅(y⋅z). Аксиома дистрибутивности:

x⋅(y+z) = x⋅y+x⋅z.

Аксиома индукции (схема аксиом):

U(0) ∧ ∀x(U(x)→U(x+1)) → ∀xU(x),

где U – любая формула языка арифметики.

Теория первого порядка называется непротиворечивой, если в ней невозможно вывести какую-нибудь формулу U вместе с ее отрицанием U. Из формулы U∧U (противоречие) вместе с логическими аксиомами можно вывести любую формулу. Поэтому теория непротиворечива тогда и только тогда, когда в ней существуют невыводимые формулы. Следующие теоремы Геделя показывают, насколько непросто обстоит дело даже в такой, казалось бы, простой теории, как формальная арифметика.

Теорема (первая теорема Геделя о неполноте). Любая формальная теория, содержащая формальную арифметику, неполна: в ней существует и может быть эффективно построена формула U, не содержащая свободных переменных, такая, что U истинна, но не выводима.􀀀

Теорема (вторая теорема Геделя о неполноте). Для любой непротиворечивой формальной теории, содержащей формальную арифметику, формула, выражающая непротиворечивость теории, недоказуема.􀀀 Эти две знаменитые теоремы имеют большое методологическое значение. Первая говорит о том, что для достаточно богатых теорий не существует адекватных и полных формализаций. Вторая утверждает, что непротиворечивость теории не может быть установлена средствами самой этой теории. Заметим, однако, что вторая теорема Геделя не отрицает возможности установить непротиворечивость теории. Например, непротиворечивость формальной арифметики может быть доказана (это сделано Генценом), правда, методами, не формализуемыми в формальной арифметике.

Не нашли, что искали? Воспользуйтесь поиском: