34
$\begingroup$

As a sentential logic, intuitionistic logic plus the law of the excluded middle gives classical logic.

Is there a logical law that is consistent with intuitionistic logic but inconsistent with classical logic?

Improve this question
$\endgroup$
1
  • 8
    $\begingroup$ A purely logical law I don't think so. But there are, say, arithmetical axioms, like the extended Church-Turing thesis, which can be postulated and lead to interesting theories inconsistent with classical logic. $\endgroup$
    – Gro-Tsen
    Commented May 3, 2021 at 9:34

3 Answers 3

Reset to default
35
$\begingroup$

No, every consistent propositional logic that extends intuitionistic logic is a sublogic of classical logic. (That’s why consistent superintuitionistic logics are also called intermediate logics.)

To see this, assume that a logic $L\supseteq\mathbf{IPC}$ proves a formula $\phi(p_1,\dots,p_n)$ that is not provable in $\mathbf{CPC}$. Then there exists an assignment $a_1,\dots,a_n\in\{0,1\}$ such that $\phi(a_1,\dots,a_n)=0$. Being a logic, $L$ is closed under substitution; thus, it proves the substitution instance $\phi'$ of $\phi$ where we substitute each variable $p_i$ with $\top$ or $\bot$ according to $a_i$. But already intuitionistic logic can evaluate variable-free formulas, in the sense that it proves each to be equivalent to $\top$ or to $\bot$ in accordance with its classical value. Thus, $\mathbf{IPC}$ proves $\neg\phi'$, which makes $L$ inconsistent.

Improve this answer
$\endgroup$
10
  • 2
    $\begingroup$ Interesting. So the logics (between IPC and CPC) form a directed set (or even a lattice?), what's the point giving up LEM, then? $\endgroup$
    – Asaf Karagila ♦
    Commented May 3, 2021 at 10:13
  • 9
    $\begingroup$ @AsafKaragila: Many reasons! Two major kinds, which particularly show why this answer’s result doesn’t kill the interest of IPC: Interest in models where LEM fails (e.g. topological models); and interest in intuitionistic systems with richer languages (e.g. IFOL, IHOL, modal logics), where the analogue of this answer doesn’t hold — there are consistent anti-classical principles. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented May 3, 2021 at 10:22
  • 4
    $\begingroup$ A complete lattice, yes. $\endgroup$
    – Emil Jeřábek
    Commented May 3, 2021 at 10:23
  • 2
    $\begingroup$ What about higher-order logic? You answer for propositional logic, and Peter LeFanu Lumsdaine's answer gives examples in specific theories, but are there “purely logical” postulates of, say, pure predicate logic (note: I'm not sure what I mean exactly) that could be consistent and incompatible with classical logic? $\endgroup$
    – Gro-Tsen
    Commented May 3, 2021 at 13:17
  • 5
    $\begingroup$ @PeterLeFanuLumsdaine The point is that the closure of a logic under substitution of formulas for predicates applies to all predicates in the signature, including the equality predicate if you formulate it as an extra-logical predicate in FO-without-equality. It would not apply to equality treated as a logical symbol in FO-with-equality. $\endgroup$
    – Emil Jeřábek
    Commented May 3, 2021 at 16:29
31
$\begingroup$

Your question sounds like you’re thinking mainly about plain propositional logic, and for that, Emil Jeřábek’s excellent answer shows why the answer is “no”. But to supplement it a little, in case you’re also interested in richer systems: Yes, in languages beyond plain propositional logic (e.g. in first-order and higher-order logic), there are many interesting consistent statements that are inconsistent with LEM. These are often known as anti-classical principles. Two very well-studied examples:

  • Church’s thesis, the statement “all functions $\mathbb{N} \to \mathbb{N}$ are computable”. This is typically considered over Heyting Arithmetic (the intuitionistic analogue of Peano arithmetic, using IFOL), or other systems extending HA.

  • Brouwer’s continuity principle, “all functions $[0,1] \to \mathbb{R}$ are uniformly continuous”. This is typically considered over constructive set theories (eg IZF), intuitionistic higher-order logic (IHOL, aka elementary topos logic), or similar systems.

Many other interesting anti-classical principles have been considered over IFOL, IHOL, intuitionistic type theories, and other first-order or higher-order systems. I dimly recall also seeing anti-classical principles studied in modal logics (showing that they can occur in purely propositional settings), but I’m afraid I don’t remember any specific examples of these.

Improve this answer
$\endgroup$
4
  • 5
    $\begingroup$ Note that the given examples such as Church’s thesis are not consistent logical laws. They are just statements consistent with a particular theory formulated over intuitionistic logic. The distinguishing feature of a logical law is that it is a schema not tied to a particular interpretation of predicate and function symbols; that is, it is closed under substitution of arbitrary formulas for these symbols. $\endgroup$
    – Emil Jeřábek
    Commented May 3, 2021 at 16:47
  • $\begingroup$ @EmilJeřábek: Good point — I was forgetting that technical sense of “logical law”, I’m used to “law” just being used more loosely for statements taken as axioms. In that case: read in predicate logics, I agree, these aren’t consistent if taken as “laws”. In IHOL and most type theories, these don’t need any predicate symbols, so arguably are “laws”, but then also arguably, that definition of “law” isn’t appropriate to such systems. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented May 3, 2021 at 17:14
  • $\begingroup$ Is it accurate to say that in some sense univalence is an example of such a principle? $\endgroup$
    – Tim Campion
    Commented May 3, 2021 at 17:35
  • 2
    $\begingroup$ @TimCampion: Unlike the others I mention, univalence isn’t anti-classical — it’s consistent with LEM, at least for the right formulation of LEM (quantifying over propositions and using “or” not “+”). See §3.4 of the HoTT book, or Kapulkin–Lumsdaine arxiv.org/abs/2006.13694 . Univalence is inconsistent with the BHK translation of LEM (quantifying over all types and using “+” not “or”), but generally the BHK translation (while very important and useful for other things) is the wrong one to use for these kinds of comparisons. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented May 5, 2021 at 15:37
26
$\begingroup$

In first-order logic, the sentence $$\neg\forall x,y(\neg\neg x=y \to x=y)$$ is consistent with intuitionist logic but not with classical logic.

One might call this "the fuzziness of identity". In synthetic differential geometry, as axiomatized in Models for smooth infinitesimal analysis by Moerdijk and Reyes, this is actually a theorem about the real numbers.

Improve this answer
$\endgroup$
2
  • 2
    $\begingroup$ Is the sentence $\exists x,y \ \neg (\neg\neg x=y \to x=y)$ also consistent with intuitionistic logic? $\endgroup$
    – Sophie Swett
    Commented May 3, 2021 at 23:50
  • 4
    $\begingroup$ No. Here is the intuitionist refutation of that sentence: In general, we have $\neg P \to (P\to Q)$ and $Q \to (P \to Q)$. Taking contrapositives gives $\neg(P\to Q)\to(\neg\neg P\wedge \neg Q)$. So the sentence in your comment would imply $\neg^4 x=y \wedge \neg x=y$. This in turn implies $\neg^4 x=y \wedge \neg^3 x=y$, which is a contradiction. $\endgroup$
    – user44143
    Commented May 4, 2021 at 0:17

You must log in to answer this question.

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