# How to prove $\vdash p\to\neg\neg p$ in this system?

I was asked to prove $$\vdash p\to\neg\neg p$$ in this system.

Axioms:
$$(\mathcal A_1)\vdash p\to(q\to p)$$
$$(\mathcal A_2)\vdash (p\to(q\to r))\to((p\to q)\to (p\to r))$$
$$(\mathcal A_3)\vdash \neg\neg p\to p$$

I have tried to use axiom 2 and find a proper proposition $$x$$ such that $$\vdash (p\to(x\to\neg\neg p)) \to ((p\to x)\to (p\to \neg\neg p))$$ holds, but I couldn't find one.

Any help would be appreciated.

Note from a comment on a deleted answer: there is also a rule that $$\lnot P$$ may be replaced by $$P \to \bot$$.

• For a system like this, trying to solve individual propositional expressions is like trying to build a house with a blindfold on. You should first learn truth tables, then translate the process of proving something with truth tables into the language of this logic. This is usually hidden as a "proof of completeness". Figuring out how to solve every propositional expression is much much easier than figuring out how to solve 1 propositional expression. – DanielV May 19 at 3:14
• If modus ponens is the only rule of inference, this isn't possible. – Doug Spoonwood May 20 at 14:21

If $$A$$ is a set of propositions, $$p$$, $$q$$ are propositions, then $$A \vdash p\to q$$ is equivalent to $$A \cup \{p\} \vdash q$$.
$$\{p,\neg p\}\vdash p\tag{1; assumed}$$ $$\{p,\neg p\}\vdash \neg p=(p\to\bot)\tag{2; assumed}$$ $$\{p,\neg p\}\vdash \bot\quad\tag{3; MP,1,2}$$ $$\{p\}\vdash (\neg p\to \bot)=\neg\neg p\tag{4; DT}$$ $$\vdash (p\to \neg\neg p)\tag{5; DT}$$
• This is correct. You might want to replace F with $\bot$ for clarity since F looks like a propositional variable. Also you can use \tag to name expressions. – DanielV May 20 at 5:15