The Strength of Predicative Abstraction
Sean Drysdale Walsh · arXiv (Cornell University) · 2014
Frege’s theorem says that second-order Peano arithmetic is interpretable in Hume’s Principle and full impredicative comprehension. Hume’s Principle is one example of an abstraction principle, while another paradigmatic example is Basic Law V from Frege’s Grundgesetze. In this paper we study the strength of abstraction principles in the presence of predicative restrictions on the comprehension schema, and in particular we study a predicative Fregean theory which contains (i) all the abstraction principles whose equivalence relations can be proven to be equivalence relations in a weak back-ground second-order logic, as well as (ii) a form of global choice (cf. Definition 2.7). Our main theorem shows that this predicative Fregean theory interprets a variant KPN∗ of Kripke-Platek set theory KP (cf. Theorem 3.2). Since this theory KPN ∗ in turn inter-prets the predicative subsystem Σ11-AC of second-order Peano arithmetic, we obtain a predicative analogue of Frege’s theorem. The proof of this result proceeds by using the set-theoretic resources of the Grundgesetze to emulate the definitions featuring in the von Neumann relative consistency proof of the axiom of foundation (cf. Definition 3.1), and by using an abstraction principle related to the Burali-Forti paradox to reduce the complexity of testing for well-foundedness.