Give a proof that "p & ~p" implies "q"?

Question

Context: This is not a textbook or homework problem. I was hoping you younger folks could help my tired old brain. "Everybody knows" a contradiction implies anything. What I'm looking for is a specific proof of the conclusion "q" from the premise "p & ~p", in some widely used proof theory for propositional logic.

The use of truth tables is not allowed, since I call that model theory. And no tricks like taking what's to be proved as one of your axioms, on the grounds that it's valid. A proof in an axiomatic system would be preferred, but a natural deduction proof is fine too. Please give a reference to a text or website that sets out the proof theory in full.

I do actually need this for something I'm working on. Thanks for your help.

Answer 1

You can see in Elliott Mendelson, Introduction to Mathematical Logic (4th ed - 1997), page 38, the Lemma 1.11.c [see page 39 for the derivation] :

$\vdash \lnot \mathcal B \rightarrow (\mathcal B \rightarrow \mathcal C)$.

It is the "basic building block" for proving in an Hilbert-style proof system (axioms + modus ponens) the Ex Falso Quodlibet.

In Natural Deduction, you can use the so-called $\lnot$-elimination rule (from $A$ and $\lnot A$, infer $\bot$, i.e. the falsum) followed by the Abs-rule (from $\bot$, infer $B$ whatever) to derive from a contradiction a formula wathever [you can see the discussion about the DN rules involving $\lnot$ and $\bot$ in this post].

Note.

This is Mendelson's axiom system :

(A1) $\mathcal{B} \rightarrow ( \mathcal{C} \rightarrow \mathcal{B})$

(A2) $(\mathcal{B} \rightarrow ( \mathcal{C} \rightarrow \mathcal{D})) \rightarrow ((\mathcal{B} \rightarrow \mathcal{C}) \rightarrow (\mathcal{B} \rightarrow \mathcal{D}))$

(A3) $(\lnot \mathcal{C} \rightarrow \lnot \mathcal{B}) \rightarrow ((\lnot \mathcal{C} \rightarrow \mathcal{B}) \rightarrow \mathcal{C})$.

With (A1) and (A2) he proves Lemma 1.8 [page 36] :

$\vdash \mathcal{B} \rightarrow \mathcal{B}$.

With the help of Lemma 1.8 and using only (A1) and (A2) it is possible to prove the Deduction Theorem [Prop 1.9, page 37]:

if $\Gamma, \mathcal{B} \vdash \mathcal{C}$, then $\Gamma \vdash \mathcal{B} \rightarrow \mathcal{C}$.

Finally, Mendelson proves Lemma 1.11.c :

$\vdash \lnot \mathcal B \rightarrow (\mathcal B \rightarrow \mathcal C)$.

Without DT we may still have ex falso quodlibet as a "derived rule" :

(1) $\quad \lnot \mathcal B$ --- assumed

(2) $\quad \mathcal B$ --- assumed

(3) $\quad \vdash \mathcal B \rightarrow ( \lnot \mathcal C \rightarrow \mathcal B )$ --- (A1)

(4) $\quad \vdash \mathcal{\lnot B} \rightarrow ( \mathcal{\lnot C} \rightarrow \mathcal{\lnot B})$ --- (A1)

(5) $\quad \mathcal{\lnot C} \rightarrow \mathcal B$ --- from (2) and (3) by modus ponens

(6) $\quad \mathcal{\lnot C} \rightarrow \mathcal{\lnot B}$ --- from (1) and (4) by modus ponens

(7) $\quad \vdash (\lnot \mathcal{C} \rightarrow \lnot \mathcal{B}) \rightarrow ((\lnot \mathcal{C} \rightarrow \mathcal{B}) \rightarrow \mathcal{C})$ --- (A3)

(8) $\quad \mathcal{C}$ --- from (5), (6) and (7) by modus ponens twice.

Thus :

$\quad \lnot \mathcal B, \mathcal B \vdash \mathcal C$.

In Mendelson's system, $\land$ and $\lor$ are not primitive; they are defined as :

$p \land q =_{def} \lnot (p \rightarrow \lnot q)$

$p \lor q =_{def} \lnot p \rightarrow q$

Having the Deduction Theorem, Mendelson proves a couple of other useful results [see Corollary 1.10, page 38] and then Lemma 1.11 including :

$\vdash \lnot \lnot \mathcal B \rightarrow \mathcal B$ --- Lemma 1.11.a

and

$\vdash \mathcal B \rightarrow \lnot \lnot \mathcal B$ --- Lemma 1.11.b.

Now we have :

(a)$\quad \vdash \mathcal B \rightarrow \lnot \lnot \mathcal B$ --- Lemma 1.11.b

(b)$\quad \vdash \lnot \lnot (\mathcal B \rightarrow \lnot \lnot \mathcal B)$ --- from Lemma 1.11.b "applied to itself" by modus ponens

(c)$\quad \vdash \lnot (\mathcal B \land \lnot \mathcal B)$ --- with definition of $\land$

(d)$\quad \vdash \lnot (\mathcal B \land \lnot \mathcal B) \rightarrow ((\mathcal B \land \lnot \mathcal B) \rightarrow \mathcal C)$ --- Lemma 1.11c with the substitution of $(\mathcal B \land \lnot \mathcal B)$ in place of $\mathcal B$.

Thus :

$\vdash \mathcal B \land \lnot \mathcal B \rightarrow \mathcal C$ --- from (c) and (d) by modus ponens.

Further reading.

You can usefully see the note by Peter Smith on Types of proof system in his Logic Matters blog.

Answer 2

I read this on Wikipedia maybe, but I can't find a source now.

Given: $p$ and $\overline p$ are true.

To prove: $q$

$$p\lor q =True\tag{vacuosly since $p$ is true}$$

But $\overline{p}$ is true, $\implies p$ is false. $$false \lor q = True \implies q=True$$

Answer 3

I use Polish notation.

Since you want something widely used (there exists systems which get less used which you might find more interesting for certain purposes), I'll use the axiom system referenced by Wikipedia. It's axioms are

3 CCpCqrCCpqCpr.

4 CpCqp.

5 CCNpNqCqp.

The system also has definitions for other connectives. You won't find all definitions of all of the other binary and unary connectives in most logic textbooks, and they aren't needed here. The relevant definition that we need for this problem is:

1. C $\delta$ NCpNq $\delta$ Kpq,

where $\delta$ is a variable functor of one argument.

You've asked for a proof of KpNp $\vdash$ q. Due the deduction metatheorem and its converse, if KpNp $\vdash$ q, then CKpNpq. Also, if CKpNpq, then KpNp $\vdash$ q. Now the definition tells us that if we can prove CNCpNNpq, that CKpNpq can follow. I use the notation Dx.y * z for condensed detachment with x as the major premise, y as the minor premise, and "z" as the resulting formula. I'll also write the annotation of the proof before the proof. So, here's a proof:

D3.3 * 7

7 CCCpCqrCpqCCpCqrCpr

D4.4 * 8

8 CpCqCrq

D3.4 * 9

9 CCpqCpp

D4.3 * 10

10 CpCCqCrsCCqrCqs

D4.5 * 11

11 CpCCNqNrCrq

D7.8 * 12

12 CCpCCqprCpr

D4.8 * 13

13 CpCqCrCsr

D9.5 * 14

14 Cpp

D3.14 * 15

15 CCCpqpCCpqq

D7.13 * 16

16 CCpCCqCrqsCps

D3.11 * 17

17 CCpCNqNrCpCrq

D12.11 * 18

18 CNpCpq

D12.10 * 19

19 CCpqCCrpCrq

D4.18 * 20

20 CpCNqCqr

D3.18 * 21

21 CCNppCNpq

D15.20 * 22

22 CCCNpCpqrr

D16.19 * 23

23 CCCpqrCqr

D23.21 * 24

24 CpCNpq

D22.17 * 25

25 CNNpCqp

D16.25 * 26

26 CNNpp

D5.26 * 27

27 CpNNp

D24.27 * 28

28 CNCpNNpq

Now in 1. we substitute $\delta$ with C'r, where the apostrophe [ ' ] indicates the wff which immediately follows $\delta$ in 1 (NCpNq, and Kpq respectively) obtaining 29.

29 CCNCpNqrCKpqr

Finally D29.28 yields

30 CKpNpq.

Now assume KpNp as a premise. Thus, by detachment and 30 we obtain q as a conclusion. Thus, we have KpNp $\vdash$ q as a meta-theorem.