Пусть Г – множество формул. Запись Г  _L А означает, что существует конечная последовательность формул X_i  Г, , такая, что X₁, X₂, …,X_{n   L} A. Вместо Г{X}  _L А будем писать  Г, X  _L А. Легко видеть, что из Г  _L (АВ) следует существование вывода Г,  А  _L В. Верно и обратное утверждение:

Теорема (о дедукции). Пусть Г – множество формул исчисления L; А и В – формулы, и пусть

Г,  А  _L В.

Тогда Г  _L (АВ). В частности, при пустом Г, из выводимости А  _L В вытекает теорема:    _L АВ.

Доказательство. Пусть В₁, В₂, …, В_n = В – вывод формулы из формул, принадлежащих множеству Г{A}. Докажем с помощью индукции по i, что Г  _L (АВ_i), а затем применим это к i = n, чтобы получить Г  _L (АВ). При i = 1 имеем В₁  Г, либо В₁ = А, либо В₁ – аксиома. Если В₁  Г, либо В₁ – аксиома, тогда получаем с помощью аксиомы  (А1)  формулу  В₁(АВ₁).   Применение MP к  В₁ и В₁ (AВ₁) дает вывод для   АВ₁  из Г.  Если же  В₁ = А, то имеем:   _L (АВ₁) по доказанной лемме о том, что верна теорема   _L АА.

Докажем теперь: Г   _L  (АВ_i) при  i > 1, предполагая, что выводимость Г    _L  (АВ_к) уже доказана для всех k < i.

Для В_i имеем 4 возможности: В_i  Г; В_i – аксиома; В_i = А; В_i непосредственно следует из В_j и В_m, при некоторых j, m  i-1. В первых трёх случаях  Г   _L АВ_i доказывается так же, как при i = 1. В четвёртом случае формула В_m равна формуле (В_jВ_i), и  согласно предположению индукции имеем:

Г   _L (АВ_j)    и     Г  _L (А(В_jВ_i)),

ибо (В_jВ_i)=В_m. По аксиоме (А2) верно   

 _L  (А(В_jВ_i)) ((АВ_j) (АВ_i)).

Применение

MP

приводит к выводу Г    _L  (АВ_j) (АВ_i). Из этого вывода и вывода Г   _L  (АВ_j) с помощью Modus Ponens получаем:

Г    _L  (АВ_i).

Таким образом,  Г    _L  (АВ_i), для всех i = 1,…,n.  В частности, при i = n, получаем:

Г   _L (АВ),

что и требовалось доказать.