help with some Hilbert style proofs in a propositional logic axiom system.

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.

• Are you allowed to use the deduction theorem (if $P, \Gamma \vdash Q$ then $\Gamma \vdash P \rightarrow Q$)? Without that, direct proofs in a Hilbert-style proof system tend to become very bogged down. – Daniel Schepler Oct 11 '17 at 22:56
• Sure, go ahead with it! I've not learnt it yet, but I think I'll be able to follow a proof. – SSF Oct 11 '17 at 23:00

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)$

• That's great, thanks! (but surely the others don't follow from the DT so trivially?) – SSF Oct 11 '17 at 23:22
• @Tangent You're right, the others are a good bit more difficult ... let me see if I can find a good hint ... – Bram28 Oct 11 '17 at 23:40
• Where did you find these derivations? – DanielV Oct 13 '17 at 5:58
• @DanielV I has some help from the proofs on MetaMath, but mostly it was just trial and error ... – Bram28 Oct 13 '17 at 16:28