# Does the Law of the Excluded Middle imply syntactical completeness?

The Law of the Excluded Middle (LEM) states that for any proposition $p$, we have $\vdash p \lor \lnot p$.

Syntactic completeness (a.k.a negation completeness) states that for any proposition $p$, we have $\vdash p$ or $\vdash \lnot p$.

As far as I'm aware, in classical propositional logic the former implies the latter (what's the simplest way to justify this?). This is highly problematic though, because it would mean that the contrapositive LEM is false) renders classical (Peano) arithmetic inconsistent – that is, LEM cannot possibly be a valid axiom/rule.

This strikes me as plain wrong, from what I've read. So, where have I messed up in my reasoning? Can we not in fact say that $\vdash p \lor \lnot p$ implies $\vdash p$ or $\vdash \lnot p$, at least not for classical logic? It seems intuitively true, but since I'm struggling to justify it formally, perhaps this is where the mistake lies.

• Propositional variable is neither provable nor refutable even if $p\lor \lnot p$ is provable. You might misunderstand the completeness. Sep 20 '15 at 2:26
• As far as I know, there are two completeness in logic and they are not coincide. When we call a theory $T$ is complete, every sentence (over the language of $T$) is provable or refutable from $T$. However when we say a logical system $\mathcal{L}$ is complete, it means (semantic) satisfiability implies (synthetic) provability. Sep 20 '15 at 2:30
• The two notions are different : the so-called semantic completeness for e.g. propositional calculus says that "if $\varphi$ is valid (i.e. a tautology), then it is provable". Thus, $p \lor \lnot p$ being a tautology, is provable; but $p$ is not a tautlogy (for any $p$), and thus it is not provable. Negation-completeness says that "for every sentence $\varphi$, either $\varphi$ or $\lnot \varphi$ is provable". Propositional logic, like first-order logic, are not negation-complete. Sep 20 '15 at 7:09
• This is a crucial difference between truth and provability. Yes, $\phi\lor \psi$ is true iff at least one of $\phi$ and $\psi$ is true. But we may have that $\phi\lor \psi$ be provable while neither of $\phi$ and $\psi$ is provable. This should be intuitive: you know by pure logic that I'm either sitting or not sitting, but, you know neither that I'm sitting nor that I'm not.
– mmw
Sep 20 '15 at 14:16
• @Noldorin - sorry for my insistence : the fact that $\vdash p \lor \lnot p$ but not $\vdash p$ or $\vdash \lnot p$ is due exactly to the soundenss and completeness of classical prop logic. If $\vdash p$ or $\vdash \lnot p$, this means that either $p$ or $\lnot p$ is a tautology, which is not, as already said in the answer and comments. Sep 20 '15 at 17:16

The key point is that syntactic completeness is a property of a formal system $S$ as viewed from the meta-system. Just because $S \vdash p \lor \neg p$ does not imply that $S \vdash p$ or $S \vdash \neg p$. The former "$\lor$" is a symbol in the language of the formal system, while the latter "or" is a part of the language of the meta-system. They only coincide for semantics, namely $M \vDash p \lor \neg p$ iff $M \vDash p$ or $M \vDash \neg p$ if $M$ is a structure and $p$ is a sentence over $M$. But if there are different models of $S$ that disagree on some sentence $p$, and $S$ is sound, then necessarily $S$ cannot prove $p$ and cannot prove $\neg p$, since whatever $S$ proves must be true for every model of $S$.
• Yes, but thanks for the clarification anyway. As I understand, $\vdash p \lor \neg p$ does imply $\vdash p$ or $\vdash \neg p$ for a given $p$, in any system of constructive logic. Mar 14 '17 at 15:54
• @Noldorin: It's not just for constructive logic. It's for any formal system that can interpret PA$^-$, including strong classical set theories like ZFC or strong type theories like MLTT or weak arithmetic theories like Q. But if I'm not mistaken intuitionistic first-order logic does satisfy that $\vdash p \lor \neg p$ iff $\vdash p$ or $\vdash \neg p$, because the only way you can derive a disjunction is by the introduction rule since intuitionistic logic forbids double negation elimination or LEM, and the principle of explosion can only be used under impossible (unprovable) assumptions. Mar 15 '17 at 6:21
• I see. What's $PA^-$, some variant of Peano Arithmetic? I presume that although you say ZFC, it must still be in a constructive setting, else it would contradict what you and others have said above. :) Mar 15 '17 at 23:34
• @Noldorin: PA$^-$ is described here. And no, ZFC is full ZFC, but I misread your comment as "does not imply". Haha! So I was indeed saying that any formal system that can interpret classical arithmetic does not satisfy the disjunction property. Thanks for catching my misreading! Mar 16 '17 at 15:03
There are plenty of sentences of classical propositional logic that are neither provable nor refutable. The simplest is $p$, where $p$ is a proposition letter.