Formally proving $p\wedge q \rightarrow p$ I want to write a full prove for $p\wedge q \rightarrow p$ without using deduction, using only ${\neg, \rightarrow}$ connectives.
I want to use the standard axiomatic system:
$\alpha\rightarrow(\beta\rightarrow\alpha)$
$(\alpha\rightarrow(\beta\rightarrow\gamma))\rightarrow((\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow\gamma))$
$(\neg\beta\rightarrow\neg\alpha)\rightarrow((\neg\beta\rightarrow\alpha)\rightarrow \beta)$
I only succeeded to prove it using deduction. I tried to work back from deduction to full proof using the general fact (on which deduction theorem proof relies) that $\alpha \vdash\beta \Rightarrow \vdash\alpha\rightarrow B_i$, for every $B_i\in\{B_i\}_1^n$ the prove sequence of $\beta$ from $\alpha$ , in order to find a formula $\gamma$ to apply $A2$ such that $(\neg(p\rightarrow\neg q)\rightarrow(\gamma \rightarrow p))\rightarrow((\neg(p\rightarrow\neg q)\rightarrow\gamma)\rightarrow(\neg(p\rightarrow\neg q)\rightarrow p))$
My proof using deduction:
First $p\wedge q \rightarrow p \equiv \neg(p\rightarrow\neg q)\rightarrow p$

*

*deduction: $\neg(p\rightarrow q)\vdash p$

*applying lemma: $\alpha\vdash\beta\Leftrightarrow\neg\beta\vdash\neg\alpha$ one may prove: $\neg p\vdash p\rightarrow q$

*deduction: $\neg p,p\vdash q$

*A3:
$(\neg q\rightarrow\neg p)\rightarrow((\neg q\rightarrow\ p)\rightarrow q)$

*A1 : $\neg p\rightarrow (\neg q\rightarrow\neg p)$

*MP by assumption $(\neg q\rightarrow\neg p)$

*A1 : $p\rightarrow (\neg q\rightarrow p)$

*MP by assumption $(\neg q\rightarrow p)$

*MP 6 from 4:$(\neg q\rightarrow\ p)\rightarrow q$

*MP 8 from 9:$q$
 A: HINT
Work backwards. Since you need to show $\vdash \neg (p \rightarrow \neg q) \rightarrow p$ you probably want to show $\neg (p \rightarrow \neg q) \vdash p$ and then use the Deduction theorem.
Second, since the goal is now $p$, you probably want to use axiom 3 and show $\neg p \rightarrow \varphi$ and $\neg p \rightarrow \neg \varphi$ for some $\varphi$.
What might be that $\varphi$? Well, you have as a premise $\neg (p \rightarrow \neg q)$, so that could be your $\neg \varphi$, so then the $\varphi$ would be $p \rightarrow \neg q$.
OK, so here's the basic proof strategy/plan:


*

*Show that $\vdash \neg p \rightarrow (p \rightarrow \neg q)$ (which is easy: prove $p, \neg p \vdash q$ and then apply Deduction theorem twice)

*Show that $\neg (p \rightarrow \neg q) \vdash \neg p \rightarrow \neg (p \rightarrow \neg q)$ (even easier, using axiom 1)

*Given 1 and 2, and using axiom 3, we can quickly get: $\neg (p \rightarrow \neg q) \vdash p$

*Apply Deduction theorem on 3 to get $\vdash \neg (p \rightarrow \neg q) \rightarrow p$, i.e. $\vdash (p \land q) \rightarrow p$
