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

DOI10.1016/0304-3975(92)90021-7MaRDI QIDQ1199547zbMATH OpenOpenAlexWikidataFDO

Authors 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

axiom of choicecalculus of constructionsinduction principle over data typespolymorphically typed lambda calculusproof by contradictionsecond-order quantification

Mathematics Subject Classification ID

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

Recommendations

• A simple model construction for the calculus of constructions
• scientific article; zbMATH DE number 4014064
• scientific article; zbMATH DE number 4074451
• scientific article; zbMATH DE number 1722653
• Proof-irrelevant model of CC with predicative induction and judgmental equality

Cites work

• Dependence and independence results for (impredicative) calculi of dependent types
• Extensional PERs
• scientific article; zbMATH DE number 194511 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• The calculus of constructions

Cited in

(11)

• Independence of the equational axioms for iteration theories
• Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
• scientific article; zbMATH DE number 1722653 (Why is no real title available?)
• On choice rules in dependent type theory
• The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF
• scientific article; zbMATH DE number 2003160 (Why is no real title available?)
• A simple model construction for the calculus of constructions
• scientific article; zbMATH DE number 3230240 (Why is no real title available?)
• scientific article; zbMATH DE number 3325540 (Why is no real title available?)
• Independence of the primitive symbols of Lewis's calculi of propositions
• The compatibility of the minimalist foundation with homotopy type theory

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1199547)