# Modus ponens proof

I'm trying to prove that $\neg\bullet\varphi$ in system $L(\neg, \to, \bullet)$,

$\bullet \varphi \approx (\varphi \to \varphi)$

Axiomas are the followind:

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?

We cannot prove it ...

As said in your previous post :

in system $$\mathcal L(\neg, \to, \bullet)$$, $$\bullet$$ "acts" as a constant truth, i.e. $$\bullet \varphi \approx (\varphi \to \varphi)$$.

If we consider the usual truth functional properties of the conncetives : $$\lnot, \rightarrow$$, and replace $$\bullet \varphi$$ with $$\top$$ ("the true"), we have that :

A1) $$\neg\neg\bullet\bullet\varphi$$ is $$\neg \neg (\top \to \top)$$, that is always $$\top$$

A2) $$(\neg\bullet\varphi \to \neg \psi)$$ is $$(\neg \top \to \neg \psi)$$, that is $$(\bot \to \neg \psi)$$, and again it is always $$\top$$

A3) $$((\varphi\to\psi) \to (\neg\psi\to\neg\varphi))$$ is a tautology; thus it is also $$\top$$.

Of course, modus ponens preserves validity.

But :

$$\neg\bullet\varphi$$ is $$\neg \top$$ i.e. $$\bot$$.