Consistency of the intensional level of the Minimalist Foundation with Church's thesis and axiom of choice

摘要

Consistency with the formal Church's thesis, for short CT, and the axiom of choice, for short AC, was one of the requirements asked to be satisfied by the intensional level of a two-level foundation for constructive mathematics as proposed by Maietti and Sambin (in Crosilla, Schuster (eds) From sets and types to topology and analysis: practicable foundations for constructivemathematics, Oxford University Press, Oxford, 2005). Here we show that this is the case for the intensional level of the two-level Minimalist Foundation, for short MF, completed in 2009 by the second author. The intensional level of MF consists of an intensional type theory a la MartinLof, calledmTT. The consistency ofmTTwithCTandACis obtained by showing the consistency with the formal Church's thesis of a fragment of intensional Martin-Lof's type theory, called MLtt1, where mTT can be easily interpreted. Then to show the consistency of MLtt1 with CT we interpret it within Feferman's predicative theory of non-iterative fixpoints I D1 by extending the well known Kleene's realizability semantics of intuitionistic arithmetics so that CT is trivially validated. More in detail the fragment MLtt1 we interpret consists of first order intensional Martin-Lof's type theory with one universe and with explicit substitution rules in place of usual equality rules preserving type constructors (hence without the so called. -rule which is not valid in our realizability semantics). A key difficulty encountered in our interpretation was to use the right interpretation of lambda abstraction in the applicative structure of natural numbers in order to model all the equality rules of MLtt1 correctly. In particular the universe of MLtt1 is modelled by means of I D1-fixpoints following a technique due first to Aczel and used by Feferman and Beeson.