On Relating Theories: Proof-Theoretical Reduction
This is the latest version of this eprint.
Rathjen, M orcid.org/0000-0003-1699-4778 and Toppel, M (2019) On Relating Theories: Proof-Theoretical Reduction. In: Centrone, S, Negri, S, Sarikaya, D and Schuster, PM, (eds.) Mathesis Universalis, Computability and Proof. Humboldt-Kolleg: Proof Theory as Mathesis Universalis, 24-28 Jul 2017, Loveno di Menaggio (Como), Italy. Springer , pp. 311-331. ISBN 978-3-030-20446-4
The notion of proof-theoretical or finitistic reduction of one theory to another has a long tradition. Feferman and Sieg (Buchholz et al., Iterated inductive definitions and subsystems of analysis. Springer, Berlin, 1981, Chap. 1) and Feferman in (J Symbol Logic 53:364–384, 1988) made first steps to delineate it in more formal terms. The first goal of this paper is to corroborate their view that this notion has the greatest explanatory reach and is superior to others, especially in the context of foundational theories, i.e., theories devised for the purpose of formalizing and presenting various chunks of mathematics.
A second goal is to address a certain puzzlement that was expressed in Feferman's title of his Clermont-Ferrand lectures at the Logic Colloquium 1994: "How is it that finitary proof theory became infinitary?" Hilbert's aim was to use proof theory as a tool in his finitary consistency program to eliminate the actual infinite in mathematics from proofs of real statements. Beginning in the 1950s, however, proof theory began to employ infinitary methods. Infinitary rules and concepts, such as ordinals, entered the stage.
In general, the more that such infinitary methods were employed, the farther did proof theory depart from its initial aims and methods, and the closer did it come instead to ongoing developments in recursion theory, particularly as generalized to admissible sets; in both one makes use of analogues of regular cardinals, as well as "large" cardinals (inaccessible, Mahlo, etc.). (Feferman 1994).
The current paper aims to explain how these infinitary tools, despite appearances to the contrary, can be formalized in an intuitionistic theory that is finitistically reducible to (actually Π02
-conservative over) intuitionistic first order arithmetic, also known as Heyting arithmetic. Thus we have a beautiful example of Hilbert's program at work, exemplifying the Hilbertian goal of moving from the ideal to the real by eliminating ideal elements.
Rathjen, M https://orcid.org/0000-0003-1699-4778
Toppel, M
© Springer Nature Switzerland AG 2019. This is an author produced version of a paper published in Mathesis Universalis, Computability and Proof. Uploaded in accordance with the publisher's self-archiving policy.
Relative interpretability; Partial conservativity; Proof-theoretical reduction; Infinite proof theory; Ordinal analysis
Published (online): 26 October 2019
John Templeton Foundation (US) 60842
Available Versions of this Item
On relating theories: proof-theoretical reduction. (deposited 18 Sep 2020 15:21)
On Relating Theories: Proof-Theoretical Reduction. (deposited 13 Jun 2019 13:27) [Currently Displayed]
Filename: Relating_Theories.pdf