Is this Hilbert proof system complete?

Question

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

Answer 1

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.