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 '14 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 '14 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 '14 at 8:59

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

New contributor
Mahmood Bakhshi is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.

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.