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

6 · (A ® B) ® (A ® C) МР(4, 5)

(Т2): любая константа (символ выделенного элемента) является термом.

(Т3): если t₁ , … , t_m – термы, а f ^(m) – один из функциональных символов теории, то f ^(m)(t₁ , … , t_m) – терм.

(Т4): других термов нет.

Теперь от простого к сложному строится понятие формулы специальной теории:

(Ф1): если t₁ , … , t_m – термы, а P ^(m) – один из предикатных символов теории, то P ^(m)(t₁ , … , t_m) – бескванторная формула, зависящая от всех переменных, участвующих в термах t₁ , … , t_m , причём все её переменные свободны.

(Ф2): если A и В – две формулы, то (A Ù B), (A Ú B), (A ® B), (A « B), – тоже формулы, в которых свободны все вхождения объектных переменных, свободные в А или в В, и связаны все вхождения объектных переменных, связанные в А или в В.

(Ф3): если A(x) – формула хотя бы с одним свободным вхождением объектной переменнойx, то выражения (" x A(x)) и ($ x A(x)) – формулы, в которых связаны вхождения всех объектных переменных, связанных в А, а также все вхождения x, и свободны все вхождения объектных переменных, свободные в А, кроме переменной х. При этом формула A(x) называется областью действия квантора.

(Ф4): других формул нет.

Система аксиом специальной теориисостоит из

· аксиом формального исчисления предикатов,

· специальных аксиом теории.

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

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

IV. Пример специальной теории: формальная арифметика. Алфавитсостоитиз нескольких групп символов:

·достаточно большое количество переменных x, y, … , x₁₀₀ , … для обозначения натуральных чисел,

·1 – выделенный элемент,

· + , × – знаки бинарных арифметических операций сложения и умножения,

· = – единственный предикатный символ равенства чисел,

·Ù , Ú , ® , « , – логические связки,

·", $– кванторы,

·( , ) – служебные символы (скобки).

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

(АВ1): любая переменная является арифметическим выражением.

(АВ2): 1 – арифметическое выражение.

(АВ2): если A и В – арифметические выражения, то (А + В) и (А×В) – тоже арифметические выражения.

(АВ3): других арифметических выражений нет.

Примеры: 1.1 + x – не арифметическое выражение, т.к. нет скобок.

2. ((x + 1)×(z + t)) – арифметическое выражение.

Формулы арифметикитожеопределяются от простого к сложному:

(Ф1): если А, В – два арифметических выражения, то (А = В) – бескванторная формула, зависящая от всех переменных, участвующих как в А, так и в В, причём все её переменные свободны.

(Ф2): если A и В – две формулы, то (A Ù B), (A Ú B), (A ® B), (A « B), – тоже формулы, в которых свободны все вхождения объектных переменных, свободные в А или в В, и связаны все вхождения объектных переменных, связанные в А или в В.

(Ф3): если A(x) – формула хотя бы с одним свободным вхождением объектной переменнойx, то выражения (" x A(x)) и ($ x A(x)) – формулы, в которых связаны вхождения всех объектных переменных, связанных в А, а также все вхождения x, и свободны все вхождения объектных переменных, свободные в А, кроме переменной х. При этом формула A(x) называется областью действия квантора.

(Ф4): других формул нет.

Примеры: 1. ((x = 1) Ù (y×x+1 = 1)) – бескванторная формула со свободными переменными x и y.

2. ((x + 1)×(z + t) + 1) = (t) – не формула (лишние скобки в правой части).

3. (" t ((x + 1)×(z + t) + 1) = (t + x + 1)) – формула с квантором, связывающим переменную t и свободными переменными x, z.

Аксиомы формальной арифметикикроме аксиом исчисления предикатов включают несколько групп аксиом:

Рефлексивность: (" x (x = x))

Симметричность: (" x (" y ((x = y) ® (y = x)))

Транзитивность: (" x (" y (" z (((x = y) Ù (y = z)) ® (x = z))))

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

Это – очень сильная форма подстановки, её можно значительно ослабить.

Условимся для арифметических выражений А(x₁ , … , x_n) и В(y₁ , … , y_m) использовать краткую запись А(x₁ , … , x_n) ¹ В(y₁ , … , y_m) вместо отрицания .

Аксиомы операций сложения и умножения:

Существование и единственность следующего: (" x ($ ! y (y = x + 1)))

Единица – наименьший элемент: (" x ((x + 1) ¹ 1))

Равенство следующих: (" x (" y ((x + 1) = (y + 1)) « (x = y)))

Ассоциативность прибавления 1: (" x (" y ((x + (y + 1)) = ((x + y) + 1))))

Единица – нейтральна по умножению: (" x ((x×1) = x))

Связь сложения и умножения: (" x (" y ((x×(y + 1) = ((x×y) + x)))))

Схема формальной индукции

Для любой формулы арифметики А(x) со свободной переменной x следующая формула является аксиомой: ((А(1) Ù (" y (А(y) ® А(y + 1)))) ® (" x А(x))).

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