Analyzing realizability by Troelstraʹs methods Original Research Article

Realizabilities are powerful tools for establishing consistency and independence results for theories based on intuitionistic logic. Troelstra discovered principles ECT0 and GC1 which precisely characterize formal number and function realizability for intuitionistic arithmetic and analysis, respectively. Building on Troelstraʹs results and using his methods, we introduce the notions of Church domain and domain of continuity in order to demonstrate the optimality of “almost negativity” in ECT0 and GC1; strengthen “double negation shift” DNS0 to DNS1 and use it with GC1 and Markovʹs Principle MP to characterize the classically provably realizable formulas of analysis; and show that intuitionistic analysis with GC1, MP and DNS1 is consistent and satisfies Troelstraʹs and Churchʹs Rules. We end with a discussion of semi-intuitionistic theories and a conjecture.