# Modus ponens proof in system L(¬,→,∙)

I'm trying to prove $\neg\neg\bullet\varphi$

in system $L(\neg, \to, \bullet)$, where $\bullet$ is constant truth, i.e. $\bullet \varphi \approx (\varphi \to \varphi)$

Using modus ponens with axiomas:

A1) $\neg\neg\bullet\bullet\varphi$

A2) $(\neg\bullet\varphi \to \neg \psi)$

A3) $((\varphi\to\psi) \to (\neg\psi\to\neg\varphi))$

but still with no success. Could anybody suggest me some flow of proof?

Hint Take $\psi=\bullet\bullet\varphi$ in A2 and apply A3 and modus ponens.
• We have then $\psi \approx \bullet\bullet\varphi$, $\varphi \approx \varphi$, then using a2 $(\neg\bullet\varphi \to \neg\bullet\bullet\varphi)$ and a3 $((\varphi \to \bullet\bullet\varphi) \to (\neg\bullet\bullet\varphi\to\neg\varphi) )$ and using modus ponens if $a$, and $a \to b$ then $b$, but I don't see what can be $a$, and $b$ here. – Levitan Nov 2 '14 at 17:16
• @Levitan You're not using (A3) in the intended way. Allow me to rewrite (A3) as $((A\to B)\to (\neg B\to \neg A))$. You want to use (A3) with $A=\neg \bullet \varphi$ and $B=\neg \bullet \bullet \varphi$, so that you can use (A2). – Git Gud Nov 2 '14 at 17:21