Axiomatizing higher-order Kleene realizability (Q1338200): Difference between revisions

Kleene's realizability definition is extended to an ``internal realizability notion'' in the effective topos \textit{Eff}. The development of this internal realizability definition leads naturally to axioms in higher-order arithmetic, called ``covering axioms''. The new realizability definition can be formally defined in systems of higher- order arithmetic, and it is shown that, together with the well-known uniformity principles and Extended Church's Thesis, the covering axioms axiomatize the formalized realizability over higher-order arithmetic. One obtains a formal system which captures a large part of what can be said to be ``constructively true'' in \textit{Eff}. As an application, we develop the basic theory of ``modest sets'' in this system, and show an important completeness property of this category in it .