Short proof of the principle of explosion in propositional calculus

logicpropositional-calculus

I am working through 'Notes on logic and set theory' by P.T. Johnstone. Exercise 2.2 reads

Write down a proof of ($\bot\Rightarrow q$) in the propositional calculus.

Here $q$ is an arbitrary primitive proposition and 'proof' means deduction from the axioms

(a) $(p \Rightarrow (q\Rightarrow p))$

(b) $((p \Rightarrow (q\Rightarrow r)) \Rightarrow ((p \Rightarrow q) \Rightarrow (p \Rightarrow r)))$

(c) $(\neg\neg p \Rightarrow p)$

and modus ponens. Here is my solution:

Instead of proving that $\,\,\vdash (\bot \Rightarrow q)$ we prove that $\{\bot\}\vdash q$. This is easy:

  1. $\bot$ —– premiss

  2. $(\bot \Rightarrow ((q\Rightarrow \bot)\Rightarrow \bot))$ —– instance of (a)

  3. $((q\Rightarrow \bot) \Rightarrow \bot)$—– modus ponens

  4. $(((q\Rightarrow \bot )\Rightarrow \bot) \Rightarrow q)$ —– instance of (c)

  5. $q$ —– modus ponens

Then the Deduction theorem finishes the job. (The Deduction theorem says that if $S$ is a set of propositions and $s,t$ are propositions then $S\vdash (s\Rightarrow t)$ if and only if $S\cup \{s\}\vdash t$.)

I am unsatisfied, however, since I did not explicitly write down the proof of $(\bot \Rightarrow q)$. I tried to do this by following the algorithm given in the proof of the Deduction theorem (see Theorem 2.4 in Johnstone's book) but it turned into a mess, so I gave up. My question:

Is there a short proof of $\,\,\vdash (\bot \Rightarrow q)$, like that of $\{\bot\}\vdash q$?

Best Answer

To save us from parenthesis hell, let's follow the proof-theory convention of writing $P \rightarrow (Q \rightarrow R)$ as $P \rightarrow Q \rightarrow R$.

We can write down a short, seven-line proof as follows:

  1. $\neg\neg x \rightarrow x$ [axiom C]
  2. $(\neg\neg x \rightarrow x) \rightarrow \bot \rightarrow (\neg\neg x \rightarrow x)$ [axiom A]
  3. $\bot \rightarrow \neg\neg x \rightarrow x$ [MP 2,3]
  4. $(\bot \rightarrow \neg\neg x \rightarrow x) \rightarrow (\bot \rightarrow \neg\neg x) \rightarrow \bot \rightarrow x$ [axiom B]
  5. $(\bot \rightarrow \neg\neg x) \rightarrow \bot \rightarrow x$ [MP 3,4]
  6. $\bot \rightarrow \neg\neg x$ [axiom A]
  7. $\bot \rightarrow x$ [MP 6,5]

How can one find this proof? I first inspected your proof, which uses the deduction theorem, and took note of the key step: $\bot \rightarrow \neg\neg x$ constitutes instance of axiom A. I knew that one can get $(\bot \rightarrow \neg\neg x) \rightarrow \bot \rightarrow x$ cheaply from $\neg\neg x \rightarrow x$ using a standard trick coming from the proof of the deduction theorem: I use this trick with some frequency, see e.g. another Hilbert system question. This is where the first four lines come from.

This is certainly an improvement over the 17 lines obtained by naive use of the deduction theorem. I don't know whether one can get anything even shorter.

Related Question