Typed proof calculus models intuitionistic first-order logic with epsilon operator

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

Logic in Computer Science

Summary

This paper develops a formal system that precisely describes reasoning in a kind of mathematical logic that includes a special tool called Hilbert's epsilon-operator. The authors show that their system is both sound (it only proves true statements) and complete (it can prove all true statements) when interpreted in certain mathematical structures called thin epsilon-hyperdoctrines. They also demonstrate how their system behaves with and without the epsilon feature, and provide formal computer-checked proofs of their main results. This work lays groundwork for future approaches that keep track of proofs in detailed semantic settings.

What this means in practice

  • For program language designers: Define and verify programming languages or logics featuring choice operators using the authors’ typed proof calculus and epsilon-hyperdoctrinal semantics.
  • For formal verification engineers: Develop proof assistants or verification tools that rigorously handle first-order reasoning with epsilon terms backed by the formalized metatheory provided.

A theory result. No direct application yet.

Authors

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

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.
View PDFOpen arXiv