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

Формальная (аксиоматическая) теория

Лекция 4

Простой пример формального исчисления (исчисление А)

 

Формальный язык:

1. Алфавит: O I + =

2. Терм: O, OI, OII, OIII, … - суть термы, если t1, t2, t3 – термы, то t1+t2=t3 – формула.

Обозначим OII…I через n, где n – количество палочек.

Исчисление:

3. Аксиомы: 0+0=0, 1+0=1, 0+1=1

4. Правило вывода: из k1+m1=n1 и k2+m2=n2 непосредственно следует k1+k2+m1+m2=n1+n2

Вывести 2+3=5

Формальная (аксиоматическая) теория считается определенной, если:

(1). Задано счетное множество символов. Конечные цепочки символов - выражения теории .

(2). Выделено подмножество выражений теории , называемых формулами.

(3). Выделено некоторое подмножество формул , называемых аксиомамитеории .

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

«Непосредственное следствие», вывод, следствие множества формул, теорема.

(1). Символы L: и заглавные буквы латинского алфавита (с цел. полож. индексами).

(2). Все буквы - формулы. Если ,- формулы, то и - тоже формулы.

(3). Каковы бы ни были формулы теории L, следующие формулы суть аксиомы L:

(A1) ;

(A2) ;

(A3) .

(4). Правило вывода - modus ponens (МР): есть непосредственное следствие и .

Пример вывода формулы в теории L:

(1.) -

Теорема дедукции: Если Г - множество формул, и - формулы и , то .

В частности, если , то .

Доказательство: , пусть вывод , где .

Индукцией по i (1<=i<=n) докажем (тогда теорема дедукции доказана).

- либо элемент Г, либо аксиома, либо совпадает с .

В первых двух случаях из схемы аксиом (А1) и по МП .

В третьем случае, когда совпадает с , из (1.) , следовательно, .

Допустим, что для любого k<i.

- либо элемент Г, либо аксиома, либо совпадает с , либо следует по МП из каких-то и (j,m<i).

Первые три случая как и при i=1.

В четвертом случае имеет вид ,

согласно индуктивному предположению, и .

Из схемы аксиом (А2) .

По МП , и снова по МП .

Утверждение доказано по индукции (а, значит, и теорема дедукции доказана).

Замечания:

1. При доказательстве использованы только схемы аксиом (А1) и (А2).

2. Доказательство позволяет по данному выводу из Г и построить вывод из Г.

Следствия:

1. . Действительно, ведь из .

2. . Действительно, ведь из .

3. . Действительно, ведь

Утверждение: Формула теории L является теоремой теории L, тогда и только тогда, когда она является тавтологией.

Утверждение: Всякая теорема теории L является тавтологией.

Теорема о полноте теории L: Если формула теории L является тавтологией, то она является теоремой теории L.