Journal article 1037 views
Ordinal notations and well-orderings in bounded arithmetic
,
Chris Pollett,
Samuel R Buss
Annals of Pure and Applied Logic, Volume: 120, Issue: 1-3, Pages: 197 - 223
Swansea University Author:
Arnold Beckmann
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1016/S0168-0072(02)00066-0
Abstract
Ordinal notations and provability of well-foundedness have been a central tool in the study of the consistency strength and computational strength of formal theories of arithmetic. This development began with Gentzen's consistency proof for Peano arithmetic based on the well-foundedness of ordi...
| Published in: | Annals of Pure and Applied Logic |
|---|---|
| ISSN: | 0168-0072 |
| Published: |
2003
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa13723 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
Ordinal notations and provability of well-foundedness have been a central tool in the study of the consistency strength and computational strength of formal theories of arithmetic. This development began with Gentzen's consistency proof for Peano arithmetic based on the well-foundedness of ordinal notations up to ε0 . Since the work of Gentzen, ordinal notations and provable well-foundedness have been studied extensively for many other formal systems, some stronger and some weaker than Peano arithmetic. In the present paper, we investigate the provability and non-provability of well-foundedness of ordinal notations in very weak theories of bounded arithmetic, notably the theories S i 2 and T i 2 with 1 ≤ i ≤ 2 . We prove several results about the provability of well-foundedness for ordinal notations; our main results state that for the usual ordinal notations for ordinals below ε0 and Γ0 , the theories T i 2 and S 2 2 can prove the ordinal Σ b 1 - minimization principle over a bounded domain. PLS is the class of functions computed by a polynomial local search to minimize a cost function. It is a corollary of our theorems that the cost function can be allowed to take on ordinal values below Γ0 , without increasing the class PLS . |
|---|---|
| College: |
Faculty of Science and Engineering |
| Issue: |
1-3 |
| Start Page: |
197 |
| End Page: |
223 |