I need to show that $(\phi \rightarrow \psi), (\phi \rightarrow \neg \psi) \vdash \neg \phi$ using the axioms: For any formula $\psi,\theta, \phi$ $$ 1.:(\psi \rightarrow (\theta \rightarrow \psi))$$ $$2.:(\psi \rightarrow (\phi\rightarrow\theta)) \rightarrow((\psi\rightarrow\phi)\rightarrow(\psi\rightarrow\theta)))$$ $$3.: ((\neg \psi \rightarrow \neg \theta) \rightarrow (\theta \rightarrow \psi))$$

I'm allowed to use Thinning Rule, Contradiction and Deduction.

Looking at this, I'm thinking this has to be by contradiction. But I have no idea how to start this.

Can anyone please help me? Thank you!

  • $\begingroup$ Can't you use that $\lnot \lnot \phi \rightarrow \phi$? $\endgroup$ Oct 1, 2014 at 5:41
  • $\begingroup$ You can prove ALL $\rightarrow$, $\lnot$ tautologies from this axiom set using just deduction (or modus ponens or detachment). Note that (($\phi$ $\rightarrow$ $\psi$) $\rightarrow$ (($\phi$ $\rightarrow$ $\lnot$ $\psi$) $\rightarrow$ $\lnot$ $\phi$)) is a tautology. $\endgroup$ Oct 1, 2014 at 21:57
  • $\begingroup$ @Doug Spoonwood: so modus ponens (and substitution I suppose) also are allowed, not only the three axioms? $\endgroup$
    – Lehs
    Oct 2, 2014 at 8:59

3 Answers 3


In your previous post you have proved Double Negation elimination :

$\vdash (¬¬p → p)$

with axioms 1 and 3; so we assume that we can use it.

We assume also the Proof by contradiction theorem :

If $\Gamma, ¬φ \vdash ψ$ and $\Gamma, ¬φ \vdash ¬ψ$, then $\Gamma \vdash φ$.


1) $(φ → ψ)$ --- assumed

2) $(φ → ¬ψ)$ --- assumed

3) $\vdash \lnot \lnot φ → φ$ --- DN

4) $(φ → ψ), \lnot \lnot φ \vdash ψ$ - from 3) by modus ponens

5) $(φ → ¬ψ), \lnot \lnot φ \vdash ¬ψ$ - from 3) by modus ponens

Now we apply Thinning and then Proof by contradiction to 4) and 5) with $\Gamma = \{ (φ → ψ), (φ → ¬ψ) \}$ to derive :

6) $ (φ → ψ), (φ → ¬ψ) \vdash \lnot φ$.


You can solve this problem fairly quickly using Prover9. All you need to do comes as to use the graphical interface, and put in the following as your assumptions... note you do need the periods:

1. -P(x->y) | -P(x) | P(y).  

Via this axiom and the rule of hyperresolution this enables you to accurately interpret steps in the proof to behave just like applications of condensed detachment. The "-" is negation like your $\lnot$ symbol.

2. P(x->(y->x)).

3. P((x->(y->z))->((x->y)->(x->z))).

4. P((-x->-y)->(y->x)).

And put this as the goal:


"P" you can interpret as meaning $\vdash$. Thus, once you have $\vdash$((x->y)->((x->-y)->-x)), if you assume (x->y) as well as (x->-y), you can detach -x as desired.


We first prove a general case:

$\{P\rightarrow Q, P\rightarrow R\}\vdash P\rightarrow Q\wedge R$

Now, the proof is as follows:

$$\begin{array}{r|ll} (1) & P\rightarrow Q & Hyp.\\ (2) & P\rightarrow R & Hyp.\\ (3) & (Q\rightarrow(R\rightarrow(Q\wedge R)) & Theorem\\ (4) & P\rightarrow(R\rightarrow(Q\wedge R)) & (1), (3), HS\\(5) &(P\rightarrow(R\rightarrow(Q\wedge R))\rightarrow((P\rightarrow R)\rightarrow(P\rightarrow(Q\wedge R)) & Ax. 2\\ (6) & (P\rightarrow R)\rightarrow(P\rightarrow(Q\wedge R)) & (4),(5), MP\\ (7) & P\rightarrow(Q\wedge R) & (2), (6), MP \end{array}$$ Now, replacing $R$ by $\neg Q$ we get $\{P\rightarrow Q,P\rightarrow\neg Q\}\vdash P\rightarrow(Q\wedge\neg Q)$, which is equivalent with $P\rightarrow\bot$, and this is equivalent with $\neg P$; Using $\vdash(Q\wedge \neg Q)\leftrightarrow\bot$ and $\vdash\neg P\leftrightarrow\bot$.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .