Intuitionistic logic coderivative reveals limits in Heyting algebra and completeness
Two applications of the point-free coderivative
Logic in Computer Science
Summary
Some special math structures called Heyting algebras help us understand a kind of logic called intuitionistic logic, which is different from everyday logic. The authors show a simpler way to prove that one particular Heyting algebra can’t appear in a certain mathematical context called a topos. They also prove that using complete Heyting algebras to understand all statements in a more complex version of this logic doesn’t always work as expected.
What this means in practice
- •For theorem prover developers: Avoid relying on complete Heyting algebras for guaranteed strong completeness in intuitionistic second-order logic proof systems.
- •For formal verification engineers: Use the coderivative approach to identify limits of representing certain logical algebras within topos-based semantics.
A theory result. No direct application yet.
Authors
Zoltan A. Kocsis
Abstract
We present two new applications of Simmons' point-free Cantor-Bendixson coderivative operator in intuitionistic logic. First, we use it to give a simplified proof of the recent result of Xu and Ye that the free Heyting algebra on two generators does not occur as the Heyting algebra of subterminal objects in any elementary topos. Then we use it to prove that complete Heyting algebra semantics is not strongly complete for intuitionistic second-order propositional logic: semantic consequence from an arbitrary set of assumptions does not coincide with ordinary syntactic consequence.