A realizability semantics for inductive formal topologies, church’s thesis and axiom of choice

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.