{"id":"arxiv/2610.15080","url":"https://arxiv.org/abs/2610.15080","tags":["math.LO","cs.LO","math.CT"],"score":0,"title":"Internal Languages for Thin Epsilon-Hyperdoctrines: Soundness, Completeness, and Rocq Formalization","domain":"math.LO","source":"arxiv","authors":["Zoltán Gábor Molnár","Csaba Tóth"],"reviews":0,"subject":"math.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-10-10","reactions":{}}