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.

I presume you already know the answer to your own question by now, but for completeness...

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 \
eg p$ does not imply that $S \vdash p$ or $S \vdash \
eg 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 \
eg p$ iff $M \vDash p$ or $M \vDash \
eg 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 $\
eg p$, since whatever $S$ proves must be true for every model of $S$.