arXiv · 2609.29436
Two applications of the point-free coderivative
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.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Zoltan A. Kocsis. 2026-09-24. Two applications of the point-free coderivative. https://arxiv.org/abs/2609.29436
Cite the original work for its findings. Save a collection to share your selection of sources.