Элементы формальных теорий

Принципы построения ф.т.

Для задания ф.т. нужно определить:

1)алфавит;

2)формулы - правильно построенное выражение;

3)аксиомы – подмножество формул (конечно, бесконечно);

4)правило вывода – правило получения новых формул из уже имеющихся;

F(A1 , A2 ,..., An 1 , An ) - n-местное отношение на множестве формул.

Если (A1, A2 ,..., An 1, An ) вступают в отношение F, то говорят, что формула (A1, A2 ,..., An 1, An ) непосредственно выводима из (A1 , A2 ,..., An 1 ) и записывают:

	A1 , A2 ,..., An 1	F или	A1 , A2 ,..., An 1 ├─ An .
	An
├─ - выводимость.

Теоремой называется формула B, если существует последовательность формул A1 , A2 ,..., An 1 , An B такая, что каждый член последовательности либо является аксиомой, либо получен по некоторому правилу вывода из предыдущих: ├─B (B – выводима).

Говорят, что множество формул B выводимо из множества гипотез ( ) :

├─B, где Г – некоторый список формул, если существует последовательность A1 , A2 ,..., An 1 , An B, любой член которой либо формула из списка Г, либо аксиома, либо

получен по правилу вывода из предыдущей.

Пример: классическое исчисление высказывания L. 1) Алфавит A, Bi (,), ,

2)Формулы:

а) символ каждой переменной или переменная с индексом объявляется формулой; б) если A и B – формулы, то A -формула, (А B) - формула;

в) других формул нет Замечание: внешние скобки будем опускать.

3)Следующие формулы называются схемой аксиом:

I)A (B A) ;

II)(A (B C)) ((A B) (A C))

III)( B A) (( B A) B)

Аксиомой называется формула, полученная из какой-либо схемы аксиом подстановкой на места её переменной какой-либо формулы.

			A	B
	Подстановка в первую схему аксиом:			.
			C	A A
	I) C ((A A) C) - аксиома по первой схеме аксиом.
	4) Modus Ponens (MP) – правило вывода -			A B, A
				B
	Утверждение о A A. ├─ A A.(├─ - теорема).
	A	B	C
	II)	A A
	A		A
	B1 : (A ((A		A) A)) ((A (A A)) (A A)) - аксиома по II схеме.
	B2 : A ((A		A) A) - аксиома по I схеме.

21

A	B
I)
A	A A
Применим правило отделения.

B3 : (A (A A)) (A A) по MP к B1 , B2 Посылка этой импликации.

B4 : A (A A) - аксиома по I схеме аксиом.

A		B
I)	A
		A

B5 : A A по MP к B3 , B4

Доказали, что ├─ A A.

Утверждение. (├─ о дедукции) , A ├─ B ├─ A B. Доказательство.

B1 , B2 ,..., Bn B (каждый член последовательности либо аксиома, либо гипотеза, либо получен по правилу вывода из предыдущих)

...A B1...A B2 ...A Bi ...A Bn

(сделали основу и покажем, что можно сделать вставки так, что вся

последовательность превратится в вывод A B)

По индукции:

1) вставка перед первой A B1

(по MP)

а)

B1

-

аксиома

или

формула из

списка Г, тогда

вставка

B1 (A B1 ), B1 A B1 (по MP)

б) если

B1 A,

нужно сделать A A (берём 4 формулы из доказанной ранее

теоремы, где A A, в качестве вставки).

2) Предположим, что все вставки до A Bi 1

сделаны и покажем, что можно

сделать вставку перед формулой A Bi .

а) B1

- аксиома или формула из списка Г.

B (A B ),B A B

(по MP из предыдущих)

i

i

i

i

аксиома по I подстановке

б) Bi A

...A A (аналогично пишем те же 4 формулы)

в) Bi

по MP из предыдущих.

B j Bk Bi ,...,

Bk ,

j, k i

По допущению индукции где-то сделаны вставки

...A (Bk Bi )...A Bk

Возьмём вторую схему аксиом.

A

B

C

B

B

A

k

i

(A (Bk

Bi )) ((A Bk ) (A Bi )) - аксиома по первой схеме

(A Bk ) (A Bi ) по MP к

Применим правило вывода к

A Bi по MP к

.

В этом случае вставка состоит из двух формул:

и

22

Если перед любой формулой можно сделать вставку, то и перед последней тоже можно.

...A B1...A B2 ...A Bi 1...A Bi ...A Bn , ч.т.д. Следствие (обобщённая ├─ о дедукции).

, A ├─ B ├─ A B Доказательство.

1)- уже доказано.

2).

Существует последовательность формул B1 , B2 ,..., A B, каждый член которой или гипотеза, или аксиома, или получена по MP из предыдущих.

B1 , B2 ,..., A B, A, B по MP к предыдущим.

Применение теоремы о дедукции.

1. Транзитивность импликаций (т.и.).

A B, B C ├─ A C

1)A B - гипотеза;

2)B C - гипотеза;

3)A - гипотеза;

4)B по MP к 1, 3;

5)C по MP к 2, 4;

6)	A B, B C,	A ├─ C (итог пяти пунктов);
7)	A B, B C ├─ A C (по теореме о дедукции).

A B, B C т.и.

A C

2. Правило сечения (п.с.).

A (B C), B ├─ A C

1)A (B C) - гипотеза;

2)B - гипотеза;

3)A - гипотеза;

4)B C по MP к 1, 3;

5)C по MP к 2, 4;

6)	A (B C), B, A	├─C
7)	A (B C), B ├─ A C (по теореме о дедукции).

23