scientific article; zbMATH DE number 1746890

DOI10.1002/1521-3870(200202)48:2%3C179::AID-MALQ179%3E3.0.CO;2-KMaRDI QIDQ4531082zbMATH OpenFDO

Authors Silvio Valentini

Publication date 29 May 2002

Full work available at URL https://doi.org/10.1002/1521-3870(200202)48:2%3C179::AID-MALQ179%3E3.0.CO;2-K

zbMATH Keywords

constructive set theoryconstructive type theoryextensional set constructors

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Recommendations

• The inconsistency of higher order extensions of Martin-Löf's type theory
• Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?
• Integrating classical and intuitionistic type theory
• The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory
• The constructive Hilbert program and the limits of Martin-Löf type theory

Cites work

• Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 192841 (Why is no real title available?)
• scientific article; zbMATH DE number 1302067 (Why is no real title available?)
• Inductively generated formal topologies.
• The inconsistency of higher order extensions of Martin-Löf's type theory

Cited in

(10)

• A cartesian closed category in Martin-Löf's intuitionistic type theory
• Extensional set equality in the calculus of constructions
• Relative constructivity
• Conservativity of equality reflection over intensional type theory
• Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?
• Converse extensionality and apartness
• Extensionality of ^*
• The inconsistency of higher order extensions of Martin-Löf's type theory
• THE AXIOM OF CHOICE IS FALSE INTUITIONISTICALLY (IN MOST CONTEXTS)
• Constructing unprejudiced extensional type theories with choices via modalities

This page was built for publication:

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