Hilbert's ϵ‐operator in intuitionistic type theories
From MaRDI portal
Publication:4304116
DOI10.1002/malq.19930390137zbMath0802.03005MaRDI QIDQ4304116
Publication date: 5 October 1994
Published in: Mathematical Logic Quarterly (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1002/malq.19930390137
completeness theorem; Hilbert's \(\varepsilon\)-calculus; intuitionistic type theories; \(\varepsilon\)- operator; intuitionistic higher-order logic; topos semantics
03G30: Categorical logic, topoi
03B20: Subsystems of classical logic (including intuitionistic logic)
Related Items
The epsilon-reconstruction of theories and scientific structuralism, A categorical interpretation of the intuitionistic, typed, first order logic with Hilbert's \(\varepsilon\)-terms, The epsilon calculus and Herbrand complexity, Hilbert's logic. From axiomatics to proof theory, Formalization of the arithmetization of Euclidean plane geometry and applications, Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator, A characterization of those categories whose internal logic is Hilbert's \(\varepsilon\)-calculus, Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
Cites Work