Аксиоматическая теория 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.

Дата добавления: 2013-12-13