We present a Kleene realizability semantics for the intensional level of the Minimalist Foundation, for short mTT, extended with inductively generated formal topologies, the formal Church’s thesis and axiom of choice. This semantics is an extension of the one used to show the consistency of the intensional level of the Minimalist Foundation with the axiom of choice and the formal Church’s thesis in the work by Ishihara, Maietti, Maschio, Streicher [Arch.Math.Logic,57(7-8):873-888,2018]. A main novelty here is that such a semantics is formalized in a constructive theory as Aczel’s constructive set theory CZF extended with the regular extension axiom.
A realizability semantics for inductive formal topologies, church’s thesis and axiom of choice
Maietti Maria Emilia
;Maschio Samuele;
2021
Abstract
We present a Kleene realizability semantics for the intensional level of the Minimalist Foundation, for short mTT, extended with inductively generated formal topologies, the formal Church’s thesis and axiom of choice. This semantics is an extension of the one used to show the consistency of the intensional level of the Minimalist Foundation with the axiom of choice and the formal Church’s thesis in the work by Ishihara, Maietti, Maschio, Streicher [Arch.Math.Logic,57(7-8):873-888,2018]. A main novelty here is that such a semantics is formalized in a constructive theory as Aczel’s constructive set theory CZF extended with the regular extension axiom.
| File | Dimensione | Formato | |
|---|---|---|---|
|
1905.11966.pdf
accesso aperto
Tipologia:
Published (publisher's version)
Licenza:
Creative commons
Dimensione
427.71 kB
Formato
Adobe PDF
|
427.71 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
