Так формулируется теорема дедукции для ИВ в Мендельсоне:
Мендельсон писал(а):
Предложение 1.8. (Теорема дедукции). Если

- множество формул,

- формулы и

, то

.
Однако не утверждается, что верно обратное: если

, то

. Думаю, что это верно:
Док-во: Пусть

, докажем, что

.

означает, что есть вывод

из

. Построим вывод:
1.

(гипотеза)
2.

(следует из 1 по условию)
3.

(гипотеза)
4.

(MP из 2. и 3.)
Значит

.
(ну тупо, конечно, но так надо) (аксиомы не использовал, только MP)
Вот сразу после доказательства идет следствие 1.9 (которое я счел следствием предложения 1.8).
Мендельсон писал(а):
Следствие 1.9. (i)

...
Доказательство (i):
1.

(гипотеза)
2.

(гипотеза)
3.

(гипотеза)
4.

(MP из 1. и 3.)
5.

(MP из 2. и 4.)
Ну и собственно вопрос: я в упор понять не могу, каким образом из теоремы дедукции и 1 и 2 следует 3. И думаю, что 3 следует из 1 и из обратной теоремы дедукции (которую я на всякий случай доказал, чтоб было видно, что доказательство возможно), а теорема дедукции тут вообще не нужна.
Правильно?
