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?
MathOverflow is a question and answer site for professional mathematicians. It only takes a minute to sign up.
Sign up to join this communityAs 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?
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.
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.
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.