Hilbert's ϵ‐operator in intuitionistic type theories
From MaRDI portal
Publication:4304116
DOI10.1002/malq.19930390137zbMath0802.03005OpenAlexW2190514756MaRDI 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 theoremHilbert's \(\varepsilon\)-calculusintuitionistic type theories\(\varepsilon\)- operatorintuitionistic higher-order logictopos semantics
Categorical logic, topoi (03G30) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items
Formalization of the arithmetization of Euclidean plane geometry and applications, The epsilon-reconstruction of theories and scientific structuralism, Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator, Dialectica principles via Gödel doctrines, 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, A categorical interpretation of the intuitionistic, typed, first order logic with Hilbert's \(\varepsilon\)-terms, Hilbert's logic. From axiomatics to proof theory, The epsilon calculus and Herbrand complexity
Cites Work
