License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2014.162
URN: urn:nbn:de:0030-drops-54966
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5496/
Go to the corresponding LIPIcs Volume Portal

Maietti, Maria Emilia ; Maschio, Samuele

An Extensional Kleene Realizability Semantics for the Minimalist Foundation

pdf-format:
10.pdf (0.6 MB)

Abstract

We build a Kleene realizability semantics for the two-level Minimalist Foundation MF, ideated by Maietti and Sambin in 2005 and completed by Maietti in 2009. Thanks to this semantics we prove that both levels of MF are consistent with the formal Church Thesis CT. Since MF consists of two levels, an intensional one, called mtt, and an extensional one, called emtt, linked by an interpretation, it is enough to build a realizability semantics for the intensional level mtt to get one for the extensional one emtt, too. Moreover, both levels consists of type theories based on versions of Martin-Löf's type theory. Our realizability semantics for mtt is a modification of the realizability semantics by Beeson in 1985 for extensional first order Martin-Löf's type theory with one universe. So it is formalized in Feferman's classical arithmetic theory of inductive definitions, called ID1^. It is called extensional Kleene realizability semantics since it validates extensional equality of type-theoretic functions extFun, as in Beeson's one. The main modification we perform on Beeson's semantics is to interpret propositions, which are defined primitively in MF, in a proof-irrelevant way. As a consequence, we gain the validity of CT. Recalling that extFun+CT+AC are inconsistent over arithmetics with finite types, we conclude that our semantics does not validate the Axiom of Choice AC on generic types. On the contrary, Beeson's semantics does validate AC, being this a theorem of Martin-Löf's theory, but it does not validate CT. The semantics we present here seems to be the best approximation of Kleene realizability for the extensional level emtt. Indeed Beeson's semantics is not an option for emtt since AC on generic sets added to it entails the excluded middle.

BibTeX - Entry

@InProceedings{maietti_et_al:LIPIcs:2015:5496,
  author =	{Maria Emilia Maietti and Samuele Maschio},
  title =	{{An Extensional Kleene Realizability Semantics for the Minimalist Foundation}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{162--186},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5496},
  URN =		{urn:nbn:de:0030-drops-54966},
  doi =		{10.4230/LIPIcs.TYPES.2014.162},
  annote =	{Keywords: Realizability, Type Theory, formal Church Thesis}
}

Keywords: Realizability, Type Theory, formal Church Thesis
Collection: 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Issue Date: 2015
Date of publication: 12.10.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI