PREDICATIVITY: THE OUTER LIMITS

STEPHEN G. SIMPSON

Abstract. Beginning with ideas of Poincaré and Weyl, Feferman in the sixties undertook a profound analysis of the predicativist foundational program. He presented a subystem of second order arithmetic IR and argued convincingly that it represents the outer limits of what is predicatively provable. Much later, Friedman introduced another system ATR_{0} which is conservative over IR for Π_{1}^{1} sentences yet includes several well known theorems of algebra, descriptive set theory, and countable combinatorics that are not provable in IR. The proof-theoretic ordinal of both systems is Γ_{0}. ATR_{0} has emerged as one of a handful of systems that are important for reverse mathematics. From a foundational standpoint, we may say that IR represents predicative provability while ATR_{0} represents predicative reducibility. Subsequently Friedman formulated mathematically natural finite combinatorial theorems that are not only not predicatively provable but go beyond Γ_{0} and therefore are not predicatively reducible.

§1. IR and ATR_{0}. In his first major work on systems of predicative analysis [3, 4], Feferman introduces the system IR and proposes it as an explication of predicative provability.

“Although we strongly believe that the explications proposed in this paper for the notion of predicative provability in analysis are correct, we are not convinced that the matter has been settled conclusively by the results obtained so far. It is premature to say just what would constitute final evidence concerning this question. We expect that this will be revealed, at least in part, by further study of the theories considered here.” (page 29)

In subsequent papers on predicative provability, Feferman does not back away from this proposal. The systems that he introduces in [5, 6, 7] as explications of predicative provability are conservative over IR.

Received by the editors October 29, 1999 and, in revised form, October 16, 2000. 1991 Mathematics Subject Classification. 03F35, 03D80, 03B30. Preparation of this paper was partially supported by NSF grant DMS-0070718. This paper is a writeup of my talk at a symposium at Stanford University, December

11–13, 1998, in honor of Solomon Feferman’s 70th birthday. I would like to thank Sol for his encouragement over many years and especially when I was writing my book [26] on reverse mathematics and subsystems of second order arithmetic.

Meeting \begin{matrix}c \\ ◯ \end{matrix} 1000, Association for Symbolic Logic

In this paper I want to compare Feferman’s system IR [3, 4] with another subsystem of second order arithmetic ATR_{0} due to Friedman [10]. We begin by briefly reviewing the definitions of these systems.

§2. Rules Versus Axioms. Both IR and ATR_{0} are formal systems or theories in the language of second order arithmetic. While ATR_{0} is easily defined by means of a finite set of axioms, IR is more conveniently described in terms of inference rules rather than axioms.

1. The Δ_{1}^{1} Comprehension Axiom:

\begin{matrix}(∀n ((∃X α(n, X)) ↔ (∀Y β(n, Y)))) \\ → ∃Z ∀n (n ∈ Z ↔ ∃X α(n, X)) \end{matrix}

Here α and β are arithmetical formulas.

2. The Δ_{1}^{1} Comprehension Rule:

\begin{matrix}∀n ((∃X α(n, X)) ↔ (∀Y β(n, Y))) \\ ∃Z ∀n (n ∈ Z ↔ ∃X α(n, X)) \end{matrix}

Here α and β are as above.

3. The Hierarchy Axiom:

∀Z (WO(Z) → ∀X ∃Y H(Z, X, Y))

Here WO(Z) is a Π_{1}^{1} formula expressing that Z is a well ordering of the integers, and H(Z, X, Y) is an arithmetical formula expressing that Y is a Turing jump hierararchy along Z starting at X.

4. The Hierarchy Rule:

\begin{matrix}WO(<_{e}) \\ ∀X ∃Y H(<_{e}, X, Y) \end{matrix}

Here <_{e} is a primitive recursive linear ordering of the integers, and WO(Z) and H(Z, X, Y) are as above.

5. The Transfinite Induction Axiom:

∀Z (WO(Z) → TI(Z, γ))

Here WO(Z) is as above, γ is an arbitrary formula, and TI(Z, γ) expresses transfinite induction along Z with respect to γ.

6. The Transfinite Induction Rule:

\begin{matrix}WO(<_{e}) \\ TI(<_{e}, γ) \end{matrix}

Here <_{e} and WO(Z) and TI(Z, γ) are as above. We are now ready to define the systems IR and ATR_{0}.

1. IR consists of the Δ_{1}^{1} Comprehension Rule, the Hierarchy Rule, and the Transfinite Induction Rule.

2. ATR_{0} consists of the Hierarchy Axiom. It is known that ATR_{0} includes the Δ_{1}^{1} Comprehension Axiom. It is a system with restricted induction (see Friedman [10]) and so does not include the Transfinite Induction Rule.

§3. Model-Theoretic Properties of IR and ATR_{0}. It is known that IR and ATR_{0} are proof-theoretically similar:

1. They have the same proof-theoretic ordinal: |IR| = |ATR_{0}| = Γ_{0}.

2. IR and ATR_{0} prove the same Π_{1}^{1} sentences. In particular, they prove the same arithmetical sentences.

3. IR and ATR_{0} have the same proof-theoretic strength. These results are due to Friedman [11, §4]. The main point that we would like to make here is that IR and ATR_{0} differ greatly in some other, very significant respects. In particular:

1. IR explicates predicative provability, while ATR_{0} explicates predicative reducibility.

2. ATR_{0} is much stronger than IR, model-theoretically and, above all, math-

ematically. The following properties of the two systems indicate how different they are from the model-theoretic point of view.

1. The minimum ω-model of IR is HYP(Γ_{0}), i.e., L_{Γ_{0}} ∩ P (ω). This is a

relatively small initial segment of

HYP = {X ⊆ ω : X is hyperarithmetical},

i.e., L_{ω_{1}^{CK}} ∩ P (ω).

2. The minimum ω-model of the Δ_{1}^{1} Comprehension Axiom is HYP.

3. HYP is the intersection of all ω-models of ATR_{0}.

4. ATR_{0} has no minimal ω-model.

5. ATR_{0} automatically holds in any β-model.

6. HYP is the intersection of all β-models.

7. There is no minimal β-model. We can also compare IR and ATR_{0} with the perhaps more familiar system Π_{∞}^{1}-TI_{0} consisting of the Transfinite Induction Axiom. The latter system is sometimes known as bar induction. Some model-theoretic properties:

1. Π_{∞}^{1}-TI_{0} includes both IR and ATR_{0}. The precise relationship to ATR_{0} is that Σ_{1}^{1}-TI_{0} = ATR_{0} + Σ_{1}^{1}-IND (Simpson [22]).

2. Π_{∞}^{1}-TI_{0} is proof-theoretically stronger than IR and ATR_{0}.

3. |Π_{∞}^{1}-TI_{0}| = φ_{ε_{Ω+1}}(0) = the Howard ordinal.

4. Π_{∞}^{1}-TI_{0} has no minimal ω-model.

5. Π_{∞}^{1}-TI_{0} automatically holds in any β-model.

6. HYP is the intersection of all β-models.

7. There is no minimal β-model. For proofs of the model-theoretic results mentioned above, see Chapters VII and VIII of Simpson [26].

Remark 1. We see above that ATR_{0} and Π_{∞}^{1}-TI_{0} are model-theoretically stronger than IR, in that the ω-models are larger. One might think that the greater strength comes from the fact that ATR_{0} and Π_{∞}^{1}-TI_{0} deal with arbitrary well orderings of the integers, and not only primitive recursive ones. However, this is not the case. Letting ATR_{0}^{−} be ATR_{0} with the Hierarchy Axiom restricted to primitive recursive linear orderings, the above model-theoretic results for ATR_{0} continue to hold for ATR_{0}^{−}. Thus these results are seen to have a certain robustness.

§4. A Set-Theoretic Version of ATR_{0}. In [5] Feferman introduced a settheoretic version of IR. Subsequently Simpson [21] introduced a set-theoretic version of ATR_{0} known as ATR_{0}^{set}, defined by

ATR_{0}^{set} = Axiom of Extensionality

+ Axiom of Foundation:

∀x (x ≠ ∅ → ∃u ∈ x (u ∩ x = ∅))

+ closure under F_{0}−F_{8}, i.e., under rudimentary functions

+ Axiom of Infinity

+ ∀x (x is hereditarily countable)

+ Axiom Beta:

∀r (WF(r) → ∃f (field(r) ⊆ dom(f)
∧ ∀u ∈ dom(f) (f(u) = {f(v) : ⟨v, u⟩ ∈ r}))) .

It is shown in Simpson [21] (see also [26, §VII.3]) that ATR_{0}^{set} is conservative over ATR_{0}. Actually, it is a definitional extension of ATR_{0}, where well founded trees encode hereditarily countable sets in the usual way.

§5. Reverse Mathematics of ATR_{0}. As is well known, ATR_{0} is one of the five basic systems of reverse mathematics. From Simpson [26, Chapter V] we have:

Theorem 2. The following are equivalent over RCA_{0}.

1. ATR_{0}.

2. Every disjoint pair of analytic sets can be separated by a Borel set.

3. The domain of a single-valued Borel set in the plane is Borel.

4. Every uncountable closed (or analytic) set has a perfect subset.

5. Clopen (or open) determinacy.

6. The clopen (or open) Ramsey Theorem.

7. For every countable bipartite graph, there exists a König covering, i.e., a pair (C, M) where C is a vertex covering, M is a matching, and C consists of one vertex of each edge in M. (This is a combined result of Aharoni/Magidor/Shore 1992 [1] and Simpson 1994 [25].)

8. Comparability of countable well orderings, i.e., well orderings of the integers.

9. The Ulm theory for countable reduced Abelian p-groups.

There are some interesting open questions concerning the reverse mathematics aspect of ATR_{0}.

1. Is Fraïssé’s conjecture for countable linear orderings provable in ATR_{0}? See [26, X.3.31] and Marcone 1994 [16] and Shore 1993 [19].

2. A well known consequence of the Ulm theory (see Kaplansky [14]) is: If each of two countable reduced Abelian p-groups is a direct summand of the other, then they are isomorphic.

Is this statement equivalent to ATR_{0}? This question is due to Friedman (see [26, V.7.7]). Some recent progress on this question is in Friedman [9].

Remark 3. The reverse mathematics investigations of [26, Chapter V] seem to indicate that, mathematically, IR is no stronger than ACA_{0} (arithmetical comprehension), and Π_{∞}^{1}-TI_{0} is no stronger than ATR_{0}. Thus ATR_{0} is a much better system than IR from the viewpoint of reverse mathematics.

§6. Impredicative Π_{2}^{0} Combinatorial Theorems. In the aftermath of Paris/Harrington, it has been shown that certain mathematically appealing, finite combinatorial theorems are not provable in IR or ATR_{0} or even stronger systems. In particular, such theorems are neither predicatively provable nor predicatively reducible. For a survey of this general area, see Simpson [24]. Recently Feferman [8] has cited some of these results in footnotes. We now state some of these results.

6.1. An Impredicative Ramsey-Type Theorem. Friedman/McAloon/ Simpson 1982 [11] were the first to exhibit a mathematically natural, finite combinatorial theorem which is not predicatively provable. To state their result, we need some definitions.

Definition 4. Let X be a finite set of positive integers.

1. A coloring of X is given by P (X) = C_{1} ∪ C_{2}, where C_{1} and C_{2} are closed under initial segment. A set Y ⊆ X is said to be homogeneous for the given coloring if either P (Y) ⊆ C_{1} or P (Y) ⊆ C_{2}.

2. X is said to be 0-dense if |X| ≥ 2 and |X| ≥ min X. X is said to be (n+1)- dense if for every coloring of X there exists an n-dense homogeneous set.

Theorem 5 (Friedman/McAloon/Simpson). The following statements are pairwise equivalent over PRA.

1. ∀ n ∃ n-dense finite set.

2. uniform Π_{2}^{0} reflection for IR.

3. uniform Π_{2}^{0} reflection for ATR_{0}.

6.2. Friedman’s Work on Kruskal’s Theorem. Friedman has shown that certain interesting combinatorial properties of finite trees are not provable in IR and ATR_{0} and stronger systems. See the exposition in Simpson [23].

It turns out that there is a close connection between these results and recent spectacular work in finite graph theory. Namely, Friedman/Robertson/Seymour [12] have used them to show that the celebrated Robertson/Seymour Graph Minor Theorem is not provable in Π_{1}^{1}-CA_{0}.

6.3. A Recent Result of Friedman. In order to state Friedman’s most recent result along these lines, we first give the necessary definitions.

Definition 6.

1. A tree T is a finite poset with a minimum element such that the predecessors of each element are linearly ordered. The height of x ∈ T is the number of predecessors of x in T. The height of T is the maximum height of an element of T. We say that T is of degree ≤ k if each element of T has at most k immediate successors.

2. T (≤ i) = {x ∈ T : height(x) ≤ i}.

3. T (i) = {x ∈ T : height(x) = i}.

4. T (> i) = {x ∈ T : height(x) > i}. Note that T (≤ i) is a subtree of T.

Now consider the following combinatorial statement concerning finite trees. For each k there exists n so large that the following holds. If T is a tree of height n and degree ≤ k, then there exists 1 ≤ i ≤ n and an inf-preserving embedding of T (≤ i) into T which carries T (i) into T (> i).

Friedman has recently shown that this statement is equivalent to uniform Π_{2}^{0} reflection for Π_{2}^{1}-TI_{0}. In particular, this statement of Friedman is true but not provable in ATR_{0}. See also Friedman’s contribution to this volume.

REFERENCES

[1] Ron Aharoni, Menachem Magidor, and Richard A. Shore, On the strength of König’s duality theorem for infinite bipartite graphs, Journal of Combinatorial Theory, Series B, vol. 54 (1992), pp. 257–290.

[2] J. N. Crossley, J. B. Remmel, R. A. Shore, and M. E. Sweedler (editors), Logical Methods, Birkhäuser, 1993, 813 pages.

[3] Solomon Feferman, Systems of predicative analysis, I, The Journal of Symbolic Logic, vol. 29 (1964), pp. 1–30.

[4] , Systems of predicative analysis, II, The Journal of Symbolic Logic, vol. 33 (1968), pp. 193–220.

[5] , Predicatively reducible systems of set theory, [18, part 2], 1974, pp. 11–32.

[6] , A more perspicuous formal system for predicativity, [15, volume i], 1978, pp. 68–93.

[7] , Reflecting on incompleteness, The Journal of Symbolic Logic, vol. 56 (1991), pp. 1–49.

[8] , Does mathematics need new axioms?, American Mathematical Monthly, vol. 106 (1999), pp. 99–111.

[9] Harvey Friedman, Metamathematics of Ulm theory, June 24, 1999, unpublished, 34 pages.

[10] , Systems of second order arithmetic with restricted induction, I, II (abstracts), The Journal of Symbolic Logic, vol. 41 (1976), pp. 557–559.

[11] Harvey Friedman, Kenneth McAloon, and Stephen G. Simpson, A finite combinatorial principle which is equivalent to the 1-consistency of predicative analysis, [17], 1982, pp. 197–230.

[12] Harvey Friedman, Neil Robertson, and Paul Seymour, The metamathematics of the graph minor theorem, [20], 1987, pp. 229–261.

[13] L. A. Harrington, M. Morley, A. Scedrov, and S. G. Simpson (editors), Harvey Friedman’s Research on the Foundations of Mathematics, Studies in Logic and the Foundations of Mathematics, North-Holland, 1985, XVI + 408 pages.

[14] Irving Kaplansky, Infinite Abelian Groups, revised ed., University of Michigan Press, 1969, VII + 95 pages.

[15] K. Lorenz (editor), Konstruktionen versus Positionen, beiträge zur Diskussion um die Konstruktive Wissenschaftstheorie, Walter de Gruyter, Berlin, 1978, Volume I, XX + 350 pages, Volume II, X + 406 pages.

[16] Alberto Marcone, Foundations of BQO theory, Transactions of the American Mathematical Society, vol. 345 (1994), pp. 641–660.

[17] G. Metakides (editor), Patras Logic Symposion, Studies in Logic and the Foundations of Mathematics, North-Holland, 1982, IX + 391 pages.

[18] D. S. Scott and T. J. Jech (editors), Axiomatic Set Theory, Proceedings of Symposia in Pure Mathematics, vol. XIII, American Mathematical Society, 1971–1974, Part 1, VI + 474 pages, Part 2, VI + 222 pages.

[19] Richard A. Shore, On the strength of Fraïssé’s conjecture, [2], 1993, pp. 782–813.

[20] S. G. Simpson (editor), Logic and Combinatorics, Contemporary Mathematics, American Mathematical Society, 1987, XI + 394 pages.

[21] Stephen G. Simpson, Set theoretic aspects of ATR_{0}, [27], 1982, pp. 255–271.

[22] , Σ_{1}^{1} and Π_{1}^{1} transfinite induction, [27], 1982, pp. 239–253.

[23] , Nonprovability of certain combinatorial properties of finite trees, [13], 1985, pp. 87–117.

[24] , Unprovable theorems and fast growing functions, [20], 1987, pp. 359–394.

[25] , On the strength of König’s duality theorem for countable bipartite graphs, The Journal of Symbolic Logic, vol. 59 (1994), pp. 113–123.

[26] , Subsystems of Second Order Arithmetic, Perspectives in Mathematical Logic, Springer-Verlag, 1999, XIV + 445 pages.

[27] D. van Dalen, D. Lascar, and T. J. Smiley (editors), Logic Colloquium ’80, Studies in Logic and the Foundations of Mathematics, North-Holland, 1982, X + 342 pages.

E-mail: simpson@math.psu.edu
URL: http://www.math.psu.edu/simpson/

DEPARTMENT OF MATHEMATICS, PENNSYLVANIA STATE UNIVERSITY, STATE COL-LEGE, PA 16802, USA