# Show that $(\phi \rightarrow \psi), (\phi \rightarrow \neg \psi) \vdash \neg \phi$

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't you use that $\lnot \lnot \phi \rightarrow \phi$? – Jonas Gomes Oct 1 '14 at 5:41
• 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. – Doug Spoonwood Oct 1 '14 at 21:57
• @Doug Spoonwood: so modus ponens (and substitution I suppose) also are allowed, not only the three axioms? – 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 φ$.

Proof

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((x->y)->((x->-y)->-x)).


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