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
Cites Work