The system L0 is defined as follows:

Axioms: A1 (α → (β → α))

A2 ((α → (β → γ)) → ((α → β) → (α → γ)))

A3 ((¬β → ¬α) → (α → β))

The only rule of inference is Modus Ponens: MP From α and (α → β) infer β.

In one of my problem sheets, I am told that I am allowed to use the following theorem: if ⊢ (α → β) and ⊢ (¬α → β) then ⊢ β

I am wondering if it is possible to prove this within the system? We've proved the Deduction Theorem, but I don't think its obviously useful here. I want to say something like "either a is true or ¬α is true" but this is not the sort of proof that was given for DT - however, without this sort of reasoning, I'm struggling to see an obvious way of proving the theorem.

Is it provable? And if so, can you point me in the right direction?

Thanks a lot!

  • $\begingroup$ I'm not sure if this is necessary, but is $\lnot \alpha$ an abbreviation for $\alpha \to \bot$ in your system? (so you can use A1 and A2 to reason about $\lnot \alpha$ as well). $\endgroup$ – Magdiragdag Aug 22 '17 at 18:30
  • $\begingroup$ What you are calling "Lo" is the hilbert system. It is complete wrt classical propositional logic and satisfies the deduction theorem. In other words, anything you can prove with truth tables can be proven with "Lo", although it may be very convoluted. $\endgroup$ – DanielV Aug 22 '17 at 20:35

Yes, we can, but it's a bit of work! (well, I myself couldn't find any shorter way ...)

First, 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)$ A1

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

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

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

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

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

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

  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)

(historical sidenote: if we apply the Deduction Theorem on Contraposition, we get $\vdash (\phi \to \psi) \to (\neg \psi \to \neg \phi)$ , which is one of the axioms used by Frege ... Frege also used DN Intro and DN Elim as axioms, but Lukaciewicz figured out how to derive all these three using A3).

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

Or, we can apply the Deduction Theorem twice to get it in its conditionalized form:

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

So yes, this certainly means that if $\vdash \alpha \to \beta$ and $\vdash \neg \alpha \to \beta$, then$\vdash \beta$

  • $\begingroup$ Not only was this comment very helpful with the given question, its given me a lot of intuition on the subject and a backlog of proofs for other questions! Thanks so much! $\endgroup$ – Maths That Imo Aug 23 '17 at 9:46
  • $\begingroup$ @MathsThatImo Cool, glad I could help! And yes, I learned all this through self-study, and it took me a while to get to this point ... I found that most texts are really quite unhelpful in showing how to actually work with this system, and merely point out the axioms, the Deduction Theorem, and a passing mention of completeness, but if you actually try to prove something, more often than not you're quickly stuck. I am still building my 'backlog'! :) $\endgroup$ – Bram28 Aug 23 '17 at 13:16
  • $\begingroup$ Yeah I've definitely payed attention to this. Do you have any recommendations on texts that don't have that flaw, or just on whichever text you found the most useful? Thanks a lot! $\endgroup$ – Maths That Imo Aug 23 '17 at 13:41
  • 1
    $\begingroup$ @MathsThatImo I really don't have one textbook :( I had to piece things together from various places. One website I did helpful is metamath.org, though it takes a bit of time to piece it together from that site as well. But I also found bits and pieces on this very Math.SE community site. $\endgroup$ – Bram28 Aug 23 '17 at 14:21

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.