Формулы вывода основание

1. (A ((A A) A)) A _1; { A A/B }.

2. ((A ((A A) A)) ((A A) A)) A ₂; { A A/B, A/C }.

3. ((A (A A)) (A A)) MP; 1,2.

4. A (A A) A ₁; A/B.

5. A A MP; 4,3.

Теорема 4.10. A _{├ L} B A

Доказательство

1. A на основаниигипотезы.

2. A (B A) на основании A ₁.

3. B A на основании MP; 1,2.

 

Всякую доказанную выводимость можно использовать как новое (производное) правило вывода. Например, последняя доказанная выводимость называется правилом введения импликации:

Дедукция

В теории L импликация очень тесно связана с выводимостью.

Теорема 4.11. (дедукции) Если Г, A _{├ L} B, то Г _{├ L} A B и обратно.

Доказательство

Прямой вывод. Пусть E ₁,..., Е_п — вывод В из Г, А. Е_п = В. Индукцией по i покажем, что _{├ L} A Е_i. Тем самым теорема будет доказана. База: i = 1. Возможны три случая.

1. Пусть E ₁ — аксиома. Тогда рассмотрим вывод E ₁, E ₁ (А E ₁ ), A E ₁. Имеем Г _{├ L} A E ₁.

2. Пусть E ₁ Г. Тогда рассмотрим вывод E ₁ ,E ₁ (А E ₁ ), A E ₁. Имеем Г _{├ L} A E ₁.

3. Пусть E ₁ = А. Тогда по первой теореме предыдущего раздела _{├ L} E ₁ E ₁, а значит _{├ L} A E ₁.

В любом случае Г _{├ L} A E ₁. Таким образом, база индукции доказана. Пусть теперь Г _{├ L} A E ₁ для всех i < k. Рассмотрим E_k. Возможны четыре случая: либо E_k — аксиома, либо E_k Г, либо E_k = А, либо формула E_k получена по правилу Modus po­nens из формул E_i и E_j, причем i, j < k и E_j = E_i E_k. Для первых трех случаев имеем Г _{├ L} A E_k аналогичным образом. Для четвертого случая по индукционному предположению имеется вывод Г _{├ L} A E_i и вывод Г _{├ L} A (E_i E_k). Объединим эти выводы и достроим следую­щий вывод: