Logic Colloquium: Infinite Ray Theorems: Complexity and Reverse Mathematics: Theorems of Hyperarithmetic Analysis
Richard A. Shore - Cornell University
A ray in a graph G = (V, E) is a sequence X (possibly infinite) of distinct vertices x0, x1, . . . such that, for every i, E(xi , xi+1). A classical theorem of graph theory (Halin ) states that if a graph has, for each k 2 N, a set of k many disjoint (say no vertices in common) infinite rays then there is an infinite set of disjoint infinite rays.
The proof seems like an elementary argument by induction that uses the finite version of Menger’s theorem at each step. One would thus expect the theorem to follow by very elementary (even computable) methods plus a compactness argument (or equivalently arithmetic comprhension, ACA0). We show that this is not the case.
Indeed, the construction of the infinite set of disjoint rays is much more complicated. It occupies a level of complexity previously inhabited by a number of logical principals and only one fact from the mathematical literature. Such theorems are called theorems of hyperarithmetic analysis. Formally this means that they imply (in !-models) that for every set A all transfinite iterations (through well-orderings computable from A) of the Turing jump beginning with A exist. On the other hand, they are true in the (!-model) consisting of the subsets of N generated from any single set A by these jump iterations.
There are many variations of this theorem in the graph theory literature that inhabit the subject of ubiquity in graph theory. We discuss a number of them that also supply examples of theorems of hyperarithmetic analysis as well as classical variations that are proof theoretically even stronger.
This work is joint with James Barnes and Jun Le Goh.
If time permits we will also discuss a new class of theorems suggested by a "lemma" in one of the papers in the area. We call them almost theorems of hyperarithmetic analyisis. These are theorems that are proof theoretically very weak over Recursive Comprehension (RCA0) but become theorems of hyperarithmetic analysis once one assumes ACA0.