1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Daniel Schepler Oct 11 '17 at 22:56
  • $\begingroup$ Sure, go ahead with it! I've not learnt it yet, but I think I'll be able to follow a proof. $\endgroup$ – SSF Oct 11 '17 at 23:00
2
$\begingroup$

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

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.