Predicativity through transfinite reflection
Andr\'es Cordon Franco, David Fern\'andez Duque, Joost J. Joosten and, F\'elix Lara Mart\'in
TL;DR
This paper characterizes Predicative Analysis, specifically ATR0, using stronger reflection principles, linking it to the provability framework of Elementary Arithmetic and Peano Arithmetic.
Contribution
It provides a new characterization of ATR0 through the lens of stronger reflection principles, advancing understanding of predicative analysis.
Findings
ATR0 characterized by stronger reflection principles
Connection between Peano Arithmetic and Elementary Arithmetic
Advances in formalizing predicative analysis
Abstract
Peano Arithmetic is known to be provably equivalent to reflection over Elementary Arithmetic. We prove a characterization of Predicative Analysis in the guise of ATR0 in terms of stronger reflection principles.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsComputability, Logic, AI Algorithms · Mathematical and Theoretical Analysis · Logic, programming, and type systems