Realization of Intuitionistic KPM in Explicit Mathematics

Sergei Tupailo

We continue the study of realizability of different intuitionistic theories in Feferman’s Explicit Mathematics began in [1] and [2]. It’s easily seen that intuitionistic Kripke-Platek Set Theory IKP is a subsystem of Aczel’s Constructive Set Theory CZF, so that embedding of IKP into T_{0} is already contained in [2]. However, analogous relations don’t hold for much stronger theories IKPi and IKPM, which are intuitionistic versions of familiar KPi and KPM, resp. Nevertheless, we can modify our realizability interpretation to take care of these theories as well.

The key question is how to realize admissibility. If we take it to be expressed by a new predicate symbol Ad, then we define 𝔯 \underline{rn} Ad(α) ≡ 𝔯 \underline{rn}^{E}Ad(α) as

p_{000}𝔯 \underline{rn}^{E}Tran[α] ∧ p_{001}𝔯 \underline{rn}^{E}Pair^{α} ∧ p_{010}𝔯 \underline{rn}^{E}Union^{α} ∧ p_{011}𝔯 \underline{rn}^{E}Infinity^{α} ∧

∀x ε α∀𝔵(lnx = 1 → p_{100}𝔯x𝔵 \underline{rn}^{E}(s[str(α, x), 𝔵] ∈ α)) ∧

∀x ε α∀𝔵(lnx = 1 ∧ ∀y ε str(α, x)(lny = 1 → 𝔵y ε α ∧ ln(𝔵y) = 1) → p_{101}𝔯x𝔵 \underline{rn}^{E}(sc[str(α, x), 𝔵] ∈ α)),

where p_{klm}𝔯 is p_{k}(p_{l}(p_{m}𝔯)), k, l, m = 0, 1,

s[β, 𝔵] :≐ {c ε seq | lnc = 0 ∨ (lnc ≠ 0 ∧ c = sm(sm_{0}c, 𝔵) ∧ sm_{0}c ε β)},
sc[β, x] :≐ {c ε seq | lnc = 0 ∨ (lnc ≠ 0 ∧ headc ε β ∧ bodytc ε j(β̄, λy.str(α, 𝔵y)))},
β̄ :≐ {y ε β | lny = 1},

and the rest of definitions are the same as in [2]. With these definitions Ad-axioms are realized and all corresponding theorems of [2] still hold, including

Theorem 4 IKPM is realizable in T_{m}.

[1] S. Tupailo. Realization of analysis into Explicit Mathematics. Submitted,

http://www.iam.unibe.ch/~sergei/an.ps

[2] S. Tupailo. Realization of Constructive Set Theory into Explicit Mathematics: a lower bound for impredicative Mahlo universe. Submitted,

http://www.iam.unibe.ch/~sergei/czf.ps

Address: Institut für Informatik und angewandte Mathematik, Universität Bern, Neubrückstrasse 10, CH 3012 Bern, Switzerland

E-mail: sergei@iam.unibe.ch