Is this Hilbert proof system complete? Note: This post considers propositional logic, with $\to$, $\bot$ as the base connectives, $\neg \phi$ is an abbreviation for $\phi\to \bot$.Consider  a usual Hilbert-style proof system(with modus-ponens as the sole inference rule) with the following axioms,

*

*$\phi \to \left( \psi \to \phi \right)$

*$\neg \phi \to(\phi\to \psi)$

*$\neg\neg \phi\to \phi$
The first axiom is a "weakening" axiom, the second is an "explosion" axiom and the third is usual double-negation. My question(which comes out of idle curiosity) is: Is this proof system complete, or in the other words does $\Gamma \vdash \phi \iff \Gamma\models \phi$?(Here "$\Gamma \vdash \phi$" means that there is a Hilbert-style proof of $\phi$, from the set of assumptions $\Gamma$). The $\implies$ direction is basically trivial, but does the other direction hold? (I’m not very sure, and don’t even know how to prove something like the deduction theorem or even $\vdash \phi\to\phi$)
 A: This is not complete.
To show it is not complete, let us consider an alternative semantics for the operators involved. That is, suppose that all statements involved evaluate to either $0$, $1$, or $2$. That is, suppose all atomic variables take the value of either $0$, $1$, or $2$, suppose that $\bot$ is a constant that denotes $1$, and suppose that the $\to$ operator works as follows:
\begin{array}{cc|c}
P&Q&P\to Q\\
\hline
0&0&0\\
0&1&1\\
0&2&2\\
1&0&0\\
1&1&0\\
1&2&0\\
2&0&0\\
2&1&2\\
2&2&0\\
\end{array}
With that, we can also figure out how $\neg$ works:
\begin{array}{c|ccc}
P&P & \to & \bot\\
\hline
0&0&1&1\\
1&1&0&1\\
2&2&2&1\\
\end{array}
OK, so now let's evaluate the three axioms you have:
\begin{array}{c|ccc}
P&\neg & \neg P &\to &P\\
\hline
0&0&1&0&0\\
1&1&0&0&1\\
2&2&2&0&1\\
\end{array}
\begin{array}{cc|ccc|cc}
P&Q&\neg P & \to & (P \to Q)&P & \to & (Q \to P)\\
\hline
0&0&1&0&0&0&0&0\\
0&1&1&0&1&0&0&0\\
0&2&1&0&2&0&0&0\\
1&0&0&0&0&1&0&1\\
1&1&0&0&0&1&0&0\\
1&2&0&0&0&1&0&2\\
2&0&2&0&0&2&0&2\\
2&1&2&0&2&2&0&0\\
2&2&2&0&0&2&0&0\\
\end{array}
So notice that all of your axioms have the property that they will always evaluate to $0$, no matter what. As such, we can call them '$0$-tautologies'
Also note that if you look at the definition of the $\to$ operator, you will find that whenever $P \to Q$ has the value of $0$, and $P$ has the value of $0$, $Q$ will have to have the value of $0$ as well. This means that if you have any two $0$-tautologies, then the only kind of statement that you can infer from that using Modus Ponens is another $0$-tautology.
Finally, consider the statement $(P \to \neg P) \to \neg P$. This is not a $0$-tautology:
\begin{array}{c|ccccc}
P&(P & \to & \neg P) & \to & \neg P\\
\hline
0&0&1&1&0&1\\
1&1&0&0&0&0\\
2&2&0&2&\color{red}{2}&2\\
\end{array}
So, this means that $(P \to \neg P) \to \neg P$ cannot be inferred from your axioms and Modus Ponens. But since $(P \to \neg P) \to \neg P$ is a tautology in normal propositional logic, that means your system is not complete.
