An extensional Kleene realizability semantics for the Minimalist Foundation

DOI10.4230/LIPICS.TYPES.2014.162MaRDI QIDQ5277976zbMATH OpenOpenAlexFDO

Authors Maria Emilia Maietti, Samuele Maschio

Publication date 12 July 2017

Full work available at URL https://arxiv.org/abs/1502.02864

zbMATH Keywords

formal Church thesisrealizabilitytype theory

Mathematics Subject Classification ID

Type theory (03B38) Second- and higher-order arithmetic and fragments (03F35) Other constructive mathematics (03F65) Categorical logic, topoi (03G30)

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 (Extended) formal Church Thesis CT. MF consists of two levels, an intensional one, called mTT and an extensional one, called emTT, based on versions of Martin-L"of's type theory. Thanks to the link between the two levels, it is enough to build a semantics for the intensional level to get one also for the extensional level. Hence here we just build a realizability semantics for the intensional level mTT. Such a semantics is a modification of the realizability semantics in Beeson 1985 for extensional first order Martin-L"of's type theory with one universe. So it is formalised in Feferman's classical arithmetic theory of inductive definitions. It is called extensional Kleene realizability semantics since it validates extensional equality of type-theoretic functions extFun, as in Beeson 1985. 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 full Axiom of Choice AC. On the contrary, Beeson's semantics does validate AC, being this a theorem of Martin-L"of's theory, but it does not validate CT. The semantics we present here appears to be the best Kleene realizability semantics for the extensional level emTT of MF. Indeed Beeson's semantics is not an option for emTT since the full AC added to it entails the excluded middle.

Recommendations

• Axiomatizing higher-order Kleene realizability
• scientific article; zbMATH DE number 4033722
• Expressing Extension-Based Semantics Based on Stratified Minimal Models
• Publication:4865640
• Kripke semantics for dependent type theory and realizability interpretations
• A non-ground realization of the stable and well-founded semantics
• An implementation of Kripke-Kleene semantics
• Minimal readability of intuitionistic arithmetic and elementary analysis
• Generalized Realizability and Intuitionistic Logic
• Minimal refinements of specifications in modal and temporal logics

Cited in

(10)

• Axiomatizing higher-order Kleene realizability
• Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
• A categorical reading of the numerical existence property in constructive foundations
• scientific article; zbMATH DE number 6694121 (Why is no real title available?)
• On choice rules in dependent type theory
• A realizability semantics for inductive formal topologies, Church's thesis and axiom of choice
• A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS
• Dynamics in Foundations: What Does It Mean in the Practice of Mathematics?
• Equiconsistency of the minimalist foundation with its classical version
• A topological reading of coinductive predicates in dependent type theory

This page was built for publication: An extensional Kleene realizability semantics for the Minimalist Foundation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5277976)