Пример 2

Построить доказательство формулы A É A Ù А

1. (A É A) É ((A É (АÉ A Ù A)) É (A É A Ù А))	1.
2. ØØAÉ A	2. АС10
3. (A É (АÉ A Ù A)) É (A É A Ù А)	3. МР(F1,F2)
4. A É (АÉ A Ù A)	4.
5. A É A Ù А	5. МР(F3,F4)
6. ├ A É A Ù А	9. ОФД (1-5) – определение формального доказательства

Обобщим понятие формального доказательства на случай вывода некоторой формулы B из других формул А₁,...,А_п, называемых посылками (гипотезами).

Определение 4. Формальным выводом формулы В из посылок А₁,..., А_п называется конечная последовательность формул В₁,...,B_k, заканчивающаяся формулой B (B_k = В), причем каждая формула этой последовательности

1. или одна из посылок А₁,..., А_n,

2. или аксиома,

3. или формула, полученная из некоторых двух предшествующих формул этой последовательности по правилу МР.

Если существует формальный вывод формулы В из формул А₁,...,А_п, то формула В называется формально выводимой из формул А₁,...,А„ и обозначается так: A₁,..., А_п├В, или Г├В, где Г = {A₁,...,A_n}.

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

Дата добавления: 2015-06-27