Правила естественного вывода

Теорема о дедукции. Правила естественного вывода исчисления высказываний. Новые правила:

p1)     Γ⊢XΓ⊢∀yX^xy     (введение общности);

p2) Γ⊢∀x XΓ⊢X^xt     (удаление общности);

p3)   Γ⊢X^xt  Γ⊢∃xX     (введение существования);

p4) Γ,X ⊢YΓ,∃yX^xy⊢Y

Пример: ∃ x X → ¬ ∀ x (¬X ).

Как и в случае исчисления высказываний, на практике вывод строится с помощью правил естественного вывода. Сохраняются структурные правила естественного вывода, так как они не связаны с сутью самого вывода. Сохраняется теорема о дедукции. Однако в доказательство этой теоремы необходимо внести некоторые коррективы.

Теорема 5.1. Если Γ, X ⊢ Y , то Γ ⊢ X → Y .

◀Доказательство теоремы, как и в исчислении высказываний, проводится индукцией по построению формулы. Рассуждения в основном повторяют доказательство теоремы из исчисления высказываний. Дополнительно надо лишь рассмотреть случай, когда конечная формула вывода получена по правилу обобщения.

Итак, пусть в выводе X1, X2, ..., Xi = X, ..., Xj, ..., Xn конечная формула имеет вид Xn = ∀xXj. Предположим в выводе формулы Xj формула X не используется. Тогда Γ ⊢ Xj и Γ ⊢ ∀x Xj . С помощью аксиомы ∀x Xj → (X → ∀x Xj с помощью правила заключения получаем Γ ⊢ X → ∀x Xj . Если формула X используется в выводе формулы Xj , то, согласно структурному ограничению, формула X не имеет свободных вхождении переменной x. Согласно индуктивному предположению из вывода Γ, X ⊢ Xj вытекает вывод Γ ⊢ X → Xj , откуда по правилу обобщения (ни X , ни Xj не содержат свободных вхождений x) получаем Γ ⊢ ∀x (X → Xj ). При- соединив аксиому ∀x(X → Xj) → (X → ∀xXj), получаем вывод формулы X → ∀xXj = X → Y▶

Теорема о дедукции позволяет без изменений перенести в исчисление предикатов все восемь логических правил естественного вывода, а вслед за ними и дополнительные правила естественного вывода: доказательства этих правил не используют правила обобщения. Кроме того, добавляются следующие четыре правила с кванторами (в этих правилах x не имеет свободных вхождений в формулы списка Γ и Y ; если y отлично от x, то y не входит свободно в X):

p1)     Γ⊢XΓ⊢∀yX^xy     (введение общности);

p2) Γ⊢∀x XΓ⊢X^xt     (удаление общности);

p3)   Γ⊢X^xt  Γ⊢∃xX     (введение существования);

p4) Γ,X ⊢YΓ,∃yX^xy⊢Y

При выводе формулы p1 учтем, что формулы списка Γ не содержат переменной x:

Формула p2 непосредственно следует из аксиомы 12:

Аналогично выводится и формула p3:

Наиболее длинный вывод получается для правила p4:

Использование правил естественного вывода такое же, как и в случае исчисления высказываний.

Пример 5.2. Выведем ∃x X → ¬∀x(¬X ). Имеем цепочку преобразований ”снизу вверх“:

∃xX → ¬∀x(¬X) ⇐ ∃xX⊢¬∀x(¬X) ⇐ X^xy ⊢¬∀x(¬X) ⇐ ∀x(¬X)⊢¬X^xy .

Последняя секвенция вытекает из правила p2.