How do I prove $(\lnot \beta \to \lnot \alpha) \to (\alpha \to \beta)$ in the four-axiom proof-system described herein?

Question

Show that $(\lnot \beta \to \lnot \alpha) \to (\alpha \to \beta)$ is a theorem, under the proof-system defined by the four axioms and rule of inference stated below. (Note how this is different from the usual three-axiom proof-system - we've replaced $(\lnot \beta \to \lnot \alpha) \to (\alpha \to \beta)$ by axioms (3) and (4)).

So, I tried to use (1) and began with $(\alpha \to \beta) \to ((\lnot \beta \to \lnot \alpha) \to (\alpha \to \beta))$, but couldn't get anywhere from here (got too messy). Could someone please help me get to the solution? Proving theorems using axioms (below) has always been troublesome for me.

List of Axioms:

• $\alpha \to (\beta \to \alpha)$ (1)
• $(\alpha \to (\beta \to \gamma)) \to ((\alpha \to \beta) \to (\alpha \to \gamma))$ (2)
• $\lnot \alpha \to (\alpha \to \beta)$ (3)
• $(\lnot \alpha \to \alpha) \to \alpha$ (4)

and Modus-Ponens is the sole rule of inference.

Answer 1

The thing about proof systems like this one is that you never actually want to write proofs in them. Instead, you usually make use of meta-theorems (like the deduction theorem) to make your life easier. I'll describe a proof using the deduction theorem, which could then in principle be unwound (following the inductive proof of the deduction theorem) into a real (but much longer!) proof in the system.

So what's the strategy for proving $(\lnot \beta\to \lnot \alpha)\to (\alpha\to \beta)$? We want to assume $(\lnot \beta\to \lnot \alpha)$ and prove $(\alpha\to \beta)$. To prove $(\alpha\to \beta)$, we want to assume $\alpha$ and prove $\beta$. Ok, how can we prove $\beta$ based on our assumptions $(\lnot \beta\to \lnot \alpha)$ and $\alpha$? Well, rule (4) gives us a limited method of proof by contradiction. If we want to prove $\beta$, it suffices to prove $(\lnot \beta\to \beta)$. And to prove $(\lnot \beta\to \beta)$, we want to assume $\lnot \beta$ and prove $\beta$. Now we're in business: from our assumptions $(\lnot \beta\to \lnot \alpha)$ and $\lnot \beta$, we get $\lnot \alpha$. Together with our assumption $\alpha$, we should be able to use the principle of explosion to get $\beta$. This is implemented by rule (3): we have $(\lnot \alpha\to (\alpha\to \beta)$, so applying modus ponens twice, we get $\beta$.

Let's turn this strategy into a proof:

1. $(\lnot\beta\to \lnot \alpha)$ (Assumption)
2. $\alpha$ (Assumption)
3. $\lnot \beta$ (Assumption)
4. $\lnot \alpha$ (MP from 1. and 3.)
5. $\lnot \alpha\to (\alpha\to \beta)$ (3)
6. $\alpha\to \beta$ (MP from 4. and 5.)
7. $\beta$ (MP from 2. and 6.)
8. $(\lnot \beta\to \beta)$ (Deduction theorem, discharging Assumption 3.)
9. $(\lnot \beta\to \beta)\to \beta$ (4)
10. $\beta$ (MP from 8. and 9.)
11. $(\alpha\to \beta)$ (Deduction theorem, discharging Assumption 2.)
12. $(\lnot\beta\to \lnot\alpha)\to (\alpha\to \beta)$ (Deduction theorem, discharging Assumption 1.)