I have at my disposal Modus Ponens (MP) and the three axioms:

  • A1: $(\alpha\to(\beta\to\alpha))$,
  • A2: $((\alpha\to(\beta \to\gamma))\to ((\alpha\to\beta)\to(\alpha\to\gamma)))$,
  • A3: $(((\lnot\beta)\to(\lnot\alpha))\to(((\lnot\beta)\to\alpha)\to\beta))$.

I'm trying to prove the Disjunction elimination: $$ \{\alpha\lor\beta,\alpha\to \gamma,\beta\to \gamma\}\vdash \gamma. $$

$\lor$ is not part of the alphabet I use, the deduction actually is: $$ \{((\neg\alpha)\to\beta),\alpha\to \gamma,\beta\to \gamma\}\vdash \gamma. $$

The deduction should be something like

\begin{array}{rl|l} \hline 1:&((\neg\alpha)\to\beta) & Premiss\\ 2:&\beta\to \gamma&Premiss\\ 3:&((\neg\alpha)\to\gamma)&1,2\ H.S.\\ 4:&(\alpha \to \gamma)&Premiss\\ 5:&\gamma& 3,4 [?]\\ \hline \end{array}

Where H.S. is Hypothetical Syllogism, a deduction that I have already proven.

The rule $[?]$, that I have to prove, correspond to $$ \{\alpha\to\beta,(\neg\alpha)\to\beta\}\vdash \beta.\tag{*} $$

(*) looks quite simple, but after hours no way to get it.

For information I have, if needed, proven other results, that I could reuse:

  • $\vdash\alpha\to\alpha$,
  • Hypothetical Syllogism: $\{\alpha\to\beta,\beta\to\gamma\}\vdash\alpha\to\gamma$,
  • $\vdash(\lnot\alpha\to\alpha)\to\alpha$,
  • $\vdash\alpha\lor\lnot\alpha$,
  • $\{\alpha\to(\beta\to\gamma),\beta\}\vdash\alpha\to\gamma$,
  • $\vdash(\neg\neg\alpha)\to\alpha$.
  • Negation introduction: $\{(\alpha\to\beta),(\alpha\to \neg\beta)\}\vdash \neg \alpha$.
  • Negation elimination: $\{\neg \alpha\}\vdash (\alpha\to \beta)$.
  • Double negative elimination: $\neg \neg \alpha\vdash \alpha$.
  • Conjunction introduction: $\{\alpha,\beta\}\vdash (\alpha\land \beta)$.

EDIT Additional known results:

  • $\neg\neg\alpha\vdash\alpha$
  • $\{\alpha,\neg\alpha\}\vdash\neg\beta$
  • $\{\alpha,\neg\alpha\}\vdash\beta$
  • Conjunction elimination, only $\alpha\land\beta\vdash\beta$
  • Disjunction introduction, only $\beta\vdash\alpha\lor\beta$
  • $\begingroup$ It seems easier to me prove modus tollens, which will allow you to do contraposition, i.e. $\neg \alpha \rightarrow \gamma$ is the same as $\neg \gamma \rightarrow \alpha$. Then you do not need your rule $(*)$. Furthermore, modus tollens would probably help you prove $(*)$: If you know $\neg \beta \rightarrow \neg \alpha$ and $\neg \beta \rightarrow \alpha$, then $\neg \beta$ would lead to a contradiction. $\endgroup$ – mrp Apr 26 '18 at 11:51
  • $\begingroup$ @mrp The proof of modus tollens would be also nice to have, sadly I wasn't able to derive it until now $\endgroup$ – PeptideChain Apr 26 '18 at 13:22
  • $\begingroup$ @LiPo Ha! I was in the middle or writing my answer, the first step was the derivation of Modus Tollens! With that, so you're almost there! $\endgroup$ – Bram28 Apr 26 '18 at 13:24

Assuming you are allowed to use the Deduction Theorem:

Let's first prove Modus Tollens: $\varphi \rightarrow \psi, \neg \psi \vdash \neg \varphi$:

  1. $\varphi \rightarrow \psi$ Premise
  2. $\neg \psi$ Premise
  3. $\neg \psi \rightarrow (\neg \neg \varphi \rightarrow \neg \psi)$ A1
  4. $\neg \neg \varphi \rightarrow \neg \psi$ MP 2,3
  5. $\neg \neg \varphi \rightarrow \varphi$ Double Negation Elimination
  6. $\neg \neg \varphi \rightarrow \psi$ H.S. 1,5
  7. $(\neg \neg \varphi \rightarrow \neg \psi) \rightarrow ((\neg \neg \varphi \rightarrow \psi) \rightarrow \neg \varphi)$ A3
  8. $(\neg \neg \varphi \rightarrow \psi) \rightarrow \neg \varphi$ MP 4,7
  9. $\neg \varphi$ MP 6,8

With the Deduction Theorem, this gives us Contraposition: $\varphi \rightarrow \psi \vdash \neg \psi \rightarrow \neg \varphi$

And now we can show $\varphi \rightarrow \psi, \neg \varphi \rightarrow \psi \vdash \psi$:

  1. $\varphi \rightarrow \psi$ Premise
  2. $\neg \varphi \rightarrow \psi$ Premise
  3. $\neg \psi \rightarrow \neg \varphi$ Contraposition 1
  4. $\neg \psi \rightarrow \neg \neg \varphi$ Contraposition 2
  5. $(\neg \psi \rightarrow \neg \neg \varphi) \rightarrow ((\neg \psi \rightarrow \neg \varphi) \rightarrow \psi)$ A3
  6. $(\neg \psi \rightarrow \neg \varphi) \rightarrow \psi$ MP 4,5
  7. $\psi$ MP 3,6
  • $\begingroup$ wow! thank you! $\endgroup$ – PeptideChain Apr 26 '18 at 13:39
  • $\begingroup$ @LiPo You're welcome! It's just a matter of creating a library of all these Lemma's. Creating them is a pain, but once you have them, proofs get easier and easier :) $\endgroup$ – Bram28 Apr 26 '18 at 13:42

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.