Logic – How to Prove Hilbert Style Proofs in Propositional Logic

formal-proofslogicpropositional-calculus

I'm very new to classical propositional logic, and my lecturer is using a system with the following axioms:

A1. X→(Y→X)

A2. (X→(Y→Z))→((X→Y)→(X→Z))

A3. (¬Y→¬X)→(X→Y)

Use uniform substitution and Modes Ponens (MP) as rule of inference. Deduction Theorem also allowed.

I'd like to deduce the following:

(a) X, Y ⊢ ¬(X→(¬Y)) (conjunction, but expressed in terms of NOT and IMPLIES)

(b) X→((X→Y)→Y)

(c) (X→Y)→(((¬Y)→X)→Y)

(d) (((¬Y)→X)→Y)→(X→Y)

Remark: The last two are to show that the axiom (A3) can be replaced with a different axiom:

B3. (¬Y→¬X)→(((¬Y)→X)→Y).

Solution: Bram28 proves (b) and (c) below. I demonstrate (a) and (d).

(d) is alright; first, I claim that X, ((¬Y→X)→Y) ⊢ Y.

Axiom (A1) gives ⊢X→(¬Y→X) so that ((¬Y→X)→Y)⊢X→Y by Hypothetical Syllogism (HS), which Bram28 shows to be valid.

Now that we have ((¬Y→X)→Y)⊢X→Y just apply the deduction theorem to get what we want: ⊢((¬Y→X)→Y)→(X→Y).

(a) is slightly trickier.
Axiom (A1) gives ⊢ Y→(X→Y) so that X, Y ⊢ (X→Y).

Next, by part (b), we have as a theorem that ⊢X→((X→¬Y)→¬Y).

Therefore X, Y ⊢(X→¬Y)→¬Y.

But ⊢(¬¬(X→¬Y))→(X→¬Y) by DN Elim, which Bram28 shows to be valid.

By HS, X, Y ⊢(¬¬(X→¬Y))→¬Y.

By Axiom (A3) and MP, X, Y ⊢(Y→¬(X→¬Y)).

Also, rather trivially X, Y ⊢Y.

Finally by MP we conclude X, Y ⊢¬(X→¬Y) as required.

Best Answer

Just as an example of how to use the Deduction Theorem, let me do b)

First, let's show that $X, X \rightarrow Y \vdash Y$:

  1. $X$ Premise

  2. $X \rightarrow Y$ Premise

  3. $Y$ MP 1,2

OK, so we have $X, X \rightarrow Y \vdash Y$

By the Deduction Theorem, we thus have $X \vdash (X \rightarrow Y) \rightarrow Y$

And applying the Deduction Thorem on that, we get $\vdash X \rightarrow ((X \rightarrow Y) \rightarrow Y)$

Now, the others aren't quite so easy, but here are some useful derivations thay may help:

Let's prove: $\phi \to \psi, \psi \to \chi, \phi \vdash \chi$:

  1. $\phi \to \psi$ Premise

  2. $\psi \to \chi$ Premise

  3. $\phi$ Premise

  4. $\psi$ MP 1,3

  5. $\chi$ MP 2,4

By the Deduction Theorem, this gives us Hypothetical Syllogism (HS): $\phi \to \psi, \psi \to \chi \vdash \phi \to \chi$

Now let's prove the general principle that $\neg \phi \vdash (\phi \to \psi)$:

  1. $\neg \phi$ Premise

  2. $\neg \phi \to (\neg \psi \to \neg \phi)$ Axiom1

  3. $\neg \psi \to \neg \phi$ MP 1,2

  4. $(\neg \psi \to \neg \phi) \to (\phi \to \psi)$ Axiom3

  5. $\phi \to \psi$ MP 3,4

With the Deduction Theorem, this means $\vdash \neg \phi \to (\phi \to \psi)$ (Duns Scotus Law)

Let's use Duns Scotus to show that $\neg \phi \to \phi \vdash \phi$

  1. $\neg \phi \to \phi$ Premise

  2. $\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))$ (Duns Scotus Law)

  3. $(\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))) \to ((\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi)))$ Axiom2

  4. $(\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi))$ MP 2,3

  5. $\neg \phi \to \neg (\neg \phi \to \phi)$ MP 1,4

  6. $(\neg \phi \to \neg (\neg \phi \to \phi)) \to ((\neg \phi \to \phi) \to \phi)$ Axiom3

  7. $(\neg \phi \to \phi) \to \phi$ MP 5,6

  8. $\phi$ MP 1,7

By the Deduction Theorem, this means $\vdash (\neg \phi \to \phi) \to \phi$ (Law of Clavius)

Using Duns Scotus and the Law of Clavius, we can now show that $ \neg \neg \phi \vdash \phi$:

  1. $\neg \neg \phi$ Premise

  2. $\neg \neg \phi \to (\neg \phi \to \phi)$ Duns Scotus

  3. $\neg \phi \to \phi$ MP 1,2

  4. $(\neg \phi \to \phi) \to \phi$ Law of Clavius

  5. $\phi$ MP 3,4

By the Deduction Theorem, this also means that $\vdash \neg \neg \phi \to \phi$ (DN Elim)

Now we can prove $\vdash \phi \to \neg \neg \phi$ (DN Intro) as well:

  1. $\neg \neg \neg \phi \to \neg \phi$ (DN Elim)

  2. $(\neg \neg \neg \phi \to \neg \phi) \to (\phi \to \neg \neg \phi)$ Axiom 3

  3. $\phi \to \neg \neg \phi$ MP 1,2

Now we can derive Modus Tollens: $\phi \to \psi, \neg \psi \vdash \neg \phi$:

  1. $\phi \to \psi$ Premise

  2. $\neg \psi$ Premise

  3. $\neg \neg \phi \to \phi$ DN Elim

  4. $\neg \neg \phi \to \psi$ HS 1,3

  5. $\psi \to \neg \neg \psi$ DN Intro

  6. $\neg \neg \phi \to \neg \neg \psi$ HS 4,5

  7. $(\neg \neg \phi \to \neg \neg \psi) \to (\neg \psi \to \neg \phi)$ Axiom3

  8. $\neg \psi \to \neg \phi$ MP 6,7

  9. $\neg \phi$ MP 2,8

By the Deduction Theorem this gives us $\phi \to \psi \vdash \neg \psi \to \neg \phi$ (Contraposition)

And if we apply the Deduction Theorem on Contradiction, we get $\vdash (\phi \to \psi) \to (\neg \psi \to \neg \phi)$.

Finally, we can prove $\phi \to \psi, \neg \phi \to \psi \vdash \psi$:

  1. $\phi \to \psi$ Premise

  2. $\neg \phi \to \psi$ Premise

  3. $\neg \psi \to \neg \phi$ Contraposition 1

  4. $\neg \psi \to \psi$ HS 2,3

  5. $(\neg \psi \to \psi) \to \psi$ Law of Clavius

  6. $\psi$ MP 4,5

Now we can apply the Deduction Theorem twice, and get:

$\vdash (\phi \to \psi) \to ((\neg \phi \to \psi) \to \psi)$

Related Question