Internal Languages for Thin Epsilon-Hyperdoctrines: Soundness, Completeness, and Rocq Formalization
Abstract
We present a typed proof-term calculus for intuitionistic intensional first-order logic with Hilbert's epsilon-operator and prove its soundness and completeness with respect to hyperdoctrinal models with thin bicartesian closed setoid categories (BiCCCs) as fibres and formula-indexed witness selections. The calculus provides an explicit internal language for these epsilon-hyperdoctrines: for each fixed typed signature, its syntactic term model is initial for syntax-indexed, interpretation-preserving model morphisms, with uniqueness up to setoid equality. The nested epsilon syntax is organized by a well-founded dependency relation on formula labels. Concrete countermodels exhibit failure of excluded middle and show that formula conversion need not identify the selected witnesses. We also compare the full calculus with its epsilon-free and epsilon-only fragments. The principal constructions and metatheorems are formalized in Rocq. With setoid BiCCCs, proof irrelevance is a choice of equality, not the erasure of proofs: the proofs and their categorical operations remain available as the basis for a future proof-relevant categorical semantics.
Related
- Optimal Decay Matrix Control Barrier Functions: Soundness and Completeness for Matrix Safety Constraints
- Global Regularity for the 3D Incompressible Navier–Stokes Equations via the Frohmanian Symplectic Tether: Lean 4 Formalization and Conditional Cubic Comparison Framework (v2.1)
- Formalization of Landau damping in the Vlasov--Poisson equations in Lean
- A Lean Formalization of the Hamilton--Perelman Proof of the Three-Dimensional Poincaré Conjecture
- A Lean Formalization of the Hamilton--Perelman Proof of Thurston's Geometrization Conjecture
BibTeX
@misc{molnar2026internal,
title = {{Internal Languages for Thin Epsilon-Hyperdoctrines: Soundness, Completeness, and Rocq Formalization}},
author = {Zoltán Gábor Molnár and Csaba Tóth},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.15080},
eprint = {2610.15080},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.15080},
}
RIS
TY - UNPB
TI - Internal Languages for Thin Epsilon-Hyperdoctrines: Soundness, Completeness, and Rocq Formalization
AU - Zoltán Gábor Molnár
AU - Csaba Tóth
PY - 2026
DA - 2026/10/10
PB - arXiv
DO - 10.48550/arxiv.2610.15080
UR - https://arxiv.org/abs/2610.15080
AB - We present a typed proof-term calculus for intuitionistic intensional first-order logic with Hilbert's epsilon-operator and prove its soundness and completeness with respect to hyperdoctrinal models with thin bicartesian closed setoid categories (BiCCCs) as fibres and formula-indexed witness selections. The calculus provides an explicit internal language for these epsilon-hyperdoctrines: for each fixed typed signature, its syntactic term model is initial for syntax-indexed, interpretation-preserving model morphisms, with uniqueness up to setoid equality. The nested epsilon syntax is organized by a well-founded dependency relation on formula labels. Concrete countermodels exhibit failure of excluded middle and show that formula conversion need not identify the selected witnesses. We also compare the full calculus with its epsilon-free and epsilon-only fragments. The principal constructions and metatheorems are formalized in Rocq. With setoid BiCCCs, proof irrelevance is a choice of equality, not the erasure of proofs: the proofs and their categorical operations remain available as the basis for a future proof-relevant categorical semantics.
ER -