Axiomatizing higher-order Kleene realizability (Q1338200): Difference between revisions
From MaRDI portal
Set OpenAlex properties. |
ReferenceBot (talk | contribs) Changed an Item |
||
Property / cites work | |||
Property / cites work: Q5605219 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3037432 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3671978 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A small complete category / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The Discrete Objects in the Effective Topos / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Colimit completions and the effective topos / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: ABOUT MODEST SETS / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5633977 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard / rank | |||
Normal rank |
Latest revision as of 10:34, 23 May 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Axiomatizing higher-order Kleene realizability |
scientific article |
Statements
Axiomatizing higher-order Kleene realizability (English)
0 references
19 December 1994
0 references
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 .
0 references
modest sets
0 references
effective topos
0 references
internal realizability
0 references
higher-order arithmetic
0 references