FOM: proof theory and the question of consistency

Fri Apr 10 16:27:06 EDT 1998

This is a reply to Stephen Simpson's FOM posting on 9 Apr 1998 10:13:46 -0400 (EDT)
> 
> (i) The deemphasis of consistency proofs is not only my opinion.
> Feferman and other eminent proof-theorists have expressed similar
> opinions.  Indeed, are there any proof-theorists who still take the
> traditional view?  (By the traditional view, I mean the view that
> consistency proofs are a principal reason to be interested in
> Gentzen-style ordinal analysis.)
> 
> Would some of the other proof-theorists on the FOM list (Tait,
> Rathjen, Friedman, Pohlers, Takeuti, Sommer, Sieg, Buss, Kohlenbach,
> Pfeiffer, Fine, ...) care to commment on this matter?

Although I belong to the ... in the list proof theorists above, I would 
like to comment on this matter, since I am personally very much interested
in the question of consistency

1. A lot of research has been carried out recently in analyzing Martin-Loef's
type theory proof theoretically. One reason for this interest was to fulfill 
the original goal of proof theory: to prove the consistency of large theories.
In traditional proof theory we reduce the consistency of theories for 
carrying out mathematics to the well-ordering of ordinal notation systems. 
The ordinal notation systems usually used for the analysis of stronger 
theories (impredicative in the sense of proof theory, i.e. of strength
bigger the ordinal $\Gamma_0$) are usually presented in a set theoretical
way by using cardinals and even large cardinals. These large cardinals
can be replaced by their recursive analogues, but still the problem
remains that one reduces the consistency of theories to a fragment of 
the standard model of set theory, so one does not gain a real 
consistency proof.

Now, using other constructive theories one can go with this reduction one step 
further: we prove the well-ordering of the ordinal notation systems in some 
constructive theory, which we consider as intuitively consistent. Then we get 
a proof of the consistency of the original theory. The constructive theories 
replaces the finitary methods in the original Hilbert program, which didn't
suffice by Goedel's incompleteness theorem.  

Of course, what remains is the question, whether the constructive
theory used is really intuitively consistent. I personally believe that
there are very good reasons for believing in the consistency of Martin-Loef's
type theory, at least if one considers the versions with one universe and 
W-type and any extensions by inductive recursive definitions. If one 
is a little bit more sceptical one can say, that at least Martin-Loef's
type theory is defined in the best possible way to guarantee its
consistency

However, in the case of theories which go slightly beyond one recursive Mahlo 
ordinal, (they are still extremely weak relative to full set theory), the only
extension of Martin-Loef's type theory of this strength which could be 
regarded as predicative is the Mahlo-universe, developed by myself, and there 
has now for several years been a discussion about, whether this can be really 
accepted as consistent  in itself (I personally believe in the consistency
of it in itself, but of course I have as well a model for it). And
even if one accepts the Mahlo-universe, it seems to be at the moment
almost impossible to define extensions of Martin-Loef's type theory
which go substantially beyond Mahlo.  (Of course one can build
certain hierarchies of Mahlo-universes but I don't regard such extensions
as substantially stronger).

2. Another approach taken by myself is to try to present the ordinal notation
systems in a different way together with some argument, that they are 
intuitively well-ordered. 

I started this project originally, because I was all the time
facing the criticism, that proof theory is too technical and nobody can
understand it any longer. Although proof theory has become very technical
I don't think that it is much more technical than other subjects of
mathematical logic. In my opinion the real hindrance to proof theory is
the mysterious way of using large cardinals for denoting small ordinals:
it is easy to understand the proof theoretical analysis, but at the end of
it one has reduced the consistency of a theory to some --- for the 
outsider --- strange  looking ordinal notation system and the question is: 
what have we gained? Part 1. above gives a partial answer, but the question 
remains: isn't it possible to reduce the consistency of the theories considered
to constructive theories in a more direct way? Are ordinals not only a 
technical tool for carrying out this reduction, and if we can get rid of them, 
their role vanishes?

Now small ordinal notation systems (below $\Gamma_0$) and even some
extensions (so called "Schuette  Klammer Symbole") are in my opinion 
intuitively well-ordered and therefore a reduction to their
well-ordering provides a real consistency proof. This is in my opinion one 
reason, why Gentzen's result was appreciated so much, and these intuitive
well-ordering proofs make it easy to teach ordinal notation systems of this 
size.

We can formalize the intuitive argument for it's well-ordering by selecting 
systematically ordinal notations in such  a way, that the new one will be 
always chosen as the least one with respect to some termination ordering out 
of a  certain (during the process increasing) set of notations
which are well-ordered (provable in primitive recursive arithmetic relative
to the well-ordering of the ordinal notations already selected) in such
a way that the resulting sequence of ordinal notations is increasing,
exhausts all ordinal notations and is therefore well-ordered. I denote this 
process as "from below": we systematically climb up the proof theoretical 
scale and refer always only to ordinals which we have introduced before.

A complete description of this argument is given in my article Ordinal systems 
(see below).

This argument can now be extended. First I thought the Bachmann-Howard
ordinal is the limit, but I found ways of getting beyond it and the
strength I have reached up to now (although not everything is written down 
yet) is Kripke Platek set theory with one recursive Mahlo ordinal.
And Mahlo does not seem to be the end of this approach, the only limit I have  
reached up to now is  my mental  capacity.

3. Of course, whatever approach we take, we cannot bypass Goedel's results.
What we can do is reduce the consistency of theories to some principles
which we regard as less doubtful then the theories in questions. The 
consistency of the principles has to be shown by philosophical
methods, and there is always space for mistakes in such considerations,
we cannot achieve the same degree of security like in mathematical proofs.

**
References ( those marked with (*) can be found on my web-page  of articles
  http://www.math.uu.se/~setzer/articles/welcome.html)

For 1.:
S.: Well-ordering proofs for Martin-Löf Type Theory with
    W-type and one Universe. To appear in APAL. (*)
Griffor, E. and Rathjen, M.: The strength of some Martin Loef type theories,
Arch. math. log, 33, 1994, pp. 347 - 385.
S.: Extending Martin-Löf Type Theory by one Mahlo-Universe (*)
S.: A Model for a type theory with Mahlo Universe (*)

For 1. and 2.:
S.: Well-ordering proofs in Martin-Löf's Type Theory. To appear in
"25 years of constructive type theory".(*)

For 2.:
S.: Ordinal Systems (*)

----
Name: Anton Setzer
Position: Research Assistant
Institution: Department of Mathematics, Uppsala University
Research interest: Proof theory, especially of Martin-Loef Type Theory
More information: http://www.math.uu.se/~setzer

----------------------------------------------------------------------- 
Anton Setzer				Telephone:
Department of Mathematics		(national)         018 4713284
Uppsala University			(international) +46 18 4713284
P.O. Box 480 				Fax:
S-751 06 Uppsala			(national)         018 4713201
SWEDEN					(international) +46 18 4713201
-----------------------------------------------------------------------