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" <ullrich@math.okstate.edu> 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