Realization of constructive set theory into explicit mathematics: a lower bound for impredicative Mahlo universe Original Research Article

We define a realizability interpretation of Aczelʹs Constructive Set Theory CZF into Explicit Mathematics. The final results are that CZF extended by Mahlo principles is realizable in corresponding extensions of View the MathML source, thus providing relative lower bounds for the proof-theoretic strength of the latter.