The independence of Markov's principle in type theory

DOI10.23638/LMCS-13(3:10)2017MaRDI QIDQ5367048zbMATH OpenFDO

Authors Thierry Coquand, Bassel Mannaa

Publication date 12 October 2017

Full work available at URL https://arxiv.org/abs/1602.04530

zbMATH Keywords

dependent type theoryforcingMarkov's principle

Mathematics Subject Classification ID

Type theory (03B38) Other aspects of forcing and Boolean-valued models (03E40) Metamathematics of constructive systems (03F50)

Recommendations

• The independence of Markov's principle in type theory
• scientific article; zbMATH DE number 1841844
• On a weakening of Markov's Principle
• Markov's rule revisited
• scientific article; zbMATH DE number 5364051

Cited in

(12)

• Markov's rule revisited
• Failure is not an option. An exceptional type theory
• scientific article; zbMATH DE number 1722653 (Why is no real title available?)
• Partiality, Revisited
• scientific article; zbMATH DE number 1841844 (Why is no real title available?)
• Russian constructivism in a prefascist theory
• Modalities in homotopy type theory
• The independence of Markov's principle in type theory
• Game semantics of Martin-Löf type theory
• An analysis of Tennenbaum's theorem in constructive type theory
• ``Upon this quote I will build my Church thesis
• Separating Markov's principles

This page was built for publication: The independence of Markov's principle in type theory

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