2.1. Определение формальной теории, или исчисления

Формальная теория Т состоит из следующих компонент:

1. Множества знаков, oбpaзyюшx алфавит языка теории.

2. Множества слов, составленных из знаков алфавита, называемых формулами.

3. Подмножества формул всего множества формул, называемых аксиомами.

4. Множества правил вывода, с помощью которых из формул получают формулы.

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

Обычно формулы состоят из конечного числа знаков. Но бывают теории с бесконечно длинными формулами, т.е. с формулами, содержащими бесконечное число знаков.

2.1.1. Доказательство. Непротиворечивость теории. Полнота теории

Формальное доказательство формулы А в теории Т - это конечная последовательность формул

Ai,Ai,...,An, (2.1)

где каждая формула Аг является либо аксиомой, либо получена из пpeдыдyшx с помощью одного из правил вывода, а An - это формула А.

Последняя формула в доказательстве (2.1) называется теоремой. Используется символическая запись для теорем :

Формальная теория называется полной, если для всякого высказывания Л имеем:

h А или h -пЛ.

По замыслу создателя исчисления предикатов Фреге, любая пра-

вш1ьно построенная формула, точнее высказывание, должна быть теоремой, т.е. должна быть доказываемым утверждением. Иначе говоря, исчисление высказываний и исчисление предикатов должны быть полными теориями. Ожидания Фреге оправдались (см. ниже теоремы 2.3 и 2.6). Но, как оказа)Юсь, более сильные теории, включающие арифметику, неполны. Это было доказано Гёделем (см. ниже теорема 2.9).

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

А&с~пА,

где А произвольное высказывание теории.

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

2.2. Исчисление высказываний

2.2.1. Язык и правила вывода исчисления высказываний

Исчисление высказываний - это следующая формальная теория:

Знак h читается как «доказуемо А» или «Л теорема». Знак h введен в 1879 г. немецким логиком Фреге.

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

1. Алфавит.

• Знаки пропозициональных переменных

Xi, Х2,Хп,...

• Логические связки

V, &, .

• Вспомогательные знаки

(> )

2. Формулы.

• Пропозициональная переменная есть (атомарная) формула.

• Если Л и В формулы, то [А&сВ), [АУ В), (А => В) формулы.

• Если А формула, то ~пА формула.

3. Аксиомы (схемы Клини).

AiBA)

(Л (В С)) {{А В) (Л С))

(Л&В) А (Л&В) В Л (В (Л&В))

Л(ЛУВ) В(ЛУВ)

(Л С) ((В С) ((Л V В) С)) IV

(Л В) ((Л -.В) -.Л)

3. Правила вывода.

А, А=)-В В

(modus ponens).