TY - GEN UR - http://lib.ugent.be/catalog/pug01:1247669 ID - pug01:1247669 LA - eng TI - Reverse mathematics and well-ordering principles PY - 2011 SN - 9781848162778 PB - Singapore AU - Rathjen, Michael AU - Weiermann, Andreas WE01 802000038735 0000-0002-5561-5323 AU - Cooper, S Barry editor AU - Sorbi, Andrea editor AB - The paper is concerned with generally Pi^1_2 sentences of the form 'if X is well ordered then f(X) is well ordered', where f is a standard proof theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded omega-models for a particular theory T_f whose consistency can be proved by means of a cut elimination theorem in infinitary logic which crucially involves the function f. To illustrate this theme, we shall focus on the well-known psi-function which figures prominently in so-called predicative proof theory. However, the approach taken here lends itself to generalization in that the techniques we employ can be applied to many other proof-theoretic functions associated with cut elimination theorems. In this paper we show that the statement 'if X is well ordered then 'X0 is well ordered' is equivalent to ATR0. This was first proved by Friedman, Montalban and Weiermann [7] using recursion-theoretic and combinatorial methods. The proof given here is proof-theoretic, the main techniques being Schuette's method of proof search (deduction chains) [13], generalized to omega logic, and cut elimination for infinitary ramified analysis. ER -Download RIS file
00000nam^a2200301^i^4500 | |||
001 | 1247669 | ||
005 | 20170102095244.0 | ||
008 | 110530s2011------------------------eng-- | ||
020 | a 9781848162778 | ||
024 | a 1854/LU-1247669 2 handle | ||
040 | a UGent | ||
245 | a Reverse mathematics and well-ordering principles | ||
260 | a Singapore, Singapore b World Scientific c 2011 | ||
520 | a The paper is concerned with generally Pi^1_2 sentences of the form 'if X is well ordered then f(X) is well ordered', where f is a standard proof theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded omega-models for a particular theory T_f whose consistency can be proved by means of a cut elimination theorem in infinitary logic which crucially involves the function f. To illustrate this theme, we shall focus on the well-known psi-function which figures prominently in so-called predicative proof theory. However, the approach taken here lends itself to generalization in that the techniques we employ can be applied to many other proof-theoretic functions associated with cut elimination theorems. In this paper we show that the statement 'if X is well ordered then 'X0 is well ordered' is equivalent to ATR0. This was first proved by Friedman, Montalban and Weiermann [7] using recursion-theoretic and combinatorial methods. The proof given here is proof-theoretic, the main techniques being Schuette's method of proof search (deduction chains) [13], generalized to omega logic, and cut elimination for infinitary ramified analysis. | ||
598 | a C1 | ||
100 | a Rathjen, Michael | ||
700 | a Weiermann, Andreas u WE01 0 802000038735 0 0000-0002-5561-5323 | ||
700 | a Cooper, S Barry e editor | ||
700 | a Sorbi, Andrea e editor | ||
650 | a Mathematics and Statistics | ||
653 | a ATR0 | ||
653 | a countable | ||
653 | a coded omega-model | ||
653 | a reverse mathematics | ||
653 | a Schütte deduction chains | ||
653 | a well ordering principles | ||
773 | t Computability in Europe 2007 (CiE 2007) : Computation and logic in the real world g Computability in context : computation and logic in the real world. 2011. World Scientific. p.351-370 q :<351 | ||
856 | 3 Full Text u https://biblio.ugent.be/publication/1247669/file/1247689 z [open] y RevWO2.pdf | ||
920 | a confcontrib | ||
852 | x WE b WE01 | ||
922 | a UGENT-WE |
All data below are available with an Open Data Commons Open Database License. You are free to copy, distribute and use the database; to produce works from the database; to modify, transform and build upon the database. As long as you attribute the data sets to the source, publish your adapted database with ODbL license, and keep the dataset open (don't use technical measures such as DRM to restrict access to the database).
The datasets are also available as weekly exports.