Правила для конъюнкции и импликации

G |– F G |– G (В&)     G |– F & G	G |– F & G (У&)     G |– F     G |– F & G   G |– G
G È { F } |– G (ВÉ)     G |– F É G	G |– F G |– FÉ G (УÉ)     G |– G

В каждом из этих пяти правил вывода, одно или два выражения над горизонтальной чертой представляют ``посылки'', к которым правило может быть применено, и выражение под чертой представляет ``заключение'' которое выводится по этому правилу. Правила В& и ВÉ – ``правила введения'' конъюнкции и импликации; У& и УÉ – ``правила удаления''. Подставляя конкретные формулы вместо метапеременных F и G и конкретные конечные множества формул вместо метапеременной G некоторое правило вывода, мы получаем пример этого правила. Например,

{q, r} |– p {p Ú q, r} |– ¬q

{q, r, p Ú q} |– p & ¬q

есть пример правила введения конъюнкции.

Пример простого вывода. Выведем формулу q из посылки p & q. Этот вывод получается за один шаг с помощью второго правила удаления конъюнкции.

Дата добавления: 2014-02-26; просмотров: 577; Нарушение авторских прав

Мы поможем в написании ваших работ!