litow@uwm-cs.UUCP (Dr. B. Litow) (10/08/87)
Recently a poster observed that first order theory of arithmetic (with a complete induction rule) can be proved consistent via transfinite induction. This of course is correct and was first proved around 1937 by Gerhard Gentzen (induction up to the ordinal "epsilon-sub 0"). The poster went on to point out that this proof cannot be formalized within 1st order arithmetic. This should not suggest that induction up to any definite countable ordinal is 'exotic'. Gentzen's proof and the Proof Theory which emerged from it are as clear and secure as any proof methods known. I suppose that transfinite induction at an ordinal above the Church-Kleene ordinal is possibly open to question. However,I think that it must be possible to give induction at "omega-sub 1" an unequivocal meaning. Perhaps someone working in recursion theory or set theory can assist here. In fact most of the theories of arithmetic including 2nd order theories are really very weak in an important sense. Various partition properties which are almost obvious and which have transparent proofs in set theory have been shown not to be provable in these sorts of arithmetic theories. I believe the earliest results of this kind were obtained around 1978 by Leo Harrington and Jeff Paris. The basic idea seems to be that one can construct recursive functions and relations such that their 'well-definedness' cannot be proved in these arithmetic theories. I believe that a strong recursion-theoretic interpretation of incompleteness is emerging from these unprovable sentences (they can all be written down in the theories) which shows that the notion of 'self-reference' is ancillary to unprovability. This is similar to the secondary importance of self-reference to the recursion theorem and inherent limitations on recursiveness. From a philosophical perspective it seems to me that there are at least two leesons to be drawn from incompleteness. First,it is useful and fairly easy to stand outside such systems and make general observations about the forms of proofs and classes of sentences in the theory. Second,it is possible but not easy to develop new concepts (often but not exclusively as axioms) which vastly extend the system. This is best illustrated by 1st order logic extended by '=' and 'element_of" together with the ZF axioms. It is not an easy task because axiom of choice,determinateness,etc. are still not well understood. In a way the partition properties can be viewed as 'transcendental' properties but they are devoid of semantics. They are properties that fall under the notions of ZF. What is missing from these subjects is any kind of system development or morphogenesis. I maintain that this is relevant to beliefs,cognition,etc. and that it is just this which cannot be studied via formal system concepts at least in their current state of development.