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 anyone please help me? Thank you!
 A: 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 φ$.

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