Proof Theory on the eve of Year 2000

Date: Fri, 3 Sep 1999 18:14:06 +0200
From: Anton Setzer 
To: sf@csli.Stanford.EDU
Subject: Re: Proof Theory on the eve of Year 2000

Dear Sol,

here are my personal points of view with respect to your questions.
I have decided that either I write a quick answer to them or I 
will never write anything, so I have decided to write a fast answer
(and therefore I might not have thought well enough about it).
The following might be distributed.

In the following I am referring to proof theory in the original
Hilbert sense, i.e. that part of it concerned with the question
of the consistency of mathematical axiom systems and direct
descendants of it, mainly ordinal analysis (including for instance 
Pi^1_2-logic)
This is of course only a very small part of the subject, but its 
the part of it, which really concerns me, and I have 
not enough knowledge to say a lot about other parts.

The following is of course a very personal point of view, coming from
a very specific angle, so I expect disagreement.  
 

1. What are, or should be the aims of proof theory?

The original goal of proof theory due to Hilbert was, to
prove the consistency of mathematical axiom systems by finitary
methods. Since finitary methods do not suffice, we have to replace
them by principles for which we have good reasons for believing
in them, or even have philosophical arguments for their correctness.
Such a reduction should be in my opinion the main aim of proof theory.

Another aim is, to compare theories with each other, especially
by determining the proof theoretic strength, in order to get an
as broad as possible picture of the proof theoretic landscape. 

2. How well has it met those aims?

I think very well, proof theory has reached quite a big strength,
constructive theories and semi-constructive theories of all kinds
have been found (ranging from ID_n, ID_alpha and extensions of 
Kripke-Platek set theory, which I regard as "semi-constructive" theories 
which already provide some reduction, up to real constructive
theories, most prominently constructive set theory, variations
of T_0 and variants of Martin-L"of type theory). 
And we have a very detailed picture of the landscape of proof theory,
were we are able to compare completely different paradigms. 

Further weak theories have been very well explored, so we know that
a large part of mathematics can be carried out in weak systems
of strength less than or equal ID_<\omega, an area 
which is so well explored that I think we can absolutely trust 
in the consistency of the corresponding theories.
And we have as well quite a good knowledge of weaker theories,
like bounded arithmetic.

3. What developments or specific achievements stand out?

First of all, we have to analyze stronger theories, Pi^1_n-CA and finally
ZF. And the area, recently reached by Rathjen and Arai, is
not very well understood yet, especially some other researchers
have to do some research on it and constructive counterparts have to
be found.

4. What, now, are the main open problems?

See 3.

5. Are there any neglected directions in proof theory?

- There is still some imprecision with what is meant by proof theoretic
  strength (which can probably only be made precise for certain 
  subclasses of theories).
- Every proof theoretist essentially starts from scratch (even
  M. Rathjen defines in his notes on the notation system for Pi^1_2-CA 
  the Veblen function). I think some more uniform methods
  are needed, or some more general concepts. However, I have little
  hope at the moment that somebody deals with such questions.

6. In what ways can or should proof theory relate to other parts of
logic/foundations/mathematics/computer science/linguistics/etc.?

- Other parts of logic: It seems that we can learn a lot from
  recursion theory and from set theory. On the other hand, 
  the area beyond Mahlo seems not to have been sufficiently studied
  in recursion theory, so the proof theoretic development in this
  region might still inspire some fruitful 
  development there (although because of the growing importance of 
  computer science it might not be tackled in the near future).

- Philosophy: I think proof theory is mainly dealing with 
  foundations, and after some mathematical reduction steps we will always
  end up with some principles, which can only be validated by 
  philosophical arguments. Here interaction with philosophy is required.

- Mathematics: Maybe we can learn something from the development
  of Algebra, how to find more abstract concepts. And there are 
  probably many more methods from all areas of mathematics, which
  could be used in proof theory.

- Computer science: I think proof theory can contribute a lot to
  computer science: we constructivize certain theories, which corresponds
  to data structures and programming principles. Most prominently I think
  the analysis of inductive definitions has led to an understanding
  of them, and because of this understanding they have become so 
  important in   computer science. Stronger principles should over
  time find their way as well into computer science, and 
  proof theoretic insight should be applied to problems in computer 
  science.
  On the other hand, questions coming from computer science might
  (and already do) motivate proof theoretic research (for instance 
  questions like   the extraction of programs from proofs, questions 
  about how to model constructive theories intended to be used in 
  computing etc.)
 
  I see the relationship to computer science similarly to the relationship
  between mathematics and physics: physics has stimulated a lot
  of new ideas in mathematics, mathematics was always been concerned with 
  giving precise proofs for what physicists proved in an imprecise way,
  and with formalizing "hacks" of physicists, and of course mathematics
  has contributed very much to physics.

  - Linguistics: I know to little about it to say something about it.
 

7. Where do you think the subject is heading?
   Where do you think it should be heading?

One direction is to move more and more into computer science. 
In some sense it is good, because we get motivations and new ideas.
I see some problem however in that attention towards foundational 
aspects and "strong proof theory" reduces too much, and that
too much weight is laid on applications rather than substantial
progress in the field. I think we should
see ourselves as proof theoretists who know where they are coming
from, and who from having a solid basis in proof theory look
at interesting problems in computer science, to which proof theory 
can contribute something.

Another, rather healthy direction seems to be, to move to stronger
and stronger theories, and in my opinion our understanding  of
the area up to Pi_3-reflection has grown very fast in the last years,
and at the moment we are about to get an understanding of 
stability.


8. Do you think more students/researchers should be involved in the
subject?  If so, how can they be encouraged to do so?

In general I think it is nice that it is not a too big area. And
maybe with more researchers we wouldn't make much more progress. 
I see only a problem in, that in the area of very strong proof theory
(concerned with big ordinals) not many researchers are involved and there 
is lack of a new generation following, so here something has to be done.

If I knew how to encourage more people, I would do so, but I don't
know.


9. Do we need more/different kinds of general expository texts?  What
about specialized texts?

I am planning a proof theory course for next year, and I have decided
that there is no book which is really suitable for the part dealing 
with impredicative proof theory, mainly because
the H-controlled derivations have changed the methods very much.
So there is need for 
 - some book suitable for courses, which  includes some impredicative
   proof theory
-  and as well a big monograph of "state-of-the-art" proof theory.



10. Overall, how would you rate the state of health of our subject?  What
is its promise for the future? 

I think there is some danger that "strong  proof theory" will die out
sooner or later, because it becomes too complicated and there are
too few people left. But I hope this will not happen. 
A big problem for me are the many wars of all kinds within proof theory. 
Maybe this lies in the nature of in subjects which have to deal
with foundational questions that people develop very divergent
points of view of what is important and that therefore conflicts
arise. On the other hand, in my opinion, if there is a real "enemy",
then it is the world outside proof theory, and we should concentrate
more on this enemy, or better to say, have to convince the real
world about the importance of our subject, rather than concentrating
on internal wars. 


Anton 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

Visiting address:
Polacksbacken, Laegerhyddsvaegen 2,
House 2, room 138
-----------------------------------------------------------------------

Date: Sun, 5 Sep 1999 14:56:52 -0400 (EDT)
From: urquhart@urquhart.theory.toronto.edu
To: sf@csli.Stanford.EDU
Cc: urquhart@urquhart.theory.toronto.edu
Subject: Re: Proof Theory on the eve of Year 2000


Dear Sol:

Thanks for sending your questions.  Here are a few comments and answers:


1. What are, or should be the aims of proof theory?

I don't have a lot to add to Georg Kreisel's extended reflections
on this subject.  I would agree with him that people no
longer look to proof theory for epistemological security (like Hilbert).
That being so, it seems to me that proof theory has two inter-related
aims:

(a)  A philosophical/foundational project of clarifying the nature of
mathematical proof, in particular making clear the logical strength and complexity
of various assumptions and theorems;

(b)  A purely technical project of extracting algorithms from proofs
and estimating their complexity.

2. How well has it met those aims?

I think rather succesfully, in the sense that the work on proof theory
since Gentzen has given us an incomparably clearer picture of the nature
of mathematical proof than the early pioneers of logic had.  This clarification
is so great that many things which used to be considered arcane (like estimating
the complexity of axiom systems) is now a matter of routine.

A remark under 1(b) is that proof theory may shortly become technologically
quite significant, in view of the fact that recent computer standards
for internet protocols demand a provably correct algorithm.  The intellectual
background for such proofs of correctness is of course that of classical proof theory.

3. What developments or specific achievements stand out?

Well, of course, Gentzen's classic work, Herbrand's analysis, 
Kreisel's work on the no-counter-example interpretations, 
the work of Feferman and his collaborators on ordinal analysis.
Hmm ... I don't consider myself a professional proof theorist, so I had better
stop here or risk showing my ignorance.

4. What, now, are the main open problems?

No question in my mind:  NP =? co-NP and related questions of propositional
proof complexity.

5. Are there any neglected directions in proof theory?

I am disappointed more proof theorists don't work on propositional proof 
complexity.  So far, it's mostly been the domain of computer scientists.

6. In what ways can or should proof theory relate to other parts of
logic/foundations/mathematics/computer science/linguistics/etc.?

I've answered that, I think, implicitly, in some of my answers above.

7. Where do you think the subject is heading?
   Where do you think it should be heading?

See answer to #5 above.

8. Do you think more students/researchers should be involved in the
subject?  If so, how can they be encouraged to do so?

That's a little tough, but one thing I would like to see is more
emphasis in the literature on open problems.  In my opinion, logicians
are rather poor at this, compared to other mathematicians.  

9. Do we need more/different kinds of general expository texts?  What
about specialized texts?

At the moment, I think the subject is fairly well served, particularly
since Sam Buss's excellent "Handbook of Proof Theory" appeared.  
There are good expositions by Schuette, Girard, Schwichtenberg
and others of the classic material, and also more recent material 
by Krajicek, Pudlak, and others.  

10. Overall, how would you rate the state of health of our subject?  What
is its promise for the future? 

Proof theorists always seem to be worrying about the health of their subject.
I suppose this is a delayed reaction to the collapse of the romantic dreams
of the Hilbert programme.  Or perhaps it's a reflection of the fact that
proof theory is a rather distant descendant of Kant's critical philosophy.
Hard to say.  Anyway, speaking as a kind of outsider, I think the subject is
pretty healthy, and it should definitely take pride in the fact that 
it contains one of the most fundamental open problems in logic (I mean
NP =? co-NP, of course).




Alasdair Urquhart



Date: Sun, 5 Sep 1999 15:25:38 -0400 (EDT)
From: urquhart@urquhart.theory.toronto.edu
To: sf@csli.Stanford.EDU
Cc: urquhart@urquhart.theory.toronto.edu
Subject: Re: Proof Theory on the eve of Year 2000


Dear Sol:

Well, yes, I think that NP =? co-NP is definitely a problem in 
proof theory.  It is most naturally stated in terms of the size
of propositional proofs of tautologies.  So, here we have the most
basic form of classical reasoning, truth-functional reasoning, and
we are asking whether there is a short proof for any tautology
("short" being defined as "polynomially bounded").  I can't think
of a more natural problem in proof theory.  Add to this that it
is closely connected with the proof theory of feasible arithmetic,
and it seems clear to me that it is a classic problem of proof theory,
though one that was quite unconsidered by the early pioneers.

There's a tendency in the proof theory community, I think, to 
restrict attention to the problems that are amenable to the 
classical techniques.  Propositional proof complexity falls largely
outside these, since cut elimination is of no help
in most cases.  I am all in favour of defining proof theory broadly,
though, as Sam Buss did in his recent Handbook.  This broadening
of scope can only be good for the health of the subject.

It's a striking fact to me that some of the most interesting recent extensions
of the concept of proof, such as that of a probabilistically checkable
proof, have come from outside the proof theory community.   These are 
not proofs in the classical Hilbert sense, of course, but from a foundational
point of view, if you define "proof" as something that convinces you, then
they really do seem to be proofs in that sense.   

Best regards,
Alasdair

Date: Mon, 6 Sep 1999 21:26:45 -0700
From: Michael Beeson 
To: Solomon Feferman 
Subject: Re: Proof Theory on the eve of Year 2000

1. What are, or should be the aims of proof theory?

    Originally, the aim was to give consistency proofs for mathematical
theories.   That was, as I understand the matter, the aim of both Hilbert
(pre-Goedel) and Gentzen (post-Goedel), and was still the aim in the fifties
when bar-recursive functionals were introduced to give a consistency proof
of analysis.  Later this aim was refined to the present apparent aim of
classifying and stratifying mathematical theories according to
"proof-theoretic strength".

2. How well has it met those aims?
   I think it has met them very thoroughly indeed, in view of the
fundamental limitations of which we are now aware.

3. What developments or specific achievements stand out?
   This you would know far better than I!

4. What, now, are the main open problems?
    Within that research program, there are only technical questions
remaining.

5. Are there any neglected directions in proof theory?
    I think that the aim of giving an account of mathematics as it actually
is done has never been taken seriously.

6. In what ways can or should proof theory relate to other parts of
logic/foundations/mathematics/computer science/linguistics/etc.?

  I have used some elementary ideas from proof theory in the design and
construction of software for mathematics education (Mathpert Calculus
Assistant).   Good examples of the relations between proof theory and
computer science would be the discovery of 2nd-order lambda-calculus and
the way that the computer language ML developed, although I don't really know
the history--perhaps proof theory was not involved in the history of ML.
It seems to me that there are various social pressures to show "applicability"
of research and that these pressures sometimes lead researchers to
exaggerate the depth of [potential] connections of their work to other
subjects.

I was very impressed with Montague semantics when studying natural
language processing.  It's a good example of a fruitful application of, 
if not proof theory itself, then tools that were invented by proof theorists
for proof theory.  I still think it could be developed further, but as far
as I know, those who are doing natural-language processing aren't using
it.

7. Where do you think the subject is heading?

More theories will be constructed, and more variants of existing theories,
and they will be interpreted one in the other, and after heavy labors,
ordinals will be assigned.

 Where do you think it should be heading?

Well, in my ignorance, I would say that the subject is just about
"finished".   Of course, that has been said of other subjects in the past
[for example, inorganic chemistry]  by other foolish mortals,  and of course
it can turn out that the subject fires up again in a rush of new and amazing
discoveries.  I can't imagine what they will be, but see the "promise for
the future" question at the end.

8. Do you think more students/researchers should be involved in the
subject?  If so, how can they be encouraged to do so?

Try me as a test case.   I have a sabbatical next year (calendar 2000), and
I haven't decided what to do with it. I could work on
   (a) branch points of minimal surfaces
   (b) developing more mathematical software for the Web
   (c) learning computational biology
   (d) some new and exciting project in proof theory.

Tempt me!   (b) and (c) have the "fire of the times" in them, while  (a) has
"timeless beauty".

9. Do we need more/different kinds of general expository texts?

Aren't you happy with Swichtenberg and Troelstra?  I thought it filled a
serious gap.

What about specialized texts?

Well, the texts of Takeuti and Schutte are pretty hard to read.  I'm sure
you could write a MUCH better one.  I doubt if anyone else could.

10. Overall, how would you rate the state of health of our subject?

It's a very mature subject, but in no danger of dying.  Its main results are
gems that will be contemplated by logicians for millennia to come.

What is its promise for the future?

Over the long-term, I think the QED project is fascinating and inevitable,
and I think proof theory should begin laying the foundations, by developing
tools that take into account the structure of mathematical theories.  The
traditional logical theories abstract away much of mathematical practice in
order to arrive at the "essence" of the matter, to facilitate
metamathematical studies.   Now that we have succeeded in analyzing the
essence, perhaps it's time to put back what was abstracted away.   This was
part of the motivation for my various papers on proofs and computation.   I
would like to see theories constructed and studied that directly account for
published mathematics.   This means paying attention not only to the role of
computation, but also to the organization of mathematical theories,
corresponding to what in computer science is called "inheritance".
The Mizar project has begun to formalize mathematics, but without the aid of
proof theorists.  There is no "theory of theories" and mathematics in Mizar
has no organization at all, it's just a collection of different computer
files, each containing some mathematics.   The hardest part of working in
Mizar is finding what has already been proved "somewhere".   Is this just a
problem to be handled with an ordinary database, or is there some proof
theory to be done?   Of course if there is proof theory, it isn't the
traditional kind.   But there is a lot of work to be done before QED can be
properly implemented (funding questions aside), and some of it could
probably be considered "proof theory".

Date: Tue, 7 Sep 1999 15:44:01 -0400 (EDT)
From: Gaisi Takeuti 
To: Solomon Feferman 
Subject: Proof Theory

Dear Sol,
I am now concentrating in some specific problem. So I don't claim that I 
have a nice global view of proof theory.  Nevertheless I have an impression 
that proof theory is doing very well in many diversified directions.  
I think that is healthy. Of course I would be happier if more people 
would work on Bounded Arithmetic related to complexity theory.
 Gaisi

Date: Wed, 8 Sep 1999 13:56:03 -0700 (PDT)
From: Sam Buss 
To: sf@csli.Stanford.EDU
Subject: Re: Proof Theory on the eve of Year 2000

Sol,

   I attach below some of my answers to at least some of
your questions.   I'd be interested in hearing the results
of your poll, and the conclusions you reach for your talk.
In particular, I am participating in a panel at the Annual
ASL meeting next summer, on the "Prospects for Mathematical Logic 
in the 21st Century", so the results of your questionaire
may be helpful to me in forming my own thoughts for the
panel.
   So caveats: my own viewpoint is at least as much from
the viewpoint of theoretical computer science as from logic.
And please treat my comments as initial thoughts rather
than fully worked-out opinions. 
 
 --- Sam

> 1. What are, or should be the aims of proof theory?

==========
SHORT ANSWER:

Understand the nature of *formal* reasoning, its relationship
to informal reasoning, and its use in mathematics and other
areas.

=================
FOR A LONGER ANSWER, see my opening discussion in the Handbook
of Proof Theory.  In the first sentence of the first chapter in 
Handbook, I wrote:

  "Proof Theory is the area of mathematics which studies the
  concepts of mathematical proof and mathematical provability."

This was followed by two paragraphs about the difference between
formal and social proofs, and then by 

  "Proof Theory is concerned almost exclusively with the study of
  formal proofs: this is justified, in part, by the close connection
  between social and formal proofs, and it is necessitated by the fact
  that only formal proofs are subject to mathematical analysis."

I then listed four main tasks of proof theory:  covering a) proof-theoretic
strengths of particular formal systems, b) the study of proofs as objects,
c) extraction of additional information (e.g., computational or 
constructive) from proofs, d) computer-based search for/construction of
proofs.

> 2. How well has it met those aims?
> 
> 3. What developments or specific achievements stand out?
> 
> 4. What, now, are the main open problems?

The aims have been spectacularly recognised in some respects:
  the existence of sound and complete proof systems for first
  order logic, proof-theoretic strength of formal systems,
  structural proof theory (cut elimination, etc.), relationships
  between provability and sub-recursive hierarchies, constructivity,
  predicativity  and impredicativity, independence results for 
  arithmetic and set theory.

Much progress remains to be done in other "big" problems:
	* Better understanding of "social proofs", i.e., the use of
		intuition (geometric or otherwise) in creating and
		understanding proofs.  Understanding the relationship 
		between social proofs and formal proofs
	* The P/NP problem and related problems in complexity theory,
		including problems about proof complexity.
	* Computerized proof search and computer aided proof construction
		is widely used, but almost no mathematical theory is
		known about the effectiveness or optimality of present-day
		algorithms (This may involve settling the
		P vs NP problem, but also includes investigations
		into strong proof systems such as type systems,
		explicit mathematics, strong constructive proof systems, ...)


> 5. Are there any neglected directions in proof theory?
>
> 6. In what ways can or should proof theory relate to other parts of
> logic/foundations/mathematics/computer science/linguistics/etc.?

Proof theory is the area of logic best equiped
to deal with problems outside of mathematics.  It is, or should be, 
widely used in computer science, linguistics, articifial intelligence,
knowledge engineering, etc.  Of course, it has serious contenders
for relevance to these areas, including contenders like neural nets, etc.
So it is frankly unclear whether logic will, in the end, be useful
for these areas.  But I think it *should* be used in these areas.

> 7. Where do you think the subject is heading?
>    Where do you think it should be heading?
> 
> 8. Do you think more students/researchers should be involved in the
> subject?  If so, how can they be encouraged to do so?
> 
> 9. Do we need more/different kinds of general expository texts?  What
> about specialized texts?
> 
> 10. Overall, how would you rate the state of health of our subject?  What
> is its promise for the future? 


  In general, I am dismayed by the relatively low level of knowledge
and low level of interest held by mathematicians for the subject of
logic in general (this applies in spades for proof theory).  Logic
courses have more-or-less vanished from the undergraduate mathematics
curriculum. (My comments here apply only to the US).
  To a lesser extent, theoretical computer science also seems to 
have a dearth of PhD students, presumably because of the poor academic 
employment opportunities in theory of computer science. 

  Proof theory needs, on the one hand, to become more relevant to
working mathematicians and to the foundations of mathematics;
and, on the other hand, to deepen its applications to areas
such as computer science, linguistics, knowledge theory, etc.

   -- Sam Buss
 

Date: Thu, 9 Sep 1999 15:45:33 -0400 (EDT)
From: Neil Tennant 
To: sf@csli.stanford.edu
Cc: neilt@mercutio.cohums.ohio-state.edu
Subject: my tuppenceworth

Sol,
thanks for sending me your questionnaire. Here is my set of answers.
Best,
Neil


1. What are, or should be the aims of proof theory?

An understanding of the structure of proofs in rigorous discourses
including, but not limited to, mathematics.

2. How well has it met those aims?

Moderately well, at least for mathematics.

3. What developments or specific achievements stand out?

The discovery of "separable" rules for the logical operators, making
inferential theories of meaning possible; the characterization of
(thus far, only rather weak) normal forms for proofs.
Relative consistency proofs.

4. What, now, are the main open problems?

Development of an expressively richer language and proof-theory for
the various branches of mathematics, so that the formal proofs
provided by the proof-theorist are more nearly homologous to
(refinements of) those found by the mathematician.

5. Are there any neglected directions in proof theory?

Use of normalization theorems as constraints on automated proof-search.

6. In what ways can or should proof theory relate to other parts of
logic/foundations/mathematics/computer science/linguistics/etc.?

See (5).

7. Where do you think the subject is heading?

Can't really say; there is a great deal of technical work whose
overall direction is difficult to evaluate.

   Where do you think it should be heading?

It should be trying to create an overall science of rigorous
reasoning, which will both illuminate the logical structure of mature
deductive sciences and provide the tools for their further development
with the aid of automated reasoners.

8. Do you think more students/researchers should be involved in the
subject?  If so, how can they be encouraged to do so?

Yes---by stressing the prospects afforded by (7).

9. Do we need more/different kinds of general expository texts?  What
about specialized texts?

There is a dearth of good expository texts; and the specialized texts
contain little in the way of fruitful applications that might entice
graduate students into the area.

10. Overall, how would you rate the state of health of our subject?  What
is its promise for the future? 

Its health is not particularly good. Proof theory is vastly
undervalued and underrated compared with model-theoretic semantics,
especially by philosophers. 

Its promise for the future, given the explosion of computer science,
will be realized by a proper theoretical alliance with automated
reasoning. 

Date: Tue, 14 Sep 1999 11:43:43 -0600
From: detlefsen.1@nd.edu
To: Solomon Feferman 
Subject: Re: Proof Theory on the eve of Year 2000 (fwd)

Thanks, Sol. I have a few responses to make. Hope it proves to be of some
use to you.
Best,
Mic

-------------------------------------------------------------------------
>
>1. What are, or should be the aims of proof theory?

I have to admit that when I read work in proof theory I am sometimes at a
loss as to what its aims are. As regards what its aims should be, I like
Hilbert's answer.

"Our formula game that Brouwer so deprecates has, besides its mathematical
value, an important general philosophical significance. For this formula
game is carried out according to certain definite rules, in which the
technique of our thinking is expressed. These rules form a closed system
that can be discovered and definitively stated. The fundamental idea of my
proof theory is none other than to describe the activity of our
understanding, to make a protocol of the rules according to which out
thinking actually proceeds. Thinking, it so happens, parallels speaking and
writing: we form statements and place them on behind another. If any
totality of observations and phenomena deserves to be made the object of a
serious and thorough investigation, it is this one ..." Foundations of
Mathematics, p. 475 (van Heijenoort)

He went on to say that use of the classical principles of logical reasoning
was particularly central and important to our thinking, that thinking has
been conducted in accordance with them ever since thinking began (vH, 379)
and that reasoning which proceeds in accordance with them is 'especially
attractive' (l.c., 476) because of its 'surprising brevity and elegance'
(ibid.). Taking classical logical reasoning away from the mathematician, he
then famously said, would be like taking away the telescope from the
astronomer and depriving the boxer the use of his fists. In a somewhat less
passionate statement he remarked that 'we cannot relinquish the use ... of
any ... law of Aristotelian logic ... since the construction of analysis is
impossible without them' (l.c., 471).
>
>2. How well has it met those aims?

I don't think that the aims announced by Hilbert have been well met by
proof theory. In particular, I think:

(i) That there has been little if any significant progress in saying
exactly in what the efficiency of classical logical reasoning (the
so-called 'brevity and elegance' that so impressed Hilbert) consists. What
is needed, it seems to me, is development of a notion of complexity (and a
metric for measuring it) that is concerned with the relative difficulty of
discovering proofs, not the difficulty of verifying (or falsifying) a GIVEN
sequence of formulae as a proof in some given system. The former, and only
the former, it seems bears any interesting relation the 'brevity' that
Hilbert was interested in. He classical logical reasoning because he
thought it made proofs easier to find. He was thus interested more in what
might be called the 'inventional' complexity of proofs (i.e. the complexity
of finding proofs) than in the 'verificational' complexity of proofs (i.e.
the complexity of verifying of a sequence that it is a proof). So, at any
rate, it seems to me. As mentioned, I don't believe that proof theory has
made much progress in analyzing this crucial notion of complexity.
>
>3. What developments or specific achievements stand out?

The analysis of the notion of a computable function. Goedel's and Church's
theorems. The work by Hilbert-Bernays, Loeb, Kreisel, Feferman, Jeroslow
and others that bears on our understanding of what a formal system is and
what serves to distinguish co-extensive formal systems from one another.
(This bears on the fundamental question of theory-identity.) Gentzen's
attempts to describe 'natural' logical reasoning.
>
>4. What, now, are the main open problems?
>
>5. Are there any neglected directions in proof theory?

Yes, see answer to (2).
>
>6. In what ways can or should proof theory relate to other parts of
>logic/foundations/mathematics/computer science/linguistics/etc.?
>
>7. Where do you think the subject is heading?
>   Where do you think it should be heading?
>
>8. Do you think more students/researchers should be involved in the
>subject?  If so, how can they be encouraged to do so?
>
>9. Do we need more/different kinds of general expository texts?  What
>about specialized texts?

I think more and better expository works are needed in every field of
logic. Proof theory is no exception. I would like to see a different type
of expository text, though ... namely, one that made more effort to relate
technical developments to the historical and philosophical origins of the
subject (such as those enumerated by Hilbert in the remarks quoted in the
answer to (1)).
>
>10. Overall, how would you rate the state of health of our subject?  What
>is its promise for the future?

Date: Tue, 14 Sep 1999 21:39:24 +0200 (MET DST)
From: Sergei Tupailo 
To: Solomon Feferman 
Cc: Sergei Tupailo 
Subject: Re: Proof Theory on the eve of Year 2000


Dear Sol,

Thank you very much for sending your questionnaire. I felt I have
something to say concerning some of your questions.

Sergei

-------------------------------------------------------------------

4. What, now, are the main open problems?
5. Are there any neglected directions in proof theory?
6. In what ways can or should proof theory relate to other parts of
logic/foundations/mathematics/computer science/linguistics/etc.?

Here I am talking mostly about the area of proof-theoretical analysis,
or any investigations of proof-theoretically strong systems
(significantly stronger than KPM).  It's worrying that work in that
area depends so much on a huge amount of technical/combinatorial
details. One can learn main methods of proof theory, and with
sufficient time and patience get through all technicalities which you
encounter when applying them to a particular system, but this, I
believe, should not take so much effort and time of proof
theorists. What seems to be missing in this field is more
conceptual/mathematical viewpoint what is happening and why things
work. One very often has an initial feeling that a particular method
works/doesn't_work in a given setting, but there is no way to prove
this except checking hundreds of cases, which are again very similar
to the situations where you have been before. It would be good if at
least sometimes one could just refer to a general theorem, applicable
to a variety of situations, instead.  The amount of "mathematics of
metamathematics", as far as proof-theoretical analysis is concerned,
seems to be way too small.

Down to specific problems, it would be good to see analysis of
power-set axiom, for example full second order arithmetic, in the
foreseeable future, but hopefully not for the expense of having proofs
infinitely more complicated.


7. Where do you think the subject is heading?

It seems to me that unless proof-theoretical analysis finds a way to
reduce its technical burden, it has a prospect to die out.


9. Do we need more/different kinds of general expository texts? 

Yes, we do. It's a shame that excellent "mainstream" mathematicians
very often have no clue of main-objectives/achievements/basic-facts of
proof theory. The question which I have to answer most often in
mathematical audiences is "What is proof theory about?" I think much
more elementary, even popular, texts, accessible to every
mathematician/graduate-student, explaining motivations, the basics and
main achievements of the subject, are necessary. After all, proof
theory was born from the concerns about foundations/consistency of
mathematics, and not every mathematician is ignorant about those
questions. I wouldn't want to see proof-theory's ties with mainstream
mathematics/mathematicians to loosen even more than they seem now.

Date: Wed, 15 Sep 1999 18:00:05 -0400 (Eastern Daylight Time)
From: Jeremy Avigad 
To: Solomon Feferman 
Subject: Re: PT on the eve of Y2K


Dear Sol,

I would have liked to have more time to think about these questions, and I
would have liked to polish these answers. But given my busy semester, this
will have to do. I hope you find these comments useful.

Cheers,

Jeremy


1. What are, or should be the aims of proof theory?

I'd rather not be dogmatic about this: lots of things go on in proof
theory that are only tangential to my own personal interests, but are
nonetheless interesting and important. So I will discuss the aspects of
proof theory that *I* am attracted to, without claiming that these are the
only legitimate motivations. 

I think that today one can distinguish between "traditional" and "modern"
aspects of the subject. By the former, I mean proof theory as the formal
study of mathematical practice, with an eye to illuminating aspects of
that practice; by the latter, I mean the more general mathematical study
of deductive systems and their properties. Of course, there is no sharp
line dividing the two, since foundational questions lead to mathematical
ones, which in turn influence our foundational views. But I do think one
can discern a difference in emphasis. In any event, I am personally
interested in the "traditional," foundational side.

On an informal level, we human beings harbor various and conflicting views
as to what mathematics is: e.g. mathematics is about abstract mathematical
objects, vs. mathematics is about calculation and construction; 
mathematics is to be valued because it is useful, vs. mathematics is to be
valued because it is an art, or esthetically pleasing; mathematics is an
objective science, vs. mathematics is a human creation; etc., etc. I don't
mean to imply that each of these dichotomies offers characterizations that
are mutually exclusive, but rather, different viewpoints. Mathematics is a
central human endeavor, and our informal understanding affects the ways we
do mathematics, the way we teach mathematics, and the kinds of mathematics
we deem worthy of support. 

In different ways, the philosophy of mathematics and mathematical logic
try to make our informal understanding explicit and precise. What I am
calling traditional proof theory studies idealized models of mathematical
activity, in the form of deductive systems, with that goal in mind. This
formal modeling helps us understand the basic concepts of mathematics, the
language, the basic assumptions, and rules of inference, the styles of
argument, the structure of various theories, and the relationships between
them. (Though, I would hasten to add, proof theory does not tell the whole
story!) The mathematical analysis of these deductive systems then enables
us to explore the relationship between abstract and concrete aspects of
the subject: mathematics is abstract, in that as it allows us to discuss
infinite sets and structures, but concrete, in that the rules governing
the discourse can be described explicitly. One then finds that these
explicit rules can often be mined for additional information.


2. How well has it met those aims?

I'd say quite well. We now have a wealth of formal systems that model
different aspects of mathematical practice, both classical and
constructive, in the languages of first-order or higher-order arithmetic,
set theory, type theory, explicit mathematics, etc., etc. We know a lot
about the relationships between the various systems, and their models. We
have a number of ways of understanding the "constructive" content of a
theory, in terms of their computational and combinatorial strength. Taking
these results all together provides a rich and satisfying account (though,
to repeat, not a complete account) of mathematical activity.


3. What developments or specific achievements stand out?

It would take me a long time to make up a good list, and then I'd worry
about what I'd left off. But I would start with the completeness and
incompleteness theorems, and the formal modeling of mathematics from Weyl
and Hilbert-Bernays to developments in Reverse Mathematics; and I would
include ordinal analysis, reductions of classical theories to constructive
ones, functional interpretations and the propositions-as-types
isomorphisms, combinatorial and other independences, and so on. All of
these provide illumination in the sense I have described above.


4. What, now, are the main open problems?

Perhaps the biggest difficulty is that (traditional) proof theorists face
is that the field is not driven by open problems. The aim is to find
characterizations and insights that are "illuminating," and it is hard to
know what further kinds of illumination one can hope for, until one finds
it. 

(Even the problem of "determining" the proof-theoretic ordinal of analysis
is not an open problem in the usual mathematical sense, since what is
required is a *natural characterization* of the ordinal, and there is no
precise specification of naturality. Notable exceptions to the statement
above occur in the context of proof complexity: e.g. questions as to the
provability of the pigeonhole principle in weak theories, or separating
Frege systems from extended Frege systems, seem to me to be important
mathematical open questions that are also of foundational interest.)

Here, however, are some general directions that I think should be pursued:

-- We should work towards better understanding of they way that strong
theories of analysis and set theory can have a bearing on the "concrete,"
say, regarding objects routinely encountered by algebraists and analysts,
or regarding Pi_2 (or even Pi_1!) statements of arithmetic.

-- We should work towards a constructive understanding of classical
mathematics that may, one day, be genuinely useful to computer scientists
-- that is, a general understanding of the way that abstract mathematical
knowledge can be represented and manipulated symbolically. 

-- We should work towards a better understanding of what can or cannot be
done with weak theories of mathematics -- elementary, feasible, etc., e.g.
regarding the extent to which real analysis can be carried out in feasible
theories, or regarding the kinds of combinatorial principles that can be
carried out in extremely weak theories.

-- We should work towards deeper and more realistic models of mathematical
proof, that go beyond the low-level "axioms + logical inference"
description. E.g. it would be nice to see attempts to explain what makes a
theorem natural, or a proof explanatory, etc. (This could be useful for
automated deduction, as well as for philosophical reasons.)


5. Are there any neglected directions in proof theory?

None that I can think of offhand; all the directions I just described are
actively being pursued, though the community is small, and there is plenty
of work to do. 


6. In what ways can or should proof theory relate to other parts of
logic/foundations/mathematics/computer science/linguistics/etc.?

If the goal is to understand what mathematics is, the more perspectives
one has, the better the picture. I would personally like to see lots of
interactions with all these areas, which provides a good way of grounding
the research.


7. Where do you think the subject is heading?
   Where do you think it should be heading?

See 4. 


8. Do you think more students/researchers should be involved in the
subject?  If so, how can they be encouraged to do so?

Absolutely. How to attract students? The usual ways: good research, good
teaching, good exposition, good textbooks, etc., etc.


9. Do we need more/different kinds of general expository texts?  What
about specialized texts?

As always, the more, the better. I am hoping to start work on an
introductory text this summer, using notes that I developed for a course
in Proof Theory that I taught last Spring.


10. Overall, how would you rate the state of health of our subject?  What
is its promise for the future?

At times, the field seems beleaguered -- for example, there are very few
American proof theorists of my generation. But at the core, I am
optimistic: the issues are profound, compelling, timely, and relevant, and
I expect that the field will always find its adherents and supporters.

Date: Thu, 16 Sep 1999 10:35:30 +0200 (MET DST)
From: Thierry Coquand 
To: sf@hypatia.stanford.edu
Subject: PT on the eve of Y2K



 Dear Sol Feferman,

 Sorry for answering so late to your interesting list of questions.
Rather than postponing indefinitely satisfactory answers,
here are first and rough suggestions.
 

                             Best regards,

                                 Thierry

-------------------------------------------------------

1. What are, or should be the aims of proof theory?

 One line of research is (generalised?) Hilbert's program:
to understand mathematical proofs from an intuitionistic
viewpoint. 

2. How well has it met those aims?

3. What developments or specific achievements stand out?

 Hilbert's tau/epsilon method.

 Gentzen's work.

 Development in the 60,70s: Spector's consistency proof,
realization that intuitionistic theory of functions is
weaker than its classical counterpart. Development of
predicative proof theory. Reduction of Pi11 to intuitionistic inductive
definitions, proofs that classical IDnu ~ intuitionistic IDnu.

 Formalisation of the notion of choice sequence (Kreisel-Troelstra).

 Bishop's realisation that a large part of mathematics can
be developped directly constructively (contradicting 
both Brouwer and Hilbert's opinion).

 Tait, Prawitz, Martin-Lof, Girard in the 70s, development
of natural deductions, notion of canonical proof. Curry-Howard isomorphism
between proof systems and functional systems.

 Since then?? Maybe reformulation of
Hilbert's program in Nelson's book ``predicative arithmetic'', 
independence results,  like PHP, in weak systems of arithmetic.

4. What, now, are the main open problems?

 Consistency of analysis
 P = NP 

5. Are there any neglected directions in proof theory?

 Connections with topos theory, boolean models. There are
parts of mathematics that try to give purely algebraic
version of results/proofs in analysis: algebraic geometry
for instance. This motivated topos theory, and the fact
that one has found connections with intuitionistic logic
is remarkable. There should be more connections with proof theory.

6. In what ways can or should proof theory relate to other parts of
logic/foundations/mathematics/computer science/linguistics/etc.?

 It should help in the development of proof systems
in computer science. Suggest also interesting experiments
we can do with formal proofs (computation of bounds, Goad's notion
of pruning,...)

 Otherwise connections complexity theory/weak systems of
arithmetic.

7. Where do you think the subject is heading?
   Where do you think it should be heading?

8. Do you think more students/researchers should be involved in the
subject?  If so, how can they be encouraged to do so?

9. Do we need more/different kinds of general expository texts?  What
about specialized texts?

 Expository texts: one text like Per Martin-Lof's book or one of
Lorenzen's book that present cut-elimination for omega-logic
in a constructive metatheory taking as primitive iterated inductive
definitions. (One paper by Tait on sequent calculus was like
this also). The development is then quite elegant, and does
not mention ordinal notations. Some more recent results may
be stated elegantly in this framework.

 It would be nice to have a presentation of the work of
Hilbert-Bernays-Ackermann-von Neumann. The 1924(?) paper of Ackermann
has not been translated in english. What was his formulation
of the tau/epsilon method?? What was his mistake? What was
von Neumann's correction?? Also, translation of Hilbert-Bernays
in english??

 The Stanford Report (beginning of 60s) should be also available:
what were the problems then? (I understand one goal was to give a model
of bar recursion using intuitionistic inductive definitions) What
has been achieved?? This is described too shortly in LNCS 897.

10. Overall, how would you rate the state of health of our subject?  What
is its promise for the future? 

 From what I can judge the quality of research is extremely
high.

Date: Thu, 16 Sep 1999 11:34:07 +0200 (MET DST)
From: Robert Staerk 
To: sf@hypatia.stanford.edu
Subject: Re: PT on the eve of Y2K

Here is my parital answer.

Remark: I am not a real proof theorist. I have learned some proof theory
from Gerhard Jaeger and I always tried to apply proof theoretic methods
to problems in Computer Science, e.g. completeness of semantics for
logic programs, adequate formal systems for functional programming, etc.


6. In what ways can or should proof theory relate to other parts of
logic/foundations/mathematics/computer science/linguistics/etc.?

For me it is important that proof theory has applications in Computer
Science. Possible applications are:

 - Formal systems for programming languages. 

   What is the analogon of "explicit mathematics" for
   object-oriented programming? What is the logic or object-oriented
   programming? In software engineering people are developing
   specification languages (e.g. UML "universal modeling language")
   and systems for software components (e.g. COM, Corba,
   JavaBeans). If you look closer at what happens, then you soon
   realize that something is missing: the glue that keeps everything
   together. How can we formally specify what a software component
   does? What are the assumptions under which it meets its
   specification? How can we be sure that a software component
   satisfies its specification? --- We need formal systems in which
   we can formalize everything.

   Methods applied in the past like `algebraic specification' were
   too much focused on a single method. That is the reason that they
   were not successful. We need universal methods which nevertheless
   have a solid foundation.

   Note, that programming has moved from `constructing executables'
   to `modeling the world' in the last decade. Proof theory should
   support this movement. Proof theorists know how to formalize the
   world. They should apply their knowledge.

 - Interactive theorem proving.

   I could never understand why some proof theorists are so strongly
   opposed to automated and interactive theorem proving. I agree
   that some projects like the QED project made too much propaganda
   in relation to the actual results they obtained. Other projects
   like Mizar, for example, made significant progress when they
   formalized the book "A compendium on continuous lattices". Why
   not apply formal systems in practice? It is good to know what the
   strength of a formal system is, but if nobody uses the formal
   system, then why is it so important? I think that proof
   theorists should support other people who believe in the formal
   method and try to show that formal methods are applicable.

   For example, proofs about programs could be re-used for software
   maintenance. Consider the Y2K problem. If we had a formal proof
   for the correctness of a program, a good tool could just point to
   the positions in a program where the assumption is used that we
   are in the year 19xx. This is an argument that even managers
   understand.

 - The logic of programs.

   This is still an open problem. Everybody feels that we should try
   to better understand the logic of programs. Old approaches, like
   Hoare's logic or dynamic logic were not so successful. Why? Maybe
   one should try to solve the problem from a proof-theoretic view
   point, e.g. what are adequate formal systems, what can be done in
   these systems, etc.

 - Proof carrying code.

   This is a recent topic of research. It is about computer
   security. If we run foreign code on our machine, we do not know
   whether the code is safe or not. Maybe it is a `virus' and
   destroys important data on our machine. How can we be sure that
   foreign code is safe?  One possibility is to attach to the code
   some kind of proof. This proof is checked on our machine by a
   proof checker before the foreign code is executed. In this way it 
   can be ensured that only certain segments of the memory are accessed
   by the foreign code and that the program counter stays within
   certain bounds. Questions that arise are now: What is the right
   format for the proofs? How can they be checked? How can they be
   generated by the compiler? By the user? How can proofs of
   high-level source code be transformed into proofs about
   executables? What kind of properties can be proved?


9. Do we need more/different kinds of general expository texts?  What
about specialized texts?

Yes, we need more introductory texts. I think the new methods
developed in the last 15 years should be applied to basic proof
theory, too, and presented to a wider audience. Several times I
have met other logicians who had completely wrong ideas about
proof theory.

10. Overall, how would you rate the state of health of our subject?  
What
is its promise for the future? 

The problem is that people of my generation (Ulrich Kohlenbach,
Andreas Weiermann, Ulrich Berger, Thomas Strahm, Michael Rathjen)
have problems to find permanent positions. Therefore I am a
pessimistic about the future of proof theory (at least here in
Europe).

-- Robert Staerk
--------------------------------------------------------
Robert F. Staerk                   (St\"ark, Stärk)
Theoretische Informatik             phone: +41 1 6327970
ETH Zentrum                           fax: +41 1 6321478
CH-8092 Zuerich   http://www.inf.ethz.ch/personal/staerk
--------------------------------------------------------

Date: Wed, 22 Sep 1999 17:56:59 -0700
From: Grigori Mints 
To: sf
Cc: mints@Turing.Stanford.EDU
Subject: PTY2K

Dear Sol,
here are at last my answers.
Grisha

1. What are, or should be the aims of proof theory?
The aim of PT is investigation of all mathematical aspects of
formalized proofs. 

2. How well has it met those aims?
It met this aim remarkably well, especially having in mind a blow
delivered by Godel's incompleteness theorem.

3. What developments or specific achievements stand out?
The most prominent specific achievements are related to extended
Hilbert-Gentzen program of analyzing the deductive and computational
strength of formal theories. More general developments include
applications to to computer science and philosophy. 

4. What, now, are the main open problems?
Determining the ordinals of subsystems of analysis beginning with
\Pi^1_2-CA and up, characterizing natural proof-theoretic ordinals,
termination of epsilon substitution method, characterization of
provably recursive functions of set theory, finding efficient
approach to proof-checking, P=NP.

5. Are there any neglected directions in proof theory?
Applications to specific  problems in mainstream mathematics.

6. In what ways can or should proof theory relate to other parts of
logic/foundations/mathematics/computer science/linguistics/etc.?
Difficult to tell in a few words

7. Where do you think the subject is heading?
   Where do you think it should be heading?
At least partially in the direction 5. above.
There is a major discrepancy between scientific side which is quite
satisfactory (cf. 2-4 above) and administrative side which is much
less satisfactory: the area of PT is contracting. Computer Science
which was a major consumer of PT experts and expertise follows the
general trend in Engineering to produce its own mathematics for
itself. 

8. Do you think more students/researchers should be involved in the
subject?
Yes, I do.
  If so, how can they be encouraged to do so?
I do not have new algorithms. Mathematicians were able to survive and
multiply, so should we. I am not sure appeal to CS and Philosophy will
be effective, but maybe we should try. 

9. Do we need more/different kinds of general expository texts?  What
about specialized texts?
Yes, we need all these, and the more the better, especially now when
publishing houses seem to be ready to publish everything written by
anybody commanding a minimum of prestige. 

10. Overall, how would you rate the state of health of our subject?  What
is its promise for the future? 
I am an optimist: such a beautiful thing will find applications
too. The health might be better, but the field has both old and young
guard, and the rest will take care of itself. 

Date: Fri, 24 Sep 1999 19:23:34 +0200 (MET DST)
From: Gianluigi Bellin 
To: Solomon Feferman 
Subject: Re: Proof Theory on the eve of Year 2000

Dear Sol, 

Thank you for having included myself in the list. 

..................................................................

Yours affectionate, 
Gianluigi 

========================================================================

> 1. What are, or should be the aims of proof theory?
> 5. Are there any neglected directions in proof theory?

The separation between "general" and "reductive" proof theory, as in the
Oslo volume 1971 (Prawitz's survey paper), institutionalizes a distinction
which in large part is historically motivated. In my view such a
separation has been detrimental to the subject as a whole. 

It is almost paradoxical that the informal notion of a proof does provide
a basic paradigm of scientific methodology, and yet the formal
representations of proofs in classical logic are so diverse that the
question of identity of proofs is still regarded as hopeless. 

In this respect, categorical logic has a real advantage in that the
identity of certain morphisms is axiomatically prescribed. Intuitionistic
and linear logic also benefit from having denotational and game-theoretic
semantics; these have not answered the questions about identity of
proofs, but certainly provide useful tools for such an investigation. 

Yet it must be possible to give an account in structural terms of the
connection between the notion of a well-order and the notion of a proof. 
There must be a way to use the insight of the classical school of proof
theory to give not only complexity measures of axiomatic theories through  
ordinal analysis, but also a criterion of identity of proofs for classical
systems. 

> 7. Where do you think the subject is heading?
>    Where do you think it should be heading?

Of course, research in set theory will go on and so the need will remain
of a proof-theoretic analysis and philosophical reflection on set-theory, 
which you, Pohlers, Rathjen, Buchholz and others have pursued, with clear
recent successes. Frankly, it is hard to imagine that there will be an
expansion of jobs in this area, as in pure set theory. 

On the other hand, in the applications to computer science the dominance
of type theory, categorical logic etc. seems evident, especially but not
only in Europe. I think this fact has to be accepted, because it is in
this intersection with computer science that most jobs will be. So, also
for this reason I see the need for a bridge between the traditions. 

> 9. Do we need more/different kinds of general expository texts?  What
> about specialized texts?

In addition to the topics I learnt in Stanford, students take a course in
complexity theory. They should learn more about typed lambda calculus (the
text of Krivine seems the best, also for its presentation of Girard's
system F), dependent types. They should be required to take also a course on
category theory, topos theory, such as the one you gave in 1989 --
clearly, the field of categorical logic has grown since then.
I speak for direct experience: that course gave me hope to be able to
understand this field sometimes and did help to establish positive
interactions with the colleagues at the LFCS-Edinburgh and elsewhere.) 

Date: Mon, 27 Sep 1999 11:19:22 +0200 (MET DST)
From: Andreas Weiermann 
To: sf@csli.Stanford.EDU
Cc: weierma@ESCHER.UNI-MUENSTER.DE
Subject: Re: Proof Theory on the eve of Year 2000

Dear Sol,

I have tried to write down some answers to 
your questions. I found it hard to give
appropriate answers and I did not always 
find one.

Best regards,
Andreas Weiermann.



> 
> 1. What are, or should be the aims of proof theory?

Proof theory should provide interesting classifications
of strengths of formalisms. This might be estalished by
assigning ordinals in a meaningful way to given concepts.

(Personally I am interested in topics which deal with
proof-theoretic ordinals like hierarchies and
questions on ordinal notation systems.)
> 
> 2. How well has it met those aims?

I have no satisfying answer to this question
but I think that it has met these aims quite well.
> 
> 3. What developments or specific achievements stand out?

The work of Arai and Rathjen on strong systems.

> 
> 4. What, now, are the main open problems?

The problem of natural well-orderings.
Since the analysis of Pi one two comprehension has been done
it seems worthwhile to provide (by the
inventors) a readable account of this.
> 
> 5. Are there any neglected directions in proof theory?

It would be nice if they would be some more nice applications
of proof theory to real pure mathematics.
> 
> 6. In what ways can or should proof theory relate to other parts of
> logic/foundations/mathematics/computer science/linguistics/etc.?

Proof-theoretic methods may prove useful to solve non trivial
problems in CS and elsewhere.
> 
> 7. Where do you think the subject is heading?
Mathematics and CS.
>    Where do you think it should be heading?
At least under mathematics.
> 
> 8. Do you think more students/researchers should be involved in the
> subject?  If so, how can they be encouraged to do so?
I have no good answer here. But I would say that more students/researchers
should be involved in the subject. A good and generally accepted research
program would be of interest here.

> 
> 9. Do we need more/different kinds of general expository texts?  What
> about specialized texts?

Some more specialized texts about so called folklore knowledge
would be of interest.
> 
> 10. Overall, how would you rate the state of health of our subject?  What
> is its promise for the future? 
> 
I have no good answer here. But I think that the subject is quite
healthy.

Date: Sun, 3 Oct 1999 15:07:43 +0200
From: Albert Visser 
To: Solomon Feferman 
Subject: Re: Proof Theory on the eve of Year 2000

Dear Sol,

Sorry for all the delay. I nearly finished my answer on Wednesday, but then ...

Best, Albert

------------------------------------------------------------------------------

Let me say first that I do not consider myself really a proof theorist. So
my evaluation
is pretty much a ---let's say medium informed--- outsiders'. (About some of
the isues I seem
to have only the fuzziest of opinions. On the other hand that gives you
some information too.)

>1. What are, or should be the aims of proof theory?

I don't think it can have or should have just one aim. Two aims that stand
out are
to give a sound classification of theories according to strength and the
other one is
to extract algorithms from proofs.

>2. How well has it met those aims?

I think it has met the first aim very well. The systematic project
to establish a connection between theories, ordinals, types and recursive
functions, stands out
as a great achievement. (I always felt that the precise classification e.g.
of a theory
like  {\sf PRA} (Parson's result) is just as interesting as results
concerning very strong
theories.)

Judging from Schwichtenberg's talk at the Troelstra conference
it is very well possible that algorithm extraction project is only now
coming of age. So here
we can perhaps expect the most interesting results in the near future.

>3. What developments or specific achievements stand out?

See my answer to 2.

What about all the work on substructural logics? That is clearly an
off-shoot of prooftheory.
I'm gradually becoming convinced (e.g. by the work of Abramski on game
theoretic
semantics) that there is something to it. I never found the applications to
linguistics of substructural
logics fully convincing, but perhaps it is already a big plus that there is
at least a program
aimed at applying the material.

I should also mention the development of type theory and the
foundation of mathematics by Per Martin-L\"of. These are at least
partly on the conto of prooftheory.

>4. What, now, are the main open problems?

I have no firm opinion here. Certainly the programme of algorithm
extraction should be pushed further.

(There are the important problems on proofchecking and proofgeneration: but
are they still proof theory?)

>5. Are there any neglected directions in proof theory?

There is a lot of work in prooftheory that I admire and that is slightly out of
the main stream, I guess it would deserve more attention.

i)   The work by Leivant showing completeness of IQC for interpretations in HA.
ii)  The work by Dyckhoff and Hudelmaier on efficient cut-elemination for
IPC and
     Pitts application of it to prove uniform interpolation.
iii) The work by Wolfgang Burr on the constructive arithmetical hierarchy.

(i)-(iii) all have something to do with understanding nested implications. The
work of Burr establises in a nearly definitive way the correct analogy of
the classical
hierarchy, a good example of absolutely basic progress.

iv) The recent estimates of Mints and Buss of how difficult it is to find
the witnesses/disjuncts
    promised in the existence/disjunction property.
v)  I always felt that it was a pity that Statman's work on alternative
measures of complexity of
    proofs died an early death.

Moreover there are problems on which proof theory is strangely silent. E.g.
the problem
of admissible rules. It is very surprising that all the work on admissible
rules is
model theoretical. E.g. Iemhoff's recent proof of the completeness of a
(non-standard) sequent system for the admissible rules of both IPC and HA
is by modeltheoretical means.
I think proof theorists should study these problems. (As far as I know
Leivant was the last one
who did anything in this direction.)

>6. In what ways can or should proof theory relate to other parts of
>logic/foundations/mathematics/computer science/linguistics/etc.?

It clearly *does* already relate to all these subjects.

logic: by being part of it

foundations: I feel that the idea of a prooftheoretical/typetheoretical
foundation
is a good one. (I never was really convinced, being a realist in the
philosophical
sense, however it is clear that we are dealing with a very coherent and
beautiful idea.)
It should be pursued further. What is lacking at the moment is a thorough
exposition
making the ML tradition accessible to philosophers.

mathematics: this will never become as central as we would like. I think
especially
extraction of algorithmic information from concrete proofs is an
interesting project.
(E.g. the work of Luckhardt.) Proof theory also can contribute to
proofchecking.
I do not know how much traditional prooftheory could
contribute to things like proof-assistants. It doesn't seem to provide a
good notion of
proofplan.

computer science: via type theory, correctness of algorithms and the like.

linguistics: I feel that the most important thing logic has to offer at the
moment
to linguists are the elementaria that mathmematicians and some computer
scientists
take for granted: what a good definition looks like, that one should verify
that a definition
does what one thinks it does, etc. It is clear that prooftheory is used in
logic oriented linguistics
viz. categorical grammar. Let's wait and see what this is going to do. I am
somewhat worried
about its lack of explanatory power.

>7. Where do you think the subject is heading?
>   Where do you think it should be heading?

I have to admit to the feeling that `high proof theory' concerned with
stronger and
stronger theories is in a degenerative phase. At least for a medium
informed outsider like me
it gives the impression more difficult but the same (i.o.w. somewhat boring).
So it would be good if there were some fresh ideas. I have no grand idea
about its future direction.

>8. Do you think more students/researchers should be involved in the
>subject?  If so, how can they be encouraged to do so?

A qualified no. See my answer to 7. It should expand only when one has some
good new ideas.

>9. Do we need more/different kinds of general expository texts?  What
>about specialized texts?

As I mentioned above ML's work is lacking a good exposition. `High proof
theory' has a number of
good expositions. Hudelmeier and Dyckhoff's work and Pitt's application of
it, deserve an exposition.

>10. Overall, how would you rate the state of health of our subject?  What
>is its promise for the future?

See my answer to 7.



############################################################
#  Albert Visser, Department of Philosophy                 #
#  Heidelberglaan 8, 3584CS Utrecht, The Netherlands       #
#  Phone: (0)30-2532173, (0)30-6350160, Fax: (0)30-2532816 #
############################################################

Date: Mon, 4 Oct 1999 16:20:03 +0200 (MET DST)
From: Ulrich Kohlenbach 
To: sf@csli.stanford.edu
Cc: Ulrich Kohlenbach 
Subject: Proof Theory on the eve of Year 2000

Dear Sol,

as a comparatively young researcher and reading the names of so many 
leading senior proof theorists in the heading of your mail I feel not quite 
comfortable to comment on your rather profound questions about the 
state of the art and the future of the whole subject of proof theory.     
However, as you repeatedly urged me to do so, here are some (sketchy) 
remarks to some of your questions. 

With best regards,

Ulrich



1. What are, or should be the aims of proof theory? 

I believe that any attempt to give an exhaustive definition of what proof 
theory is restricts the scope of this area and its applicability to
other fields in ways which are not be intended. 
So I will only sketch ONE particular type of questions studied
in proof theory which I have been interested in for several years and 
which can be summarized by the very general question: 
 
What is the status of the use of a certain principle P in a proof 
of a conclusion C relative to a deductive framework F? 

For example this covers conservation results ("P can be eliminated
from proofs of C in F+P"), reverse mathematics ("P is equivalent to C
relative to F"), but also many other interesting questions like: 
When can a non-constructive P be replaced by some constructive 
approximation ("constructive content of proofs of C in F+P")? 
When can an analytical principle P be replaced by an arithmetical one 
("arithmetical content of proofs")? 
What is the impact of the use of P on the computational complexity of 
a realization of C (e.g. if C is Pi-0-2, what is the contribution of 
P to the growth of provably recursive functions in F+P)?
Is there a speed-up of F+P over F for proofs of sentences C? 

The context F here can be e.g. a (weak) base systems, a certain 
logical framework (e.g. intuitionistic logic), but also structually 
restricted classes of proofs.         

Obviously, the questions just sketched are related to Kreisel's question
"What more do we know if we have proved a theorem by restricted means 
than if we merely know that it is true?" 

Of course, such questions can partly be also addressed using tools
from model theory instead. However, proof theory focuses on effective 
solutions, e.g. an explicit elimination procedure in case of a
conservation result etc. 

A more method-oriented answer to question 1) would be: 

Proof theory investigates proofs  

a) according to structural properties (normalization, cut-elimination
   etc.) 

and/or 

b) by proof interpretations (functional and realizability
   interpretations etc.)  

with the aim to obtain new information about proofs or classes of 
proofs (theories).

5. Are there any neglected directions in proof theory? 

In my view, proof theory notoriously lacks examples from mathematics, 
i.e. (classes of) actual mathematical proofs which illustrate  
proof theoretic phenomena and give rise to applications of proof
theory. Let me illustrate this by an example: conservation results 
for weak Koenig's lemma WKL have received quite some attention, e.g. 
in connection with reverse mathematics. However, very little focus has 
been given to the question whether there are any actual mathematical proofs 
which essentially use (in the normal mathematical sense) WKL but whose 
conclusions belong to a class of formulas for which WKL can be
eliminated (so that proof theoretically the use of WKL is not
essential). Up to my knowledge only Artin's solution of Hilbert's
17th problem as well as a whole class of uniqueness proofs in
analysis (Chebycheff approximation theory), which I studied some years 
ago, are known to be non-trivial instances of such WKL-conservation 
results and in both cases, proof-theoretic analysis turned out to be fruitful. 

I strongly believe that further such case studies would result in 
new proof theoretic techniques and insights and even new
foundationally relevant results (the case studies in approximation 
theory mentioned above incidentally yielded general meta-theorems 
of the form "non-constructive uniqueness yields effective existence" 
for a LOGICALLY rather special type of formulas which, however,
covers a large class of important uniqueness results in analysis. 
Counterexamples for slightly more general formulas show that it is 
important to focus on this logically special (but mathematically
broad) class of formulas extracted from the case studies). 
I my view, the success of model theory in giving interesting 
applications to mathematics is due to the restriction to logically 
very special but mathematically significant structure whereas proof 
theory focuses on general classes like ALL proofs in a certain system. 

Of course, applications to other areas are by no means the only 
(and probably not even the main) motivation for proof theoretic 
research but add to the more traditional foundational aims (see 
also the next question).  

6. In what ways can or should proof theory relate to other parts of 
   logic/foundations/mathematics/computer science/linguistics/etc.?

I believe that it is very important to stress that in addition to the 
well established uses of proof theory for foundational investigations, 
proof theory also can be applied as a tool: in computer science this 
has been proven already quite successfully. Applications to
mathematics are still rare but there is a potential here (see 
question 5). I think one should avoid to play out foundational 
aims against applications in mathematics/computer science and vice
versa. Both are important to secure proof theory a place in the
academic system.  


8. Do you think more students/researchers should be involved in the 
   subject? 

As I am excited about proof theory I am of course more than happy 
about every student who likes to get involved in the subject. 
However, the virtually non-existing job opportunities for logicians 
and in particular proof theorists make it currently quite problematic to
actively encourage students to do so.   

9. Do we need more/different kinds of general expository texts? What 
   about special texts? 

Yes, I think there could be more texts which are appealing to ordinary 
mathematicians and computer scientists (or at least to other
logicians) which introduce basic proof theoretic concepts using actual 
proofs in mathematics as examples. For instance, a general treatment 
of "interpretative" proof theory (Herbrand's theorem, 
no-counterexample interpretation, realizability, functional 
interpretations, ...) based on applications of these techniques to 
specific proofs thereby discussing their respective merits and
possible uses would be very useful.   

10. Overall, how would you rate the state of health of our subject? 
What is its promise for the future? 

Overall, I think that proof theory has been extremely successful in 
its applications to foundational questions and also has become an 
important applied tool in computer science. The links to ordinary 
`core' mathematics are, however relatively weak, which constitutes a great 
danger for the survival of proof theory in mathematics departments. 
The scientific standard and the level of critical reflexion about 
motivations, aims and intellectual relevance are usually very 
high (sometimes coming close to being self-destructive). 
The dissemination of the achievements of proof theory to a broader
community of logicians, mathematicians and computer scientists has 
not yet been equally successful.

Date: Tue, 5 Oct 1999 14:20:24 +0200 (MET DST)
From: Wilfried Buchholz 
To: sf@csli.stanford.edu
Subject: Re: P.T. on the eve of Y2K

Dear Sol,
 
Below you find some raw thoughts on your PTY2K questions.

Best,
Wilfried

I think the state of PT as a whole is sound, but w.r.t. the
ordinal analysis of Pi^1_2-CA (and other strong systems) the
situation is still somewhat awkward and unsatisfying.
It seems that a major open problem has been solved (independently
by Rathjen and Arai) but only very few people are interested in it,
and even fewer are willing to study this work.
So, one thing which should be done is a kind of consolidation of the
Rathjen/Arai work. More researches should be involved in that subject.
As you already pointed out 2 years ago, even if the ordinal analysis of
Pi^1_2-CA would technically be well understood, the question would remain
"what have we gained by this?" At moment the only answer I can give is the 
following: we have a "concrete" term order $\prec$ which characterizes
the arithmetic part of Pi^1_2-CA; the value of and interest on this 
characterization depends on the complexity (in an informal sense) of $\prec$.
By further investigations it should be possible to replace $\prec$ by
simpler and simpler orderings. Perhaps in far future one will be able
to describe the ordinal of Pi^1_2-CA by a term order whose definition
takes only three or four lines and can be intuitively grasped. 

Another completely different point which should be tackled is 
what Girard calls the lack of modularity in proof theory 
(cf.  Girard, Proof Theory, pg.15ff). I think that to some extent
this is connected with the lack of a proof theory textbook which
over a long period would be accepted as the standard source of the field,
like e.g. Chang-Keisler, Model Theory; Jech, Set Theory;
Shoenfield, Mathematical Logic; Barwise, Admissible Sets and Structures.

Date: Thu, 7 Oct 1999 09:54:43 +0200 (MET DST)
From: Helmut Schwichtenberg 
To: sf@csli.stanford.edu
Subject: Re: Proof Theory on the eve of Year 2000

Dear Sol,

sorry for being late in reacting to your enquiry.  Rather than
following your questionaire, I would like to communicate an aspect of
proof theory that I come to find particularly promising for the
future.  In an abstract to my course `Classical Proofs and Programs'
for the Summerschool `Foundations of Secure Computation' in
Marktoberdorf 1999, I wrote the following (this is also quoted in the
historical note by Friedrich L. Bauer, entitled `Intuitionismus und
Informatik', in Informatik-Spektrum 1999, pp.284--287, of which I
will mail you a copy)

  It is well known that it is undecidable in general whether a given
  program meets its specification.  In contrast, it can be checked
  easily by a machine whether a formal proof is correct, and from a
  constructive proof one can automatically extract a corresponding
  program, which by its very construction is correct as well.  This --
  at least in principle -- opens a way to produce correct software,
  e.g. for safety-critical applications.  Moreover, programs obtained
  from proofs are `commented' in a rather extreme sense.  Therefore it
  is easy to maintain them, and also to adapt them to particular
  situations.


Best regards,
Helmut

Date: Thu, 07 Oct 1999 18:38:58 +0200 (MET DST)
From: Thomas Strahm 
To: sf@csli.Stanford.EDU
Subject: Re: PT on the eve of Y2K



Dear Sol

Attached you find some very small answers to some of the
questions on "PT on the eve of Y2K".

Best wishes,   

Thomas

__________________________________________________________________________

4. What, now, are the main open problems?
5. Are there any neglected directions in proof theory?

   It is hard to mention specific main open problems. But what seems
very important to me are all attempts which aim at a unifying view 
of various methods and concepts which are relevant in proof theory 
today. This applies to the more technical aspects of proof theory 
as well as to more general notions such as for example "constructivity" 
or "predicativity", which are used in increasingly divergent ways
these days.
   In addition, I hope that further work on the conceptual and technical 
side of proof theory will help to reduce the syntactic and combinatorial
complexity of some of its parts. I think this is absolutely essential
for making proof theory accessible to a wider community.


6. In what ways can or should proof theory relate to other parts of
logic/foundations/mathematics/computer science/linguistics/etc.?

   The value of proof theory for the foundations of mathematics
is uncontested. But I am convinced that proof theory and proof-theoretic 
methods in general do also shed new light on various problems in 
computer science. A good example in this respect (among many others) 
are the extensive investigations in weak systems of arithmetic and 
propositional proof systems, which do illuminate numerous aspects 
of complexity theory even if so far they have not solved the main 
open problems in that subject.


8. Do you think more students/researchers should be involved in the
subject?  If so, how can they be encouraged to do so?

   Certainly it would be desirable to attract more people from
other subjects to work in proof theory and apply proof theory
to their own fields. This would make the community of proof
theorist more lively and bring new ideas from other subjects
into our field. In order to involve more people, of course it
is crucial to have available as many general (and also specialized)
texts as possible (see next question).   


9. Do we need more/different kinds of general expository texts?  What
about specialized texts?

   Of course we have excellent texts on the subject available. But maybe,
in order to attract people from other fields, it is important to
have more high quality texts of a very general/popular nature, which
are accessible to *every* mathematician/computer scientist/philospher etc.
A short text like "What is proof theory?" which is similar in spirit to
J.N. Crossley's "What is mathematical logic?" (Oxford Univ.Press, 1972)
would certainly be very useful. Of course a text like this can never
give a complete picture of the field, but maybe it would help to
make outsiders curious to learn more about proof theory.
   As to specialized texts, I believe that texts which focus on general
*methods* in proof theory are very important. Everybody working in
the field knows that the same methods are applied over and over
again in order to give a proof-theoretic analysis of a huge variety of
formal systems. For example, the general method of asymmetric 
interpretation is useful in bounded arithmetic but also in the
context of impredicative systems. Hence, it would be desirable to
have more texts which are devoted to these methods rather than the
analysis of single formal systems (which of course has to be used
in order to exemplify the general method). In this respect, some
of the articles in the new Handbook of Proof Theory are very useful
and up to the point.

Date: Thu, 7 Oct 1999 18:43:23 +0200 (MET DST)
From: Lev Beklemishev 
To: sf@csli.stanford.edu
Subject: Questionnaire

Dear Professor Feferman,

Here are the answers to your questions.

> 1. What are, or should be the aims of proof theory?

I would not specufy particular "aims" in the sense of concrete
goals to be achieved. Rather, I would define the subject as broadly
as possible, e.g., as the study of the notion of proof and proof systems
in all possible variants and aspects. (These systems need not
always relate to conventional ones. I would also predict that
in the future the variety of *kinds* of proofs we deal with 
will noticeably increase. )

I think that it is important not to draw any fixed borders
of our subject, and to be ready to expand the current areas of
interests of proof-theorists. (Compare, for example,
with the evolution of the meaning of the subject "geometry"
from Euclides through Klein to the contemporary mathematics.)

> 2. How well has it met those aims?
> 3. What developments or specific achievements stand out?

I think proof theory is a wonderful and deep subject.
Memorable developments that come to my mind (just the first
few, without much thinking):
0) Formalization of logic and mathematical reasoning;
1) Goedel's incompleteness theorems;
2) The discovery of structural proof-formats: sequent calculus,
resolution, ...
3) The discovery of epsilon_0 and the role of proof-theoretic 
ordinals;
4) The analysis of predicativity;
5) Isolation of meaningful parts of analysis and set theory 
and their reductions;
6) Extraction of effective bounds from proofs;
etc.

> 4. What, now, are the main open problems?

a) I think that the most important problem is to find new
meaningful applications and connections of proof theory with the other
logic-related areas. It is not a technical
mathematical question, but it is a problem for proof-theorists
in the sense that they should actively look for such
applications. Under the applications of proof theory I do not  
necessarily mean the "practical" applications in areas such as AI or CS. 
It is also important to establish new connections with the 
other branches of logic and mathematics.

[One recent application of the type I have in mind
was a discovered (by Razborov, Pudlak, Krajicek 
et. al.) connection between some natural problems in bounded 
arithmetic, effective Craig interpolation theorems in propositional 
logic, and cryptographic conjectures. This was motivated by a
proof-theoretical question of independence of P=NP from bounded
arithmetic theories.]

b) A good idea would be to collect and publish and/or put on a
web a classified list of technical open problems in proof theory.
(Such lists do exist, for example, in group theory.)
This could, in particular, stimulate fresh researchers 
and students and help us to set the next goals.

> 6. In what ways can or should proof theory relate to other parts of
> logic/foundations/mathematics/computer science/linguistics/etc.?

At present the situation appears to be
not fully satisfactory
(and not only for proof theory, but for logic as a whole).
I think that the kinds of applications one can expect from proof
theory are not so much the particular theorems, but rather
the background "culture": proof theory can provide appropriate
language, basic tools (like cut-elimination), proper ways of
formulating problems. 

> 8. Do you think more students/researchers should be involved in the
> subject?

Yes, we need more students and I think there is a need
in the popularization of proof-theory.

> If so, how can they be encouraged to do so?

At the moment this is difficult for objective reasons (not only
because of the lack of textbooks): the area
appears perhaps too self-oriented, and too technical.
In other words, the students generally do not see the benefits of
learning proof theory. I have even heard the qualified logicians 
express the opinion that they do not understand what 
proof-theorists are doing.

The only way of curing this disease is to 
put some effort in clarifying the basics and specific problems of
proof theory on the one hand and to come up with
new promising problems and directions of research on the other. 

> 9. Do we need more/different kinds of general expository texts? What
> about specialized texts?

I think the best texts on proof theory, so far, are
in the handbooks. In particular, I find the recent handbook 
on proof theory an excellent source.

The situation with the textbooks is less satisfactory.
We certainly need well-balanced
textbooks accessible for a beginner and/or an outsider.

> 10. Overall, how would you rate the state of health of our subject?
> What is its promise for the future?

As that of a generally healthy man, who somewhat neglected 
to monitor his health lately. But there is no reason to panic:-)


With best regards,
Lev

Date: Mon, 11 Oct 1999 19:30:53 +0200
From: Gerhard Jaeger 
To: sf@csli.stanford.edu

Dear Sol,

Below I will try to answer some of your questions although I feel that
sometimes I just repeat the obvious.

Warmly, Gerhard

---------------------------------------------------------------------

3. What developments or specific achievements stand out?

4. What, now, are the main open problems?

There are the standard well-known open problems which I do not have to repeat.
For me personally there are some interesting directions, but I would not
dare to call them the main open problems of proof theory.

(a) I think that a better and deeper understanding of nonmonoton inductive
    definitions and of higher order inductive definitions would be very
    desirable. There are some interesting recursion-theoretic results, but
    a proof-theoretic approach seems necessary.

(b) I also think that the area of feasible functionals of higher types could
    be very interesting for proof theory.

(c) Sometimes I also get the impression that computational logic(s) could
    profit from proof theory. There are interesting connections between
    proving and computing, but, especially in the context of nonclassical
    and temporal logics, more should be possible.

5. Are there any neglected directions in proof theory?

I do not know whether this is a neglected direction, but a further conceptual
consolidation of what has been achieved so far could be useful. There are,
for example, many notions of "constructive", we have predicative, predicatively
reducible, (metapredicative) and impredicative systems. Apart form
"predicative", they are all used in an informal way. I think that more
conceptual clarity would be good.

I know that I am a sinner in this repect myself since I introduced the
notion "metapredicative" without being able to give an exact definition.
However, I did it with the purpose of dealing with an interesting area between
the predicative and impredicative.

6. In what ways can or should proof theory relate to other parts of
logic/foundations/mathematics/computer science/linguistics/etc.?

I am very interested in the relationship between proof theory and the
foundations of mathematics and computer science. The connections to computer
science are also very useful for our students, after all for finding a job.

7. Where do you think the subject is heading?
   Where do you think it should be heading?

I see a certain danger that the field falls apart in several areas and
becomes technically so difficult that it is very hard for newcomers to
reach the borders of research. There are certainly important results whose
proofs have been studied in detail by very few people only. Maybe it has to
happen this way. However, if there is a change to make our field more
accessible, then it should be done.

8. Do you think more students/researchers should be involved in the
subject?  If so, how can they be encouraged to do so?

I think that proof theory is a very attractive field of research which makes
use of a variety of methods and concepts so that more students/researchers
would be very welcome. I also think that they have very good chances to find
interesting positions, for example in industry, especially if there are some
relationships in their work to computer science. Thes situation is more
complicated (at least in Europe) for Postdocs since there are only very few
tenure positions for proof theory at universities.

9. Do we need more/different kinds of general expository texts?  What
about specialized texts?

There are very good general expository and specialized texts. But as the field
developes more will be necessary. Very introductory and motivating texts, for
example for computer science students, could also help. 

10. Overall, how would you rate the state of health of our subject?  What
is its promise for the future?

I hope and think that the health of our subject, at least compared with other
subjects, is quite good. I am optimistic concerning the future provided that
there is place left at the universities to do basic research.

Date: Sun, 17 Oct 1999 19:24:59 +0100 (BST)
From: M Rathjen 
To: sf@Turing.Stanford.EDU, M Rathjen 
Subject: Y2K

Dear Sol,

here are some remarks regarding proof theory on the eve of Y2K.

Proof theory has become a vast area. Ordinal analysis of strong theories,
linear logic and game semantics, bounded arithmetic, automated theorem proving
are just a few branches which don't have much in common perhaps except for cut 
elimination.
I'm only going to say something about proof theory in the narrow sense,
leaving it to the specialists of the other branches to state their aims.

The contributions and achievements of ordinal analyses I've tried to describe
in my paper "The realm of ordinal analysis"  (I've send you a copy; it's also
down loadable from my webpage
http://www.amsta.leeds.ac.uk/Pure/staff/rathjen/preprints.html ).
I roughly grouped them into 4 groups: 

(1) Consistency of subsystems of classical second order logic and set theories
relative to constructive ones

(2) Reductions of theories formulated as conservation theorems

(3) Combinatorial independence results

(4) Classifications of provable functions

Good examples for (1) are redutions of Delta^1_2-CA+BI and KPM to Martin-L"of
type theories. A good example for (2) is the Extended Kruskal Theorem (EKT) 
which Friedman destilled from the ordinal representation system for 
(Pi^1_1-CA)_0 and which played a pivotal role in Robertson's and Seymours 
proof of the graph minor
theorem (the latter was hailed in the book by Diestel  "Graph theory" as he
most important result in graph theory since the four colour theorem). Since the
graph minor theorem implies  EKT and EKT implies the well foundedness of 
the ordinal representation system for (Pi^1_1-CA)_0, the graph minor theorem is
independent of (Pi^1_1-CA)_0.

There are  still many interesting questions relating to  ordinal analyses and
ordinal representation systems, e.g. the relationship between the Sigma_1
definable ordinals of a set theory T and the ordinal representation system
used in the ordinal analysis of T, the relationship between Carlson's
ordinal representation systems base on patterns of resemblance and the more
traditional ones based on collapsing functions, and many more.

As to the long term goals of ordinal analyses, however, I think that it has 
reached a problematic stage. Does it make  much sense to go further and tackle
ever stronger theories?  Devising an ordinal representation system and 
employing
it for the analysis of a strong theory can be a great challenge and very
difficult to achieve but I don't consider that a goal in itself. 
Ordinal analyses of Pi^1_2-CA and beyond have left me with bureaucratic
nightmares, something I truly dislike.  As yet I don't see any applications; 
though some efforts have been made. To use these results for constructive
consistency proofs constructvism would have to be developed further. Anton 
Setzer has extended ML type theory and has carried out well-ordering proofs 
in them; a very cumbersome undertaking. I doubt that his papers on that will 
ever find more than 3 readers.  One could also try to use these strong 
representation systems to
devise new combinatorial principles. The problem here is that we know no 
mathematical results that require the strength of Pi^1_2-CA. This would be
completely new territory. Also Friedmans machinery for turning indiscernibles
into finite combinatorial statements seems more appealing.
The upshot is that I hesitate to continue working on ordinal analyses. I'm 
doing other work now and will definitely need a longer break from OA.

If a student/researcher would ask me whether he should get involved in OA I'd
always point out the hazards for his career.


As ever

Michael 

Date: Tue, 19 Oct 1999 23:17:04 +0200
From: Wolfram Pohlers 
To: Solomon Feferman 
Cc: Wolfram Pohlers ,
     pohlers@math.uni-muenster.de
Subject: Re: Reminder 

Dear Sol,

sorry for the delay of my answer. I came back to Muenster two weeks 
ago and (although it is hard to believe) found hardly time to study my
e-mail, let alone to answer it. 

Here are my very personal answers to some of your questions.

Proof theory has become a quite heterogenous field. As I see it there
are two main domains:

I. Basic (or perhaps better Structural) Proof Theory
II. Pure (Mathematical) Proof Theory

I. The domain of structural proof theory comprises the study of formal
proof figures including the study of non classical logics and
manipulations on proof figures. (In some sense it meets Kreisel's idea
of a "theory of proofs"). Via the Curry - Howard isomorphism there is
a close connection to typed lambda calculi including
polymorphism. Structural proof theory seems to have applications in
computer science. Extraction of programs from proofs may serve as an
example for possible applications. Another example is automated
theorem proving. 

I think that there are many aims in structural proof theory; finding
proof systems which are easy to implement; studying the various types
of non classical logics such as modal logics, linear logics
etc. 

Personally am I am not so much attracted by structural proof theory so
I do not really know its main open problems. My impression is that
there are no "main problems" but a series of open problems of
comparable weight. 

Structural proof theory seems to be a lively and flourishing
subject. E.g. many contributions in "Theoretical Computer Science" may
be regarded as contributions to structural proof theory. In many
aspects it seems to have met many of its aims. Still there is a wide
area of solvable open problems.

I hope that the revised second edition of Schwichtenberg--Troelstra
will become a standard textbook for structural proof theory. 

A problem which is somehow on the borderline between structural and
mathematical proof theory (probably more belonging to mathematical
proof theory) is the N=NP problem. Though not genuinely
proof theoretical it is not completely unlikely that an answer to this
problem can be given by proof theoretical means.


II. My view of Mathematical Proof Theory is influenced by my personal
believe in the existence of "the mathematical universe". (This believe
I probably inherited from Sch"utte.) I know that our 
mathematical means do not allow us to explore the mathematical
universe as a whole.  Therefore the main directions of
attack -- in my opinion are: 
- developing new means, i.e. designing new axiom systems, new
   rules, finding new principles, (here I would subsume your explicit
   mathematics, Per's theory of types, constructive set theory but
   also the introduction of higher infinity axiom systems which is
   commonly counted among set theory)
- comparing them, judging their reliability,(here I would subsume
   reductive  proof theory, constructive interpretation of prima facie 
   impredicative axiom systems, perhaps also some parts of reverse
   mathematics)
and 
- determining their limits (ordinal analysis, comparison of the
    "consistency strength of higher infinity axioms). A determination of
    the limits of an axiom system should also give some answer to the
    question "what more do we know when can prove a theorem in an analyzed 
    axiom system?". Considering also this question has taught us that
    there are different degrees of analyses. Here I think on the
    differences in determining the $\Pi_1^1$-ordinal, the
    $\Pi_2^0$-ordinal or even the $\Pi_n^0$-ordinal for $n\geq 1$ in
    the sense of Lev Bekelemishev's most recent results.




My interest in determining the strength of axiom systems is not
motivated or even limited by their mathematical impact. The fact that
reverse mathematics has shown that "ordinary mathematics" can be
developed in quite modest axiom systems is no reason to neglect
stronger systems.  On the contrary, the analysis of stronger system
has shown us many phenomena which were invisible in the analysis of
weaker systems and turned out to be also meaningful for weak systems
(I think on Weierman's applications of collapsing methods to Peano
Arithmetic and G"odel's theory T). Therefore one of the main aims of
Mathematical Proof Theory should be the ordinal analysis of system
stronger than $\Pi_1_2$ comprehension. Not just to know the ordinal or
a well--ordering which is sufficient for a consistency proof but to see
how strong set existence axioms are unraveled during the analysis. I
think that proof theory has met this challenge quite well in the
past. The development during the years in which I was watching this
field is overwhelming. (Though for me it is still a pity that I cannot really
understand Arai's work which comprises the analysis of very strong
systems. ) Today we understand many things much better than in the
past.  

However, it becomes more and more difficult to involve students and
young researchers in this subject. The reason is the increasing amount
of pre-knowledge which is needed for this type of research. At the
present point we cannot even rely on a well-developed abstract
recursion theory. Therefore the thesis on which one of my doctoral
student (M.  M"ollerfeld) is working resembles much more a paper in
generalized recursion theory than a paper in proof theory. On the
other hand it is one of the beauties of the area that it brings
together different parts of mathematical logic. I am also quite
confident that we can develop the tools for the analysis of pretty
strong theories.

Of course it is much easier to work in structural proof theory which
requires only a limited amount of reading before you can start with
own research (and potentially offers better perspectives for an
academic career because it is considered to be closer to computer
science). Though I still have students working in this area I can
observe that the number of researchers around the world working in
this field diminishes. I see the danger of getting below a critical
mass which could be fatal for the subject.

One remedy I can see is a better presentation of the field. I think
that we need more expository texts which present proof theory from
different angels non concealing the other viewpoints. I believe that
there is even a (modest) market for such texts. (My believe relies on
the fact that -- according to Springer -- my Lecture Note sold very
well). Of course there is also a need for a broad and detailed
presentation of the state of the art. Here I see a personal
challenge. 


Best regards

Wolfram. 

Date: Thu, 28 Oct 1999 08:57:02 +0000
From: Peter Aczel 
To: Solomon Feferman 
Subject: Re: Responses

Dear Sol,

Your latest email has has spurred me to send you the following partial
response to your initial request.  In fact I wrote it immediately
after reading your first email, but was hoping to try to answer more of
your questions beforehand after thinking more about the questions.  I
seem to have had difficulty in bringing my second thoughts to a
conclusion.

I only attempt to answer question 1.  I do not consider myself to be a
`professional' proof theorist, so I have found difficulty in trying to
answer the other questions.  You may want to go straight to my
conclusion.

Best wishes,

Peter

1a) What is Proof Theory?

Proof Theory has its origins in Hilbert's metamathematics, a tool in
Hilbert's program for the foundations of mathematics.  It is a branch
of mathematics, which has relevence for work on `Foundations' - a
field that I consider to be not a branch of mathematics in the usual
sense.

Proof Theory is concerned with the investigation of formal systems; i.e.

a) consistency proofs,

b) structural properties of notions of formal proof for formal
systems; e.g. cut elimination and normalisation,

c) reduction relationships between formal systems,

d) ordinal notations and their use in measuring the `logical strength'
of formal systems,

1b) What should the aims of Proof Theory be?

As a branch of mathematics it has generated its own body of theory and
open problems.  Of course one of the aims is simply to develop the
theories further and solve the open problems, which will generate new
open problems.  I do not feel particularly competent to discuss such
aims and I consider them to be secondary aims.

But I think that the primary originating aim is to produce tools and
results for the work on `Foundations' that has developed out of
Hilbert's program.

Of course there are also other aims concerning the applications of
Proof Theory to other disciplines inside and outside mathematics,
which should not be ignored, but in this first aproximation to a
formulation of aims I will ignore.

Hilbert's program:

Finitist mathematics provides a concrete meaning to the primitive
recursive functions as totally defined functions on the natural
numbers and gives a concrete meaning to Pi_0^1 sentences.  Hilbert
believed that all such sentences that can be proved to be true can in
principle be proved to be true by finitistic means.  In particular the
consistency statements for the standard formal systems, T, for
infinitistic mathematics should be proved using only finitistic
means.  Once that has been done then any Pi_0^1 sentence proved to be
true in such a formal system T will be provable by finitistic means.
In this way the use of the `ideal' formulae of T would be justified.

Godel's demolition of Hilbert's program:

Not all true Pi_0^1 sentences can be proved by finitistic means.  In
particular consistency sentences for theories T cannot be proved
finitistically, or even infinitistically by methods representable in
T, but only by stronger methods.

Conclusion: 

Hilbert's idea of finitistic mathematics is still valid and important.
It captures a fundamental central core of mathematics, once one
accepts the idealisation where the feasibility of computations is
ignored.  Given this idealisation I think that there is universal
agreement about the meaning of Pi_0^1 sentences.  Where there can be
disagreement is concerning which of them are true - in particular
which consistency sentences are true.  Some will have stronger beliefs
than others; i.e. believing more Pi_0^1 sentences.  These beliefs will
arise out of a variety of belief systems, generally involving infinite
objects.  It can be dificult to objectively compare and evaluate
different belief systems.  Attempting to do so soon becomes a
philosophical and rather subjective activity.

Godel's incompleteness results show that we cannot get away from the
consideration of belief systems for mathematics.  Mathematics cannot
be encapsulated once and for all in a single belief system - there is
always the possibility of a stronger belief system.

Hilbert's metamathematics provides an alternative approach to the
philosophical one to comparing belief systems for mathematics: capture
the ideas of each belief system in a formal system and study and
compare the formal systems and in particular their consistency
sentences either using finitist methods or else perhaps using stronger
methods that one believes in.

Proof Theory should provide the tools to do this!

Date: Tue,  2 Nov 1999 14:14:53 -0500 (EST)
From: Wilfried Sieg 
To: Solomon Feferman 
Subject: Re: Proof Theory on the eve of Year 2000

Dear Sol:

I am sorry for not responding earlier to your "gentle reminder".  

.................................................................

There is certainly another reason, namely, the inherent difficulty of
your questions. Let me address them a bit indirectly and briefly.  For
me, there are three deeply interconnected aspects of proof theoretic
work:


(1) Building appropriate formal frameworks for (parts of) mathematical
practice and thus, to some extent, also for thoroughly mathematized
parts of the sciences. 

(2)  Investigating these frameworks metamathematically and using the
results in (philosophically motivated) foundational investigations.

(3) Employing proof theoretic techniques for particular purposes, for
example, in mathematics, computer science, or cognitive science.


These aspects point also to the directions of proof theoretic work along
which the subject has made most significant contributions, to logic in
general and philosophy of mathematics in particular.  Unfortunately,
many contributions are still not generally seen as having been provided
by "proof theory"!  This is true especially for the philosophical work -
that is wrapt in the shroud of "formalism".

The deep interaction of set theoretic considerations and proof theoretic
investigations of fragments of ZF is, perhaps, one of the most
remarkable developments.  However, that development has not yet been
analyzed from a thoroughly philosophical perspective.

What I find missing (or see only in its infancy) is a "structure theory"
of mathematical proofs, connected with strategies for constructing (or
searching for) proofs. Here, proof theory, cognitive science, and
computer science intersect; here is also the greatest potential for
important applications in a broad social context. I am thinking, in
particular, of pedagogical, but also "business" applications.

The subject has a great future; that's in any event my prejudiced
belief.  It offers exciting opportunities for all kinds of folks (from
the philosophically to the economically minded).  Better general
expository texts would be most helpful to spread the word.

Warm regards,

Wilfried

Date: Tue, 16 Nov 1999 11:33:42 -0800 (PST)
From: Solomon Feferman 
To: Solomon Feferman 
Subject: PT on the eve of Y2K

	A natural reaction to the original ten questions I posed is to
ask, why send out such a survey at all?  Is reading it going to affect
what anyone is doing?  Doesn't the field just self-propel in all its
different directions without having to think about where we're heading?  I
understand such doubts and don't have a convincing answer.  But I think
that all along proof theory has been more introspective than most other
fields of research, and that has to do with its origins in Hilbert's
program and the necessary steady retreat that has been made from that.  We
can point to a remarkable record of accomplishment, but in many cases we
have difficulty in saying to the outside world what the nature of that
accomplishment is.  I think of this as a search for our authentic
identity, and that some exercises like this in self-assessment can help us
find that.    

	To turn now to the questions themselves, like several other
respondents I have found it easier to deal with the questions more or less
as a whole rather than one by one, though of course taking them as a point
of departure.  In doing so, I mainly want to concentrate on open
problems/neglected areas, which are relevant to all the questions.

	Conceived of most broadly, proof theory should aim to study proofs
in the widest sense possible to make it a subject for systematic
metamathematical treatment.  Mathematical proofs are the richest and most
closely examined source of material for such a study, and it is natural to
give greatest prominence to them.  In a catholic view of proof theory one
should not be so confined, and I do so only because that's what I know the
best.  Even with this restriction, it is not clear that our theory of
proofs does justice to the subject matter.  I take it for granted that
there seems to be no way that various properties of proofs of interest to
mathematicians--such as being intelligible, beautiful, clever, novel,
surprising, etc.--can be part of a systematic metamathematical study.
Relatedly, I don't expect our theory could explain what makes one proof
*more* intelligible, beautiful, etc. than another.  On the other hand,
there is a basic relation between proofs, of interest to mathematicians,
which we would expect to be accounted for in our theory and which is not,
namely their identity: 

(Q1) When are two proofs (essentially) the same?  

It's a bit of a scandal that we have no convincing theoretical criterion
for that.  
	Let's step back for a moment.  Granted that we have to take an
idealized model of proofs for a metamathematical study, in what sense and
to what extent can we support the thesis that every proof can be
formalized?  Of course we know that the issue of the problematic role of
diagrammatic and other heuristic arguments in geometric proofs goes back
to ancient times, but they seemed to be essential for discovery and
communication.  Officially, they can be dispensed with, but in practice
they can't.  Coming up to the present day, one leading mathematician has
told me that there are proofs in topology which can't be formalized,
because they involve elements of visualization in some essential way.  And
some logicians in recent years, such as Barwise and Etchemendy, have been
investigating what they call heterogeneous reasoning, e.g. proofs that are
manipulated on computer screens that involve diagrammatic and iconic
elements in some significant way.  It's not clear to me if they are making
the case that these are non-formalizable in anything like the usual sense.
So this leads to the following question:

(Q2) Can all mathematical proofs be formalized?

An answer to this question would require something like Church's Thesis:

(Q3) What is the most general concept of formal proof?

The common view is that the notion of formal proof is relative to the
concept of formal axiomatic system.  But mathematical proofs don't wear
their underlying assumptions (*axioms*) on their sleeves, and the usual
process of representing proofs formally does so only with reference to
more or less standard background systems.  Is there a sense in which
proofs can be considered in isolation, or must they always be referenced
to a background system?  Supposing one had an answer to (Q3).  Then one
could hope to engage in case studies of challenges to a positive answer to
(Q2).  But I think it would be profitable to pursue such case studies even
without an answer to (Q3).
	Here's a related matter that I find puzzling.  It's common
experience that the standard sort of formal representation of informal
statements captures their structure and content quite well, and that there
is little uncertainty about how to pass back and forth by hand between the
informal and formal statements.  Students take to this readily, and we can
quickly and convincingly identify errors in mis-representation for them.
Note that none of this seems to require prior determination of a
background formal language in which these are to be represented.
Moreover, once such a language has been specified, it is easy to check
mechanically whether a proposed formal representation of a statement is
indeed well-formed according to the language.  
[An aside: it's my impression that there is no generally accepted standard
representation of natural language statements at large.  What is it about
mathematical statements that makes them special in this respect?]  
But now, when we come to proofs, there is no generally agreed upon
standard representation, and for the various kinds of representations
(e.g. Frege-Hilbert style, Gentzen-Prawitz natural deduction style,
Gentzen sequent style, etc.) which have been developed for proof theory,
there is no immediate passage from the informal proof to its formal
representation (or even vice-versa) and no generally accepted means of
checking such proofs for well-formedness (*correctness*) mechanically, let
alone by hand.  The proof theory that evolved from Hilbert's program
didn't concern itself with such questions.  Rather, once one was convinced
that a given body of proofs can be represented in principle in a certain
way, the only concern was whether a contradiction might be derivable from
such a body of proofs.  

(Q4) Why isn't there an easier transition from informal but in-principle
formalizable proofs to actually formalized, mechanically checkable,
proofs?  

Even if one has doubts, as I do, about the value of having proofs checked
mechanically (because, it seems to me, if you can be clear enough about a
proof to set it up for checking, you can already convince yourself of its
correctness), there should be value in analyzing what's needed to deal
with (Q4), since the conceptual problems that will need to be handled
along the way are of independent interest.  Perhaps we've been trying to
do much in one go--from informal proof to proof on the machine--and
instead one should break it up in a series of steps as has been done for
the transition from informal algorithms to their implementations.
	All of the preceding belongs, I guess, to structural proof theory,
a subject which has certainly flourished in recent years through the study
of substructural logics, especially linear logic and its kin.  Being
completely out of that area, I'm in no position to assess its current
state of health and prospects, though the fact that there continues to be
high activity is evidence that both are good.  Another area of
considerable recent development is the application of notions of
complexity to propositional proof systems, which likewise seems to be
being pursued energetically, which is all to the good.  Since some of the
basic general problems of complexity theory such as P = ? NP are
equivalent to statements about such systems, there is evidently hope that
the answer will come through an application of proof-theoretical methods.
Time will tell; I'm optimistic that the problem itself will be settled
within the next decade, and then we can see what method(s) were the
successful ones.  
Of course, it would be a feather in the cap of proof-theory if the answer
came from our community rather than, say, the computer science community
or the finite-model theory field.  

	I turn now to the part of proof theory with which I am most
familiar, and which concerns formal systems for various parts of
mathematics, ranging from fragments of arithmetic through number theory
and analysis up to systems of set theory, with way stations in algebra
along the way.  The main directions in this are the *reductive* line of
development stemming from Hilbert's program, and what I've called the
*extractive* line emphasized by Kreisel, but of course stemming from a
variety of sources (characterization of the provably recursive functions,
Kleene realizability, Godel functional interpretation, etc.) .  The
reductive line has really split into two related lines, that for lack of
better descriptions I will call here the *strength* line, dominated by the
project of ordinal analysis as well as other measures of strength, and the
*interrelation* line concerned with relations of interpretation, (partial)
conservation, etc., between formal systems.  Looking at the developments
in this part of our subject over the last 50 years, I think the progress
we have made is remarkable, and we can truly speak of having mapped out a
substantial proof-theoretical landscape, under steady expansion.
Moreover, the proof-theorists following these lines of work have a great
variety of tools at their disposal and interesting questions of
comparative methodology have emerged.  Regrettably, the achievements that
have been made have been insufficiently appreciated by logicians working
in other areas, let alone by the wider mathematical public.  I think one
of the reasons for this is the welter of formal systems that have been
studied, and it is here that some introductory texts for general
consumption could serve a useful purpose.  They might concentrate on some
few principal, *typical* systems for examples and then explain how and why
one is led to consider refinements (e.g. via restrictions of
comprehension, choice and/or induction principles).  By comparison, the
promoters of reverse mathematics have been able to reach a wider audience
by fixing on their five or six systems that every reasonably literate
person can understand, even if the reasons for fixing on those particular
systems are not prima-facie compelling in themselves.  Of course, every
interesting subject has its welter of examples and data (viz., degree
theory or large cardinal theory) but the entry to such other subjects is
not prohibitive.  If students are to be encouraged to pursue these lines
of proof theory, and I think they should, more expository work will be
needed to bring out the main features of the proof-theoretical landscape.  
	Now for some questions, beginning with the extractive line.  The
very familiar but still basic question asked by Kreisel is:

(Q5) What more than its truth do we know of a statement when it has been
proved by restricted means?

It is hard to know how this might be answered in such generality.  In
special cases, for example Pi-0-2 statements or Pi-1-1 statements, we can
say something, such as that we have somehow characterized the associated
provably recursive function or the associated ordinal (of unsecured
sequences), resp.  And for Sigma-0-1 statements we would like to say that
a witness can be extracted from a proof.  But none of these kinds of
answers is responsive to:

(Q6) What more than its truth do we know of a Pi-0-1 statement when it has
been proved by restricted means?  

This could be considered a question for the reductive line, where
consistency statements are to be established by restricted means, e.g. by
quantifier-free transfinite induction on a *natural* well-ordering; but
what does the least ordinal of such an ordering tell us about the
statement?  Perhaps (as suggested to me by Peter Aczel) something simpler
can be said, namely as to where these statements sit in their ordering by
implication (over some weak system).  Note that one can cook up
incomparable consistency statements, so the order is not linear.  Perhaps
there are even natural examples of this sort, given by consistency
statements canonically associated with finitely presented (not necessarily
finitely axiomatized) formal systems, and that leads us to:  

(Q7) What is the ordering relation between canonical consistency
statements?

Large-cardinal theorists point to the fact of the *well-ordering* of the
consistency statements associated with large cardinals, the motivations
for which came from all sorts of different directions, as evidence of some
inner harmony among them (and perhaps for their justification).  But
that's just an empirical fact about one class of consistency statements.
It would be remarkable if that were true of canonical consistency
statements in general.
	To get back on the extractive track, one slogan that has motivated
work in this area is that if one can prove a Pi-0-2 statement
constructively (and, indirectly, even classically) then one can extract a
program from the proof.  And that accomplishes a double purpose of
providing one with a proof of correctness.  So far as I know, no new
programs of interest have been obtained in this way.  In general, if some
procedure is proved to exist by usual mathematical reasoning, the
associated function is not feasibly computable.  For example, it is
trivial to prove constructively that any list can be sorted (relative to a
given ordering of its items).  But completely separate algorithmic
analyses have been necessary to find optimal sorting procedures.  That
shifts the burden to the computer scientist.  One could try to get around
this by restricting to fragments of arithmetic (or associated fragments of
analysis) whose provably recursive functions are feasible in principle.
But I think even in these cases, one would not come out with optimal
solutions.  To be sure, there is a value in developing systematic
procedures for extracting such programs even if they don't give optimal
solutions, and even if they are for already known problems.  What I would
hope to see, though, is an answer to:

(Q8) Can we extract previously unknown constructive information such as
in-principle algorithms or bounds from constructive or classical proofs?

Once one has such information, one could then subject the situation to ad
hoc non-proof-theoretical analysis to see to what extent the information
can be optimized.  Relatedly, one would hope to obtain more applications
of proof theory to mathematics.  I researched the literature on this for
my article in the *Kreiseliana* volume, and found that the existing
applications are few and far between, despite the high hopes (and a
certain amount of hype) that originally pushed the *unwinding* program.
What is needed is a sustained effort and the development of general
methods like those which led to many mathematical applications of model
theory, especially to algebra.

(Q9) Can proof-theoretical methods be applied to obtain results of clear
mathematical interest comparable to those obtained by model-theory?  

	Let's come finally to the reductive direction of work.  Here a
basic problem is that the line of development from the Hilbert program has
become so attenuated that one can no longer say in any clear-cut way what
is accomplished.  The leading work in that direction is that of Arai and
Rathjen on the subsystem of analysis based on Pi-1-2 comprehension. The
Gentzen-Schuette-Takeuti aim was to prove consistency by constructive
means.  However, if the means employed are so complicated--as they are in
the cited work--one cannot assert that one's confidence in the consistency
of this system is at all increased thereby.  Setting aside the putative
value of demonstrating consistency, one could try to see if some reduction
to a prima facie constructive system results from that work, in the form
of the interrelation line that I suggested in my article on Hilbert's
program relativized.  As far as I know, no such system is on offer.  The
other aim that has been pursued was to give up foundational goals in favor
of technical results, namely to give an ordinal analysis of the system in
question.  But we have no criterion for what constitutes an ordinal
analysis in general, in terms of which we can see what the cited work
achieves.  I am in the process of preparing a paper, *Does reductive proof
theory have a viable rationale?*, which goes further into these matters.
I don't currently have an answer to the question raised in that title and
which include the work of Arai and Rathjen, but I hope strongly that an
answer will emerge that preserves the philosophical significance of
reductive proof theory.  At any rate, to be specific:  

(Q10) What has the proof-theoretical work on Pi-1-2 comprehension
accomplished?  At the very least, how can the work be made more
understandable?

My belief is that this will require some new concepts, whether what is
accomplished is foundational or is simply an ordinal analysis.  In the
latter case, it comes back to the old question:

(Q11) What is a natural system of ordinal representation?

Finally, the ordinal analysis program leads us to questions of
methodology.  As it has been carried out in its most extensive
development, this has required the employment of concepts from higher
recursion theory and, through that, of higher set theory, involving large
cardinal notions, their admissible analogues and their formal use in
ordinal representation systems.  The phenomenon is even more widespread,
and there must be a good, unifying reason as to why it works as well as it
does:

(Q12) What explains the success of large cardinal analogues in admissible
set theory, explicit mathematics, constructive set theory, constructive
type theory, and ordinal representation systems?  

In very recent years another method has emerged at the hands of Jaeger and
his co-workers to deal with impredicative systems such as ID_1 and beyond,
that uses only techniques from predicative proof theory (namely, partial
cut-elimination and asymmetric interpretation).  

(Q13) What explains the success of metapredicative methods?  What is their
limit, if any? Does metapredicativity have foundational significance?

It may be that metapredicativity stands to locally predicative methods
(used for prevailing ordinal analysis) as the use of ordinal
representation systems built via transfinite types over the countable
ordinals stands to those built over higher number classes.  
	Still another interesting approach to ordinal analysis is the use
of model-theoretic methods recently published by Avigad and Sommer.  This
has worked successfully on a variety of predicative systems but it is not
clear yet if it can break into impredicative territory.  If it should be
able to compete successfully with ordinal analysis at higher levels, that
in my view would constitute the final detachment from the
Gentzen-Schuette-Takeuti line, and then ordinal analysis would have to
stand on its own as a contribution to the strength line.  
	To conclude, I have to admit that my feeling about the
foundationally reductive line of proof theory had been rather one of
discouragement, and that we may be at a dead end, or at least at a loss
where to go from here.  But, instead, thinking further about the ten
questions I had posed and reading the many useful responses I received has
made me feel *very* encouraged about the current state and future of our
subject as a whole.  The further questions I have raised here are my ideas
of general directions in which I think it would be profitable for proof
theory to move in the coming years.  Other workers in the field have in
some cases quite different ideas, in other cases ideas that overlap or
complement the above.  If one thought that all the interesting questions
had already been answered or could be answered without any essentially new
ideas, we would be in a bad state.  I'm convinced just the opposite is
true.  The fact that there are so many good questions and such good people
in the field to deal with them ensures its continuing vitality into the
next century.  
To be sure, seeing the way through for a foundationally and technically
informative proof theory of strong subsystems of analysis will be a great
challenge, but if the past is any predictor, we can be confident that
people will rise to that challenge.  I thus look forward with great
optimism to the developments in the coming years.  

Date: Tue, 25 Jan 2000
From: Jan von Plato


1. What are, or should be the aims of proof theory?

   Proof theory studies the general structure of mathematical proofs. 
The aim is to find concepts and results by which that structure 
can be mastered in various branches of mathematics.

   A precise representation of mathematical proofs as formal(izable) 
derivations is sought. Then questions about derivability (consistency, 
independence of axioms, conservativity problems, etc) can receive 
precise answers.

   One aim of proof theory is to find representations of mathematical 
proving that actually help in finding proofs. For example, a Hilbert-
style axiomatic representation of classical propositional logic is 
hopeless in this respect, whereas a sequent system with invertible 
rules makes the task automatic.

   I consider Martin-Lof's constructive type theory to belong to proof 
theory. So one aim of proof theory is the same as that of type-
theoretical proof editors: formal checking of correctness, in 
practical terms, program verification.


2. How well has it met these aims?

   Proof theory, largely speaking, has failed in achieving its aims. 
Gentzen's work was perfect in pure logic, the predicate calculus. 
Intuitionistic natural deduction and classical sequent calculus are 
by now mastered, but the extension of this mastery beyond pure logic 
has been modest. There is some development of proof theory of 
arithmetic but on the whole, proof theory is not a useful tool for 
the practising mathematician. 

   Proof theory would need a second Gentzen who comes with some new 
ideas about the structure of proofs in arithmetic, then says:"If you 
want to prove this and this kind of theorem (say Goldbach), then do 
this and this kind of thing." And people do it and find the proofs! 
It seems paradoxical to have ridiculously simple statements in 
arithmetic with no structured idea on how to prove them.


3. What developments or specific achievements stand out?

   The more recent success story, for me, begins when Martin-Lof extended 
the Curry-Howard isomorphism from implication to full intuitionistic 
natural deduction. (Witness Howard himself, see the remark added in -79 
to his -69 paper.) "The first really new idea since Frege invented the 
topic," as someone said.

   The sequent calculi that do not have any structural rules, the 
G3-calculi, are a gem of logic I would compare to creations such as 
the quantum-mechanical formalism. From Gentzen to Ketonen (who did 
the classical propositional part) to Kleene, Dragalin and Troelstra, 
each added some pieces until the building was finished. The last ten 
years have brought some applications of this powerful tool of 
structural proof analysis and more is in the coming. A pity one 
does not even learn of the existence of these "contraction-free" 
calculi from the recent Handbook of Proof Theory.

4. What, now are the main open problems?

   To repair the situation signalled in 2, by extending the achievements 
in the structural proof analysis of logic to mathematics. 

   The most important specific open problem of proof theory is to find 
a normalizing system of rules of natural deduction for the full 
language of classical predicate calculus, or to show that no such 
system of rules is possible. At present, we do not have the rules 
of classical natural deduction, just a fragment without disjunction 
and existence. Natural deduction for full classical propositional 
logic, with normalizing derivations throughout, exists but its idea, 
a rule of excluded middle as a generalization of indirect proof, 
does not extend to the quantifiers.

   If the problem about classical natural deduction is solved, a 
comprehensive answer can be given to: What is the computational 
content of a classical first-order proof?


5. Are there any neglected directions in proof theory?

Proof theorists, having failed in analysing proofs in mathematics, 
went on to apply their skills (somewhat opportunistically in my mind) 
in logical systems different from the two canonical ones, 
intuitionistic and classical. So I am saying that there are *overly* 
cultivated areas when other things could have been done, though I also 
find that this has led to systems with dozens of rules and with less 
understanding of what it all means. In these studies, a very formalistic 
stand has been taken on, say, Gentzen's structural rules. People treat 
them as if they were something in themselves, then try to find formal 
semantical interpretations to their systems. So I find there is neglect 
in method. Gentzen never meant weakening, contraction, exchange to have 
a "meaning" as such, he even called them later "structural modifications" 
in contrast to logical rules and said they are needed only because of some
special features of his sequent calculus. 


6. In what ways can or should proof theory relate to other parts of 
logic/foundations/mathematics/computer science/linguistics/etc?

   Logic & foundations: Proof theory is what logic and foundations are 
for me, by and large. (Maybe I could add some algebraic semantics 
but that is more mathematics than logic.) 

   Mathematics: Proof theory should win its place as a tool for 
the mathematician.

   Computer science: Formalized proofs=verified programs in computer science.

   Linguistics: Aarne Ranta's book Type-Theoretical Grammar (Oxford 1994) 
is the foremost application to linguistics.


7. Where do you think the subject is heading?
   Where do you think it should be heading?

   Structural proof theory is making steady though not expansive progress, 
with results accessible to anyone who wants to learn them. Ordinal 
proof theory seemss a bit like set theory, a never-ending search and study 
of ever stronger things.

   I find that proof theory should remain non-esoteric, which has
not been the case in so many parts of logic. The basic building blocks 
should be simple. The difficulties should come from the enormity of the 
combinatorial possibilities of putting them together. One has a great feeling 
of real discovery when the maze of all possible proof trees suddenly 
starts obeying your command. First you try and try, but there is always 
some little gap that destroys your theorem. Then you locate  the essential 
property and induction on the complexity of derivations goes through 
without too many problems. *Afterwards* others will tell you: that was 
easy (and you try to be patient about them).


8. Do you think more students/researchers should be involved in 
the subject? If so, how can they be encouraged to do so?

   Logic is dominated by other things than proof theory, a look at the 
logic journals shows this. I predict a change, through the relevance 
of computational proof theory for computer science. There are also
institutional changes: Mathematics departments are becoming smaller
through pressure created on universities by the needs of computer 
science. Such changes will contribute to the change of emphasis in 
logic, too and maybe there will be place for more researchers. 

   As to engaging students, every student of mathematics should in my
opinion have some idea of the general principles of mathematical
proof. Now they know perhaps some truth tables and that mathematical
truths are empty "tautologies", fashionable slogans from the 1920's. If
instead they had heard that the truth of a theorem is established by proof
and that knowing a proof is the possession of a mathematical construction,
some such students would by natural inclination be drawn into proof
theory. 
 
   Proof theory will be rewarding for the new things that can be done, 
where many other parts of logic are becoming untractable monsters. 
It will be rewarding for its applications and for the job a student 
can get in conputer science related industry. The latter has certainly 
happened with my (few) students. 

9. Do we need more/different kinds of general expository texts? 
What about specialized texts?

   Having just written one text of the former kind, "Structural Proof
Theory", co-authored by Sara Negri and to be published towards the end of 
2000 by Cambridge, the answer is a definite "Yes"! The book has an
interactive sequent calculus theorem prover implemented in Haskell and
donloadable from the web. 

  As to specialized texts, an exposition of Martin-Lof's type theory 
covering all things would be first on my list. An accessible 
presentation of the proof theory of arithmetic, but not suffocated 
by an abuncance of "subsystems," just one or two systems, unbounded, is 
on my list of books I would like to see appear.


10. Overall, how would you rate the state of health of our subject? 
    What is its promise for the future?

   Health is measured by estimating the average ratio of: 
degree of novelty divided by degree of complexity. The higher this
measure is in new work in a field, the better. More seriously, as 
long as a direction of research yields new simple things it is alive. 
The contrary starts happening when new things become complicated or 
the simple things repeat what was known already.

   Structural proof theory is in a healthy state. Congresses in recent 
years (the LC nm's) have been encouraging for me. 

   For the future, I foresee a time when proof theory is not one of 
the four canonical parts (or five with the addition of "philosophical 
logic") of logic conferences, but one out of two. 

Date: Tue, 25 Jan 2000 11:12:43 +0100
From: Alessandra Carbone 
To: carbone@ihes.fr, sf@csli.Stanford.EDU
Subject: Re: questions&answers (fwd)

Dear Prof. Feferman,

thanks for the invitation to contribute my view to your list. I looked at 
your questions and found the diversity of the responses very interesting. 
I feel that for a long time there were not sufficiently many new insights in 
proof theory and its relations to the rest of mathematics. 
It is difficult to get out of a way of thinking that one is used to.
Finding new paths require fresh ideas, which as I envisage, will emerge in 
the field in coming years.
 
Mathematicians show more interest to proof theory than logicians usually 
expect from them. For example, I attended a meeting this summer in Israel, 
Vision 2000 - whose list of partecipants you probably know - and during 
the meeting, the topics of automated deduction and 
computed-aided proofs were coming up in the discussion. Mathematicians were 
asking themselves many questions, often naively, in these directions 
and they never turned for help to proof theorists.

"what is a proof?" 

"what are the criteria to accept a construction (maybe a computer analysis) as 
a proof?" (see for instance,  Osterl\'e's talk in the Bourbaki Seminars (June 99) 
on the computer-aided proof of the Kepler packing problem by Hales and Ferguson.
"On the basis of what can we accept Hales and Ferguson's proof?" 
"Could we formulate general criteria?" (is this a part of proof theory?))

"can we go beyond a sequential construction of proofs, in the spirit of 
k-categories?"

"can high-dimensional geometric/combinatorial constructions generate 
fast deductions and bring proofs closer to geometric thinking?"

these are just few basic questions that come to mind. 

How to isolate "real proofs" (modelled by those that we find in mathematics) 
in the huge space of all possible proofs? what is the structure in the space 
of proofs which allows a mathematician to navigate in this huge space
and arrive at a desired proof? we hardly hope to resolve this mystery 
too soon and we will be happy with something much simpler than this.

Here are somewhat disorganised thoughts inspired by
Jan von Plato's response concerning structural proof theory.

I do not believe that by looking at invertible sequent calculus rules (for instance) 
we can answer anything about the way mathematicians do proofs. 
I do think though that structural analysis of systems 
that we know can help to understand better the limits of our methods. 
The work done in Linear Logic much contributed to understanding 
these limits. I would like to stress here, following Girard, 
that proofs are not trees! Proofs harbour by far more structure that 
can be seen within the logical language used to construct them.
This might be related to the fact that the language is linear but 
the mathematical thinking is not at all. We never find a mathematical proof 
in a linear way and it seems to me non adequate sticking to
deduction systems based on sequentiality. It would be better to admit it 
in order to find new ways.

We need to accept structural rules. Afterall mathematicians use them 
all the time. the basic principle of contraction is used everywhere in
mathematics. things glue together and the complexity of the objects 
that one studies decreases. 
we should be happy for this, since at least we are able to prove
something! (without it, proofs would be unconfortably large.) 
We should systematically study the rules of "gluing". it is not an 
easy task and mathematicians have done it much before us!

I think that it is important and instructive to think of formal systems 
of deduction without forgetting their complexity. I believe that 
the structure of the proofs reflects their complexity and there is a lot
of evidence about it. fundamental principles are yet to be discovered
but they are there and wait to be found.

Even in terms of propositional logic we do not know what is going on 
in terms of computational expressivity. What sort of computational 
power is hidden behind propositional logic? the whole spread of complexities 
lying between polynomial and exponential is there and we do not know 
much about it. 

I am afraid that proof theorists have little contact with mathematicians
and they are not sufficiently aware of how mathematicians generate 
their proofs. I think that proof theory, 
which from my point of view should speak of mathematical proofs (and i include 
proofs made by a computer), needs this interaction. It needs an effort for 
changing the language. This is not an easy task but i believe it is necessary 
if we want to see the field to get into a new direction.
This holds especially for books and expository papers. 


Best regards to everyone,

Alessandra

Responses and Comments