Independence of the induction principle and the axiom of choice in the pure calculus of constructions

DOI10.1016/0304-3975(92)90021-7zbMath0762.03008OpenAlexW1997723626WikidataQ114683722 ScholiaQ114683722MaRDI QIDQ1199547

Thomas Streicher

Publication date: 16 January 1993

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(92)90021-7

zbMATH Keywords

calculus of constructionsaxiom of choiceinduction principle over data typespolymorphically typed lambda calculusproof by contradictionsecond-order quantification

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Combinatory logic and lambda calculus (03B40)

Related Items (4)

The compatibility of the minimalist foundation with homotopy type theory ⋮ On Choice Rules in Dependent Type Theory ⋮ A simple model construction for the Calculus of Constructions ⋮ Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The calculus of constructions
• Extensional PERs
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Dependence and independence results for (impredicative) calculi of dependent types

This page was built for publication: Independence of the induction principle and the axiom of choice in the pure calculus of constructions