Analyzing realizability by Troelstra's methods (Q5957857)

The schemata \(\text{ECT}_0\) (Extended Church's Thesis) and \(\text{GC}_1\) (Generalized Continuity Principle), invented by A. S. Troelstra, permit a precise characterization of number and functional realizability for intuitionistic arithmetic and analysis, respectively.NEWLINENEWLINENEWLINEThe author introduces the notions of Church domain and domain of continuity to demonstrate the optimality of ``almost negative'' in \(\text{ECT}_0\) and \(\text{GC}_1\). Using MP (Markov's Principle), \(\text{DNS}_1\) (a strengthened version of the ``double negation shift'') and \(\text{GC}_1\), she then gives a characterization of the classically provably realizable formulas of analysis. It is shown that intuitionistic analysis with MP, \(\text{DNS}_1\) and \(\text{GC}_1\) is consistent and satisfies Troelstra's and Church's Rules. The final section of the paper is concerned with semi-intuitionistic theories. NEWLINENEWLINENEWLINEMoschovakis' paper also presents a detailed account of the earlier results on realizability interpretations by Kleene, Nelson, Troelstra, Kreisel and others.