PreprintCC BY-NC-ND 4.0arXiv
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.
Related
- Nonmonotone Coderivative-Based Newton Methods for Nonsmooth Optimization with Machine Learning Applications
- Three-point orbits of 2-transitive groups and their combinatorial applications
- A unified variational framework for augmented Lagrangian preconditioning of saddle point systems: applications to mixed-dimensional and fictitious domain methods
- Truncated sequential change-point detection for Markov chains with applications in the epidemic statistical analysis
- Modeling inhomogeneous spatial point configurations with applications to replicated patterns in real-life waiting crowds
BibTeX
@misc{kocsis2026applications,
title = {{Two applications of the point-free coderivative}},
author = {Zoltan A. Kocsis},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.29436},
eprint = {2609.29436},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.29436},
note = {CC BY-NC-ND 4.0},
}
RIS
TY - UNPB
TI - Two applications of the point-free coderivative
AU - Zoltan A. Kocsis
PY - 2026
DA - 2026/09/24
PB - arXiv
DO - 10.48550/arxiv.2609.29436
UR - https://arxiv.org/abs/2609.29436
AB - 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.
ER -