Пример 1. Формальное доказательство и формальный вывод

Формальное доказательство и формальный вывод

Правило вывода Modus ponens

Определение 2. Правилом вывода теории L называют процедуру перехода от двух формул вида А и А É B к одной формуле вида В для любых А и В.

Это правило называют modus ponens, MP. Правило МР позволяет удалять оператор É, поэтому его называют также правилом удаления импликации и обозначают УИ. В случае применения правила МР формулы А и AÉ В называют посылками, а В - заключением этого правила.

Определение 3. Формальным доказательством (в теории L) называется конечная последовательность формул В₁,..., B_k, причем каждая формула этой последовательности либо аксиома, либо получена по правилу МР из каких-либо двух предшествующих формул этой последовательности. Формальное доказательство является доказательством своей последней формулы В_k. Формула В называется формально доказуемой, или формальной теоремой (теории L), если она имеет формальное доказательство.

Утверждение «Формула В формально доказуема в теории L» будем обозначать ├_L В.

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

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

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