Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

THE INDEPENDENCE OF MARKO… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

THE INDEPENDENCE OF MARKOV'S PRINCIPLE IN TYPE THEORY

Artikel i vetenskaplig tidskrift
Författare Thierry Coquand
B. Mannaa
Publicerad i Logical Methods in Computer Science
Volym 13
Nummer/häfte 3
ISSN 1860-5974
Publiceringsår 2017
Publicerad vid Institutionen för data- och informationsteknik (GU)
Språk en
Länkar dx.doi.org/10.23638/lmcs-13(3:10)20...
Ämnesord Forcing, Dependent type theory, Markovs Principle, Computer Science, Science & Technology
Ämneskategorier Data- och informationsvetenskap

Sammanfattning

In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One 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 [CMR17]. 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.

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?