Modus ponens proof

Question

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?

Answer 1

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