логистическая система, индукция

[gefest_md]

Пусть дана система аксиом:
$p\supset[q\supset p]$
$[s\supset[p\supset q]]\supset[[s\supset p]\supset[s\supset q]]$
и два правила вывода: модус поненс и подстановка.

Первичная задача такая: Надо доказать, что в этой системе формула $\mathbf A$ является теоремой тогда и только тогда, когда $\mathrm S^f_{\mathrf a}\mathbf A\!\mid$ - теорема, где $\mathbf A$ это произвольная формула содержащая константу $f$ и не содержащая переменную $\mathbf a$, а формула $\mathrm S^f_{\mathbf a}\mathrf A\!\mid$ это результат замены в $\mathbf A$ константы $f$ на переменную $\mathbf a$.

Начал доказывать индукцией по длине доказательства формулы $\mathbf A$ (посмотрел у Клини теорему дедукции). И не знаю если можно так. Часть доказательства в которой нет уверенности выглядит примерно так:

Пусть $\mathbf A$ получается из двух ранее доказанных теорем $\mathbf A_1$ и $\mathbf A_1\supset\mathbf A$ по модус поненс. По индуктивному предположению:
$\mathrm S^f_{\mathbf a}\mathbf A_1\!\mid$
$\mathrm S^f_{\mathbf a}(\mathbf A_1\supset\mathbf A)\!\mid$
Из второй получится
$\mathrm S^f_{\mathbf a}\mathbf A_1\!\mid\supset\mathrm S^f_{\mathbf a}\mathbf A\!\mid$
Отсюда по модус поненс
$\mathrm S^f_{\mathbf a}\mathbf A\!\mid$

Теперь пусть $\mathbf A$ получается из ранее доказанной теоремы $\mathbf A_1$ по правилу подстановки, т.е. $\mathbf A$ есть $\mathrm S^{\mathbf c}_{\mathbf b}\mathbf A_1\!\mid$. $\mathbf c$ не может быть ни $f$, ни $\mathbf a$. По индуктивному предположению $\mathrm S^f_{\mathbf a}\mathbf A_1\!\mid$ - теорема, из которой по подстановке получится теорема $\mathrm S^{\mathbf c}_{\mathbf b}(\mathrm S^f_{\mathbf a}\mathbf A_1)\!\mid$. Это то же, что $\mathrm S^f_{\mathbf a}\mathrm(S^{\mathbf c}_{\mathbf b}\mathbf A_1)\!\mid$, т.е. $\mathrm S^f_{\mathbf a}\mathbf A\!\mid$ - теорема.

Если добавить к сказанному базис начиная с длины 2, будет ли этого достаточно? Можно так доказывать независимость от данных двух аксиом формулы $[[p\supset f]\supset f]\supset p$, либо $f\supset p$?