Heyting predicate calculus with epsilon symbol
From MaRDI portal
Publication:1256460
DOI10.1007/BF01091551zbMath0404.03045MaRDI QIDQ1256460
Publication date: 1977
Published in: Journal of Soviet Mathematics (Search for Journal in Brave)
Cut- Elemination; Heyting Arithmetic with Choice Axiom; Heyting Predicate Calculus With Epsilon Symbol; Normal-Form Theorem; Quantifier Elemination
03F05: Cut-elimination and normal-form theorems
03F30: First-order arithmetic and fragments
03F55: Intuitionistic mathematics
03C10: Quantifier elimination, model completeness, and related topics
Related Items
Interpreting descriptions in intensional type theory, Harmonising natural deduction, Existential instantiation and normalization in sequent natural deduction
Cites Work