tag:blogger.com,1999:blog-11295132.post4843004274672094532..comments2017-10-18T21:14:59.419-07:00Comments on A Neighborhood of Infinity: What's the use of a transfinite ordinal?Dan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger3125tag:blogger.com,1999:blog-11295132.post-10360564929820220192009-01-27T21:36:00.000-08:002009-01-27T21:36:00.000-08:00Gentzen proved Peano arithmetic consistent using o...Gentzen proved Peano arithmetic consistent using ordinals (up to epsilon nought). This was a few years after Goedel showed it couldn't be done from within Peano arithmetic. It drives me nuts that people still claim nobody has proven arithmetic is consistent.<BR/><BR/>Incidentally, does anyone know of the relationship between the use of ordinals for strong normalization proofs and the use of logical relations for the same?Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-84433143615508820022008-10-18T17:20:00.000-07:002008-10-18T17:20:00.000-07:00Pseudonym,Yes, I read that recently in Davey and P...Pseudonym,<BR/><BR/>Yes, I read that recently in Davey and Priestley's "Lattices and Order".sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-6848926379371324392008-10-18T17:10:00.000-07:002008-10-18T17:10:00.000-07:00The use that I was introduced to may years ago is ...The use that I was introduced to may years ago is that mathematical induction works on transfinite ordinals. (You need to prove two induction steps: One is the successor ordinal case, and the other is the limit ordinal case.)<BR/><BR/>The reason why this is useful is that there are some "find the fixpoint" methods that don't terminate even after ω steps, but they do terminate some time after that. So if, say, you need to find the greatest fixpoint of a functional, sometimes you need to go further than ω.Pseudonymhttps://www.blogger.com/profile/04272326070593532463noreply@blogger.com