Independence of the induction principle and the axiom of choice in the pure calculus of constructions
type: Item
instance of: scholarly article
title: Independence of the induction principle and the axiom of choice in the pure calculus of constructions
zbMATH Open document ID: 0762.03008
DOI: 10.1016/0304-3975(92)90021-7
author: Thomas Streicher
published in: Theoretical Computer Science
publication date: 1993-01-16T00:00:00Z
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 94467
zbMATH Keywords: polymorphically typed lambda calculus
zbMATH Keywords: calculus of constructions
zbMATH Keywords: induction principle over data types
zbMATH Keywords: second-order quantification
zbMATH Keywords: axiom of choice
zbMATH Keywords: proof by contradiction
Wikidata QID: Q114683722
MaRDI profile type: Publication
full work available at URL: 0304-3975(92)90021-7
OpenAlex ID: W1997723626
cites work: The calculus of constructions
cites work: Q5573961
cites work: Q4692468
cites work: Dependence and independence results for (impredicative) calculi of dependent types
cites work: Q5286647
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
cites work: Extensional PERs
description: scientific article; zbMATH DE number 94467