2.8. Дедукция

В теории £ импликация тесно связана с выводимостью. Теорема дедукции используется при доказательстве теорем, т. к. дает нам новое правило вывода.

Теорема (дедукции). Если Г – множество формул, А и B Î Г и A|-_£B, то Г|-А→В.

В частности A|-B, то А→В.

Доказательство. Пусть E₁,E₂,….E_n вывод B из Г, A. E_n = B. Покажем, что Г|-_£А→ E_i, .

Пусть i=1.

Возможны 3 случая.

1) Пусть Е₁ – аксиома. Тогда рассмотрим вывод:

1. Е₁

2. А1: . Выполним замену {А/Е1, В/А}. Получим:

3. Из 1 и 2 по правилу m.p. получаем |-_£А→ E₁.

2) Пусть Е₁Г. Доказательство аналогично 1).

3) Пусть Е₁А. Тогда по закону тождества (теорема1) , следовательно,

Таким образом Г.

Пусть i