English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We build a Kleene realizability semantics for the two-level MinimalistFoundation MF, ideated by Maietti and Sambin in 2005 and completed by Maiettiin 2009. Thanks to this semantics we prove that both levels of MF areconsistent with the (Extended) formal Church Thesis CT. MF consists of twolevels, 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 thetwo levels, it is enough to build a semantics for the intensional level to getone also for the extensional level. Hence here we just build a realizabilitysemantics for the intensional level mTT. Such a semantics is a modification ofthe realizability semantics in Beeson 1985 for extensional first orderMartin-L\"of's type theory with one universe. So it is formalised in Feferman'sclassical arithmetic theory of inductive definitions. It is called extensionalKleene realizability semantics since it validates extensional equality oftype-theoretic functions extFun, as in Beeson 1985. The main modification weperform on Beeson's semantics is to interpret propositions, which are definedprimitively in MF, in a proof-irrelevant way. As a consequence, we gain thevalidity of CT. Recalling that extFun+ CT+ AC are inconsistent over arithmeticswith finite types, we conclude that our semantics does not validate the fullAxiom of Choice AC. On the contrary, Beeson's semantics does validate AC, beingthis a theorem of Martin-L\"of's theory, but it does not validate CT. Thesemantics we present here appears to be the best Kleene realizability semanticsfor the extensional level emTT of MF. Indeed Beeson's semantics is not anoption for emTT since the full AC added to it entails the excluded middle.

An extensional Kleene realizability semantics for the Minimalist Foundation