Kreisel–Lévy-­type Theorems for Set Theories

Studies in Logic, Vol. 16, No. 3 (2023): 36–52 PII: 1674­3202(2023)­03­0036­17

Michael Rathjen        Shuangshuang Shu

Abstract.  A famous result, due to Kreisel and Lévy (1968), characterizes the uniform reflection principle for Peano arithmetic, RFN(PA), in terms of the transfinite induction principle TI(), namely induction up the ordinal , which is the first ordinal α such that . In this article we prove a generalization of this result germane to large swathes of set theories. These set theories T are of the following kind. They comprise Kripke–Platek set theory, KP, but their additional axioms are required to be of restricted syntactic complexity, that is, there exists a fixed n such that they are all of form. A typical example is KP + Powerset +  Separation + Collection with for some n.

The characterization of T +RFN(T) will be given in terms of an induction principle , allowing induction up to the first class ordinal α such that , where Ω stands for the class of all (set) ordinals. The definition of the class ordering is akin to that of the ordinal representation system for used in proof theory, whereby the role of the ordinal ω is now played by the entire class of ordinals. The proof that RFN(T) entails over T is fairly standard in that is uses techniques essentially developed by Gentzen. The converse entailment, though, is the hard part. In the case of PA, Kreisel and Lévy used the no­counterexample interpretation in a formalization due to Tait (1965). The idea of using a cut elimination procedure instead is owed to Kreisel and was implemented by Schwichtenberg (1977). Technically, it shows that the cut elimination procedure for infinite derivations can be engineered via a primitive recursive function for a natural (albeit quite subtle) coding of infinite derivations, which allow for delay inferences (called improper applications of the ω-­rule), where the premisses are the same as the conclusion. A mathematically rigorous and detailed account of how to work with such codes poses a considerable challenge. In this article we shall be avoiding codes for infinite derivations entirely by utilizing a detour through a fragment of Constructive Zermelo­Fraenkel set theory, CZF, in which general inductively defined classes can be handled without any problems. The exposition of this technical move in a set­theoretic context, which parallels the one by Buchholz (1997) for arithmetic, is quite interesting in its own right.

In general, the restriction on the complexity of the axioms of T that do not belong to KP is necessary. For instance, the above characterization does not extend to ZF. Indeed, ZF proves .

Naturally, other ordinal representation systems come to mind, for instance, , which was used by Feferman and Schütte to characterize the strength of autonomous progressions of theories. It would be interesting to figure out what kind of reflection principle corresponds to the induction principle for the class version of , i.e., .