From: kramsay@aol.commangled (Keith Ramsay) Subject: Re: proof ? Date: 24 Oct 1999 17:17:22 GMT Newsgroups: sci.math Keywords: Gentzen proof of consistency of elementary arithmetic; infinite proof In article <3811F75A.EB88E46D@math.okstate.edu>, "David C. Ullrich" writes: | Maybe someone knows what the/a point to such things is - presumably |something other than formalizing "ordinary" mathematical reasoning? |(Or, hedging to make certain I get something right, maybe infinite |proofs do have some relevance to "real" proofs, even though "real" |proofs are all finite...) Infinite proofs are used in mathematical logic in various ways. One way which I happen to have seen is in ordinal analysis. Perhaps you've heard of the Gentzen proof of the consistency of elementary arithmetic, given that epsilon-0 is a well-ordering. Gentzen was able to assign an ordinal under epsilon-0 to each proof in elementary arithmetic, and give a procedure for reducing a proof of a contradiction to a proof of a contradiction whose ordinal is smaller. That's the classic example of ordinal analysis. Ordinal analysis is more or less an attempt to get the same kind of result for other axiom systems. There are ordinal analyses of various theories of integers and sets of integers (a.k.a. theories of second order arithmetic). In the 70s they managed to analyze some impredicative theories, where sets of integers are defined in terms of properties of the set of all sets of integers. Properties of infinite proof trees can be used in an interesting way to assist those analyses. I wish I knew the details better, but situations sometimes arise where reductions akin to what Gentzen did for finite proofs can be applied to infinite proof trees. Even though the proof tree may be infinite, in some situations the structure of the tree can be defined in an elementary way. Then one can sometimes show that facts about a (finitary) formal system are related to facts about transfinite induction on those infinite trees. Consider for instance elementary arithmetic with the "omega rule", permitting inferring "for all n, P(n)" from each P(0), P(1), P(2),.... Every true statement of arithmetic has an infinite branching proof tree in a system much like elementary arithmetic but with the omega rule. The height of the tree is related to the complexity of the statement associated with it. When you allow variables ranging over sets of integers, then it's no longer quite as simple. I gather that some decades back, a nice version of Gentzen's theorem was proven using techniques like that. Rather than keep track of the complexity of the formulas which are used in certain respects in the finite proof, fold that into the structure of the infinite proof tree. I guess this permits a simpler proof than the one Gentzen had. Purists might object that this kind of infinite "proof" is too much unlike what we normally mean by proofs-- where the point is to be able to write it down and use it to inform others-- but from a proof theory point of view there are enough observed similarities to warrant calling it a more general kind of proof. They can be transformed in some of the same ways (depending upon what sort of restrictions there are on what rules are allowed in the proof). There's actually been quite a lot of study on these lines. Keith Ramsay