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.

-

1 Answer

I'm sure that this sort of single axiom schema for propositional calculus was found by C. Meredith about 50 years ago. Google tells me that his original paper was C. Meredith, Single axioms for the systems (C, N), (C, 0) and (A, N) of the two-valued propositional calculus, Journal of Computing Systems, p. 155-164, 1954. That paper will presumably give proofs that the axioms of some more familiar axiom systems can be derived from the single schema.

However, this is a mere curiosity, and I've never seen any interest in this sort of brainteaser: what's the point? I'd just ignore this exercise in Andrews!

-
 The completionist in me wants to solve this problem. Beyond that, you are probably right. As for the paper, I have been unable to find a copy of it with my googling. Did you find a link? If so, will you please include it in your answer? – Code-Guru Dec 18 '12 at 19:09