В теории £ импликация тесно связана с выводимостью. Теорема дедукции используется при доказательстве теорем, т. к. дает нам новое правило вывода.
Теорема (дедукции). Если Г – множество формул, А и B Î Г и A|-£B, то Г|-А→В.
В частности A|-B, то А→В.
Доказательство. Пусть E1,E2,….En вывод B из Г, A. En = B. Покажем, что Г|-£А→ Ei, .
Пусть i=1.
Возможны 3 случая.
1) Пусть Е1 – аксиома. Тогда рассмотрим вывод:
1. Е1
2. А1: . Выполним замену {А/Е1, В/А}. Получим:
3. Из 1 и 2 по правилу m.p. получаем |-£А→ E1.
2) Пусть Е1Г. Доказательство аналогично 1).
3) Пусть Е1А. Тогда по закону тождества (теорема1) , следовательно,
Таким образом Г.
Пусть i
1) Ek – аксиома.
2) Е1Г.
3) Е1А.
4) Ek получена из формул Ei и Ej по правилу m.p., причем i,j
Для 1), 2), 3) доказательство аналогично доказательству при i=1.
Для 4) случая:
1. (i)
2. (j)
3. А2: . Выполним подстановку {Ei/B, Ek/C}, получим (n)
4. По правилу m.p. из (j) и (n) получаем (n+1)
5. По правилу m.p. из (j) и (n+1) получаем (n+2) ч.т.д.
Таким образом, для любого k, в том числе при k=n. Но En=B Þ .
Схема аксиом A3 теории £ в доказательстве не использовалась, поэтому теорема дедукции имеет место для более широкого класса теорий, чем £.
Следствие 1. Если , то и обратно.
Доказательство. По теореме дедукции, если , то . Пусть Г={0}. Тогда имеем Следствие 1.
Следствие 2. (правило транзитивности).
Доказательство.
1. Гипотеза .
2. Гипотеза с.
3. Гипотеза А.
4. По правилу m.p. из 1 и 3 получаем B.
5. По правилу m.p. из 2 и 4 получаем C
6. Из 1-5 получаем: если , — гипотезы Г, то .
7. По теореме дедукции .
Следствие 3. (правило сечения).
Доказательство.
1. Гипотеза .
2. Гипотеза A.
3. По правилу m.p. из 1 и 2 получим .
4. В – гипотеза.
5. По правилу m.p. из 3 и 4 получим С.
6. Из 1-5 получаем:
7. по теореме дедукции .