Question:
I am developing the proof for the following exercise from An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof by Peter B. Andrews:
X1102. Let $\mathscr{M}$ be the system which has the same wffs and rule of inference as $\mathscr{P}$, and the single axiom schema
$$\left[\mathbf{A} \supset \mathbf{B} \supset { }_\blacksquare \mathbf{C} \vee { }_\blacksquare \mathbf{D} \vee \mathbf{E} \right] \supset { }_\blacksquare \mathbf{D} \supset \mathbf{A} \supset { }_\blacksquare \mathbf{C} \vee { }_\blacksquare \mathbf{E} \vee \mathbf{A}$$
Show that each theorem of $\mathscr{P}$ is a theorem of $\mathscr{M}$.
Beginning of a Proof:
Start with a theorem $\mathbf{X}$ of $\mathscr{P}$. I want to prove that $\mathbf{X}$ is also a theorem of $\mathscr{M}$. To do so, look at the proof $\mathbf{X}_1 \ldots \mathbf{X}_n$ in $\mathscr{P}$ of $\mathbf{X}$ from the empty set. Consider $\mathbf{X}_i$ for some $i$ with $1 \leq n$. We need to prove by induction on $i$ that $\mathbf{X}_i$ has a proof in $\mathscr{M}$.
From the definition of a proof in $\mathscr{P}$, there are three cases to consider: (1) $\mathbf{X}_i$ is an axiom, (2) $\mathbf{X}_i$ is a member of the empty set, and (3) $\mathbf{X}_i$ inferred by modus ponens from $\mathbf{X}_j$ and $\mathbf{X}_k$ where $j < i$ and $k < i$. Condition (2) is never true for any $\mathbf{X}_i$ and (3) follows from a trivial inductive argument.
Condition (1) is where I am struggling. Since $\mathscr{P}$ has three axiom schemata (see details below), I need to find a proof of each from the single axiom of $\mathscr{M}$. I'm not certain how to proceed from here. Am I even heading in the right direction? Should I look at proving any intermediary lemmas?
Definitions:
For clarification, here are the definitions with which I am working from the text. First, the syntactic and axiomatic structure of $\mathscr{P}$:
Definition. The set of wffs is the intersection of all sets $\mathscr{S}$ of formulas such that:
(i) $\mathbf{p} \in \mathscr{S}$ for each propositional variable $\mathbf{p}$.
(ii) For each formula $\mathbf{A}$ if $\mathbf{A} \in \mathscr{S}$, then $\mathord{\sim} \mathbf{A} \in \mathscr{S}$.
(iii) For all formulas $\mathbf{A}$ and $\mathscr{B}$, if $\mathbf{A} \in \mathscr{S}$ and $\mathbf{B} \in \mathscr{S}$, then $\left[\mathbf{A} \lor \mathbf{B} \right] \in \mathscr{S}$.
Axioms.
(1) $\mathord{\sim} \left[ \mathbf{A} \vee \mathbf{A} \right] \vee \mathbf{A}$
(2) $\mathord{\sim} \mathbf{A} \vee {}_\blacksquare \mathbf{B} \vee \mathbf{A}$
(3) $\mathord{\sim} \left[ \mathord{\sim} \mathbf{A} \vee \mathbf{B} \right] \vee {}_\blacksquare \mathord{\sim} \left[ \mathbf{C} \vee \mathbf{A} \right] \vee {}_\blacksquare \mathbf{B} \vee \mathbf{C}$
Defining $\supset$ as $\mathbf{A} \supset \mathbf{B}$ stands for $\mathord{\sim} \mathbf{A} \vee \mathbf{B}$, we can write these axioms as
(1) $\mathbf{A} \vee \mathbf{A} \supset \mathbf{A}$
(2) $\mathbf{A} \supset {}_\blacksquare \mathbf{B} \vee \mathbf{A}$
(3) $\mathbf{A} \supset \mathbf{B} \supset {}_\blacksquare \mathbf{C} \vee \mathbf{A} \supset {}_\blacksquare \mathbf{B} \vee \mathbf{C}$
$\mathscr{P}$ has one rule of inference:
Modus Ponens (MP). From $\mathbf{A}$ and $\mathord{\sim} \mathbf{A} \vee \mathbf{B}$ to infer $\mathbf{B}$.
More definitions needed to solve the exercise:
Def1. A proof of a wff $\mathbf{B}$ from the set $\mathscr{H}$ of hypotheses is a finite sequence $\mathbf{B}_1,\ldots,\mathbf{B}_m$ of wffs such that $\mathbf{B}_m$ is $\mathbf{B}$ and for each $j$ ($1 \leq j \leq m$) at least one of the following conditions is satisfied:
(1) $\mathbf{B}_j$ is an axiom.
(2) $\mathbf{B}_j$ is an member of $\mathscr{H}$.
(3) $\mathbf{B}_j$ is inferred by modus ponents from wffs $\mathbf{B}_i$ and $\mathbf{B}_k$, where $i < j$ and $k < j$.
Def2. A proof of a wff $\mathbf{B}$ is a proof of $\mathbf{B}$ from the emtpy set of hypotheses.
Def3. A theorem is a wff which has a proof.
