Consistency of the intensional level of the Minimalist Foundation with Church’s thesis and axiom of choice
| Autor: | Samuele Maschio, Maria Emilia Maietti, Hajime Ishihara, Thomas Streicher |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Discrete mathematics
Church's thesis Interpretation (logic) Logic realizabiltity type theory Church's thesis axiom of choice 010102 general mathematics Order (ring theory) Natural number 02 engineering and technology Consistency (knowledge bases) Type (model theory) 16. Peace & justice 01 natural sciences realizabiltity Philosophy Type theory axiom of choice type theory Realizability 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Axiom of choice 0101 mathematics Mathematics |
| Zdroj: | Archive for Mathematical Logic. 57:873-888 |
| ISSN: | 1432-0665 0933-5846 |
| DOI: | 10.1007/s00153-018-0612-9 |
| Popis: | 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 constructive mathematics, 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 Martin-Lof, called mTT. The consistency of mTT with CT and AC is obtained by showing the consistency with the formal Church’s thesis of a fragment of intensional Martin-Lof’s type theory, called $$\mathbf{MLtt}_1$$ , where mTT can be easily interpreted. Then to show the consistency of $$\mathbf{MLtt}_1$$ with CT we interpret it within Feferman’s predicative theory of non-iterative fixpoints $$\widehat{ID_1}$$ by extending the well known Kleene’s realizability semantics of intuitionistic arithmetics so that CT is trivially validated. More in detail the fragment $$\mathbf{MLtt}_1$$ 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 $$\xi $$ -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 $$\mathbf{MLtt}_1$$ correctly. In particular the universe of $$\mathbf{MLtt}_1$$ is modelled by means of $$\widehat{ID_1}$$ -fixpoints following a technique due first to Aczel and used by Feferman and Beeson. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|