License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2016.17
URN: urn:nbn:de:0030-drops-59939
URL: http://drops.dagstuhl.de/opus/volltexte/2016/5993/
Go to the corresponding LIPIcs Volume Portal


Coquand, Thierry ; Mannaa, Bassel

The Independence of Markovís Principle in Type Theory

pdf-format:
LIPIcs-FSCD-2016-17.pdf (0.6 MB)


Abstract

In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One tentative way to prove this would be to remark that Markov's principle does not hold in a sheaf model of type theory over Cantor space, since Markov's principle does not hold for the generic point of this model. It is however not clear how to interpret the universe in a sheaf model. Instead we design an extension of type theory, which intuitively extends type theory by the addition of a generic point of Cantor space. We then show the consistency of this extension by a normalization argument. Markov's principle does not hold in this extension, and it follows that it cannot be proved in type theory.

BibTeX - Entry

@InProceedings{coquand_et_al:LIPIcs:2016:5993,
  author =	{Thierry Coquand and Bassel Mannaa},
  title =	{{The Independence of Markovís Principle in Type Theory}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{17:1--17:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5993},
  URN =		{urn:nbn:de:0030-drops-59939},
  doi =		{10.4230/LIPIcs.FSCD.2016.17},
  annote =	{Keywords: Forcing, Dependent type theory, Markov's Principle, Cantor Space}
}

Keywords: Forcing, Dependent type theory, Markov's Principle, Cantor Space
Seminar: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue Date: 2016
Date of publication: 16.06.2016


DROPS-Home | Fulltext Search | Imprint Published by LZI