On the Proof Theoretical Strength of some Systems with the Numerical Omniscience Scheme

Solomon Feferman

The Numerical Omniscience Scheme (NOS) asserts for each formula A(n) (parameters allowed) of a given language that if A(n) is decided for each natural number n then either for all n, A(n) or there exists n with not-A(n). The scheme is considered in systems based on intuitionistic logic. A special case of NOS is the statement of the Limited Principle of Omniscience (LPO), which asserts that for all functions f of natural numbers, either f is identically zero or f has some non-zero value. Errett Bishop pointed out that all the theorems of classical analysis for which he found constructive substitutes follow from those substitutes together with LPO. NOS is here considered in the system of Heyting Arithmetic extended to finite types together with the Axiom of Choice AC in all types. It is shown that the Goedel functional (”Dialectica”) interpretation of this system together with NOS follows from its interpretation with LPO. The interpretation validates full AC. Thus the proof-theoretic strength of the interpreted system and a number of its variants has been determined by the author as reported in [1], secs. 8 and 9. In particular, if axioms for countable tree ordinals are added, the resulting system has strength measured by the Howard ordinal. This then establishes the strength of the system W introduced in [2], which uses only part of AC.

[1] J. Avigad and S. Feferman, Goedel’s functional (”Dialectica”) interpretation, in S. R. Buss (ed.) Handbook of Proof Theory, Elsevier, Amsterdam (1998), 337-405. [2] T. Coquand and E. Palmgren, Intuitionistic choice and classical logic, Archive for Mathematical Logic 39 (2000), 53-74.

Address: Dept. of Mathematics, Stanford University, Stanford CA 94305, USA