collaborators

1 paper

math.LO2026

Internal Languages for Thin Epsilon-Hyperdoctrines: Soundness, Completeness, and Rocq Formalization

Zoltán Gábor Molnár, Csaba Tóth

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 hyp…