2
$\begingroup$

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.

$\endgroup$
15
  • $\begingroup$ Propositional variable is neither provable nor refutable even if $p\lor \lnot p$ is provable. You might misunderstand the completeness. $\endgroup$
    – Hanul Jeon
    Commented Sep 20, 2015 at 2:26
  • $\begingroup$ 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. $\endgroup$
    – Hanul Jeon
    Commented Sep 20, 2015 at 2:30
  • $\begingroup$ 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. $\endgroup$
    – Mauro ALLEGRANZA
    Commented Sep 20, 2015 at 7:09
  • $\begingroup$ 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. $\endgroup$
    – mmw
    Commented Sep 20, 2015 at 14:16
  • 1
    $\begingroup$ @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. $\endgroup$
    – Mauro ALLEGRANZA
    Commented Sep 20, 2015 at 17:16

2 Answers 2

Reset to default
5
$\begingroup$

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 \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$.

$\endgroup$
8
  • $\begingroup$ 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. $\endgroup$
    – Noldorin
    Commented Mar 14, 2017 at 15:54
  • $\begingroup$ @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. $\endgroup$
    – user21820
    Commented Mar 15, 2017 at 6:21
  • $\begingroup$ @Noldorin: I checked plato.stanford.edu/entries/logic-intuitionistic and my claim is correct; search for "(DP)" for the disjunction property of intuitionistic logic. =) $\endgroup$
    – user21820
    Commented Mar 15, 2017 at 6:38
  • $\begingroup$ 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. :) $\endgroup$
    – Noldorin
    Commented Mar 15, 2017 at 23:34
  • $\begingroup$ @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! $\endgroup$
    – user21820
    Commented Mar 16, 2017 at 15:03
0
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ That's not a sentence, since it has a free variable. It's an open formula. $\endgroup$
    – Noldorin
    Commented May 4, 2018 at 22:30

You must log in to answer this question.

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