Логика высказываний с одной схемой аксиом

[revenalp]

Как доказать, что все тавтологии логики высказываний с Modus Ponens и двумя связками: $\neg$ и $\vee$ могут быть выведены из одной схемы аксиом:
$\neg(\neg (\neg A\vee B)\vee (C\vee (D\vee E)))\vee (\neg (\neg D\vee A)\vee (C\vee (E\vee A)))$?
Подозреваю, что из этой схемы нужно получить три стандартные схемы логики высказываний, из которых доказуемо всё остальное.
Подозреваю, что действовать нужно подстановкой. Например, из данной схемы я могу вывести такую схему:
$\neg(\neg C\vee (\neg A\vee B))\vee(\neg (\neg D\vee A)\vee ((E\vee A)\vee(\neg A\vee B)))$
Но в каком направлении копать, чтобы доказать, скажем, $\neg(A\vee A)\vee A$?

Оригинальную статью с доказательством отыскать не могу:
Meredith Carew A.. Single axioms for the systems (C, N), (C, O) and (A, N) of the two-valued propositional calculus. The journal of computing systems, vol. 1 no. 3 (1953), pp. 155–164.

[arseniiv]

Одной только подстановкой в общем случае не обойтись, нужны нетривиальные выводы с использованием MP. Ничего полезного подсказать не могу кроме попыток двигаться в обратную сторону от того, что нужно вывести — если $\dfrac{A,\; B}{C}\,\mathsf{MP}$, то $A\equiv\neg B\vee C$ (или $B\equiv \neg A\vee C$, но ничего нового альтернатива, конечно, не даст, так что можно ограничиваться первой).

Допустим, хотим доказать $\neg A\vee(\neg B\vee A)$. Аксиомой это явно не является, так что должны быть выведены формулы $X_2\equiv\neg X_1\vee(\neg A\vee(\neg B\vee A))$ и $X_1$. Можно попробовать решить, что $X_2$ — это какая-то подстановка в $\neg(\neg D\vee A)\vee(C\vee(E\vee A))$ (правая часть аксиомы). Может получиться, может нет.

Ещё можно попытаться подставлять что-то одинаковое и смотреть, не выводится ли какая-то полезная для будущего вещь.

Вообще, конечно, полезнее всего, если за видом этой аксиомы стоят какие-то соображения, и они известны. Знал бы — поделился, а с наскоку не видно. Раз логика классическая, можно заменить для проверки все $\neg a\vee b$ на $a\to b$ и $a\vee b$ на $\neg a\to b$ и глянуть, не получается ли что-то более внятное.

На Metamath нашлась аксиома этого же автора, но, увы, другая.

-- Вс дек 04, 2016 00:02:16 --

Впрочем, какая-то часть раздела Other axiomatizations of classical propositional calculus вам, возможно, пригодится.

[Source]

Посмотрите ссылку. Там, правда, базовые связки - отрицание и импликация.
http://us.metamath.org/mpegif/mmtheorems15.html