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

  • 1
    $\begingroup$ I can provide a partial answer for now... I am familiar with a completeness proof for a system in which your second axiom is replaced by $(\phi \rightarrow (\psi \rightarrow \theta)) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \theta))$. I also know that $\neg \phi \rightarrow (\phi \rightarrow \psi)$ can be derived in this system. Hence the partial answer to your question - if $(\phi \rightarrow (\psi \rightarrow \theta)) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \theta))$ can be derived from your three axioms, then the system is complete. $\endgroup$
    – Menander I
    Commented Mar 31, 2022 at 17:41
  • $\begingroup$ Usually in classical logic axioms are the most general tautologies for their bracket type. ¬¬ϕ→ϕ is a bit odd as an axiom, since it's an instance of (¬(ϕ→ψ)→ϕ). $\endgroup$ Commented Mar 31, 2022 at 19:23
  • 2
    $\begingroup$ @MenanderI ((ϕ→(ψ→θ))→((ϕ→ψ)→(ϕ→θ)) is not derivable in this system according to a quick check using Mace4. $\endgroup$ Commented Mar 31, 2022 at 21:04
  • $\begingroup$ @DougSpoonwood Thanks for checking ... it didn't look complete to me as well ... though with the $\neg$ being defined over $\to$ and $\bot$ I wasn't sure ... did you take that into account? $\endgroup$
    – Bram28
    Commented Mar 31, 2022 at 22:17
  • $\begingroup$ @Bram28 Unless I'm misremembering and made a mistake, I used the definition-free version. Instead of using P(C(N(x),C(x,y))) I used P(C(C(x,0),C(x,y))), and P(C(C(C(x,0),0),x)) instead of P(C(N(N(x)),x)). It would be derivable in the definiton-free version if it were derivable. $\endgroup$ Commented Apr 1, 2022 at 7:36

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

  • $\begingroup$ Interesting thanks , I haven’t read this in detail yet, but what goes wrong in trying the usual proof of completeness by showing every maximally consistent set has a model? $\endgroup$ Commented Mar 31, 2022 at 18:15
  • $\begingroup$ @VoiletFlame Hmm, I'd have to think about that myself a bit more, but my guess is that you no longer have the basic Lemma (of such a proof) that you can derive $\phi \to \psi$ if and only if you can derive $\neg \phi$ or you can derive $\psi$. With your first two axioms you have the 'if' part of this, so the 'only if' part must be false. $\endgroup$
    – Bram28
    Commented Mar 31, 2022 at 18:27
  • $\begingroup$ @VoiletFlame "The usual proof of completeness" uses a deduction metatheorem somewhere, correct? Well, this system doesn't have a deduction metatheorem. Specifically, that $\rightarrow$ distributes over itself is not provable in this system as I mentioned in my comment to MeanderI, while the deduction metatheorem implies that implication distributes over itself as provable, even when it's not an axiom. $\endgroup$ Commented Mar 31, 2022 at 21:20
  • $\begingroup$ @Bram28 I don't understand the very end of your answer: how are we using the fact that your example formula is a tautology in normal propositional logic to account for the other half of the proof? My expectation was that we need also to prove that adding this formula to the axioms does not lead to a contradiction (or alternatively that it does not allow us to prove every formula). $\endgroup$ Commented Mar 31, 2022 at 22:23
  • $\begingroup$ @CristianGratie The inability to derive some statement $\phi$ from a set of others can be demonstrated in different ways. You are referring to the method of adding the negation of $\phi$ to $\Gamma$ and showing that there is a model for the resulting set. However, I use a different method completely, showing that a certain kind of statement can not be inferred from others: starting with any instances of the OP’s axioms, which are all $0$-tautologies, and using MP, which can only infer other $0$-tautologies from $0$-tautologies, I cannot end up with a statement that is not a $0&-tautology. $\endgroup$
    – Bram28
    Commented Apr 1, 2022 at 0:16

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .