By Solomon Feferman
An index of respondents with links to their answers is to be found below.
On Sept. 3, 1999, I wrote a group of workers in proof theory and neighboring subjects, asking ten questions assessing the present state and future of proof theory. Here is the original message, and that is followed by the responses, in the order received. Personal material (other than greetings) has been removed. Authors of the responses are indexed below. In the case of comments or exchanges (in some cases by those who have already written) the name is starred with a number; these follow the direct responses to the questions. ------------------------------------------------------------------------- Dear colleagues, I have been invited to give the opening lecture at the colloquium in memory of Kurt Schuette, scheduled in Munich on Nov. 5, 1999. (The meeting will be joint with a Workshop "Proof and Computation" on Nov.5-6.) Besides planning to talk about what Prof. Schuette meant to our subject and to me personally, it seemed to me that this would be an appropriate opportunity to take measure of where we are and where we might be going. I will be giving some thought to this in the coming two months. In the meantime, I thought it might be useful, both for this particular purpose, and for the subject as a whole, to get your assessment of the state and future of proof theory. I would thus welcome your answers to any or all of the following questions which came to my mind in this respect. I expect a great diversity of opinion, and won't begin to try to represent it all in my talk. But I think it will be interesting to see whether significant areas of unanimity emerge as well as areas where we have essential differences. Please feel free to deal with any further questions that you think are appropriate, as well as pass on these questions to anyone else whose views ought to be solicited, including those who don't use e-mail. I would hope that all of you would like to see the responses as they come in, but if you prefer not to be included in that way, let me know immediately, so I can forestall that. Sol Feferman ........................................................................... 1. What are, or should be the aims of proof theory? 2. How well has it met those aims? 3. What developments or specific achievements stand out? 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.? 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?
Date: Fri, 3 Sep 1999 18:14:06 +0200 From: Anton SetzerTo: 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 BeesonTo: 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 TakeutiTo: 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 BussTo: 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 TennantTo: 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 FefermanSubject: 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 TupailoTo: 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 AvigadTo: 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 CoquandTo: 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 StaerkTo: 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 MintsTo: 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 BellinTo: 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 WeiermannTo: 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 VisserTo: 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 KohlenbachTo: 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 BuchholzTo: 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 SchwichtenbergTo: 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 StrahmTo: 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 BeklemishevTo: 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 JaegerTo: 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 RathjenTo: 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 PohlersTo: 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 AczelTo: 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 SiegTo: 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 FefermanTo: 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 CarboneTo: 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
Date: Mon, 22 Nov 1999 08:59:19 +0100 (MET) From: Anne TroelstraTo: pohlers@math.uni-muenster.de Cc: sf@csli.stanford.edu Subject: prooftheory dear Wolfram, Your answerss to Sol's queries prompt me to make a remark on terminology. I split prooftheory in structural interpretational Structural proof theory relies on the analysis of the properties of deductions in suitable formalisms; interpretational uses sysntactical translations such as realizability, Dialectica etc. I count what you call "mathematical" prooftheory also as structural, more specifically a highly developed, specialized branch of it. The terminology "basic" in my book with Helmut is really an indication of level: it discusses basis techniques for first-order logic and gives applications to very different logics, so it is rather broad than deep; there is also the "basic" result of your mathematical prooftheory, namely for first-order arithmetic. Perhaps we can agree on a somewhat standardaized designation of the various branches of proof theory. Best wishes, Anne -- A. S. Troelstra Faculteit WINS, Plantage Muidergracht 24, 1018 TV AMSTERDAM-NL phone 020-525.5298
Date: Tue, 23 Nov 1999 12:28:09 +0100 From: Wolfram PohlersTo: Anne Troelstra Cc: pohlers@math.uni-muenster.de, sf@csli.stanford.edu, pohlers@math.uni-muenster.de Subject: Re: prooftheory Dear Anne, thanks for your comment on my (very personal) view of proof theory which is now public in the net. I agree that we need some standardization in naming the different branches of proof theory. My motivation to separate it into "structural" and "mathematical" proof theory was the following. "Structural" proof theory should deal with the structural properties of proof figures, their normalization etc. The aim of "mathematical" proof theory I see in the investigation of infinite mathematical structures, especially the structure of natural numbers and sets/functions/types ... on them and the universe of sets. Here proof theory should take care of possible axiomatizations for these structures. Compare different axiomatizations (even using different logics), determine their proof power (in any sense) and finding constructive justifications for them. (Here I would subsume the work of the Muenchen- Muenster school.) Since proof theory has become so heterogeneous during the last two decades I saw a necessity to distinct at two main areas. However, I am not at all ideological about names. I can live with any name. Of course I would be curious to know your point of view. Warm regards Wolfram
Date: Tue, 23 Nov 1999 13:32:44 +0100 (MET) From: Anne TroelstraTo: sf@csli.stanford.edu Subject: copy correspondence, continued Quoting Wolfram Pohlers, > > Dear Anne, > > thanks for your comment on my (very personal) view of proof theory > which is now public in the net. I agree that we need some > standardization in naming the different branches of proof theory. My > motivation to separate it into "structural" and "mathematical" proof > theory was the following. > > "Structural" proof theory should deal with the structural properties > of proof figures, their normalization etc. > > The aim of "mathematical" proof theory I see in the investigation of > infinite mathematical structures, especially the structure of natural > numbers and sets/functions/types ... on them and the universe of sets. > Here proof theory should take care of possible axiomatizations for > these structures. Compare different axiomatizations (even using > different logics), determine their proof power (in any sense) and finding > constructive justifications for them. (Here I would subsume the work of > the Muenchen-Muenster school.) > > Since proof theory has become so heterogeneous during the last two > decades I saw a necessity to distinct at two main areas. However, I > am not at all ideological about names. I can live with any name. Of > course I would be curious to know your point of view. > > Warm regards > > Wolfram > It occurred to me even before your answer, that you were making a distinction along the lines of subject matter, whereas I had been thinking along the lines of methods. The structural proof theory of first-order predicate logic becomes highly non-trivial in the area of complexity theory of propositional logic, another highly specialised area, just as "mathematical proof theory" in your sense. Systems falling under mathematical proof theory have also been studied by interpretational methods, so my remark that "mathematical proof theory" was a special branch of structural proof theory is not quite correct, though I think it is probably in the main correct for the Schuette school (Buchholz, Pohlers,...) I am quite happy to go along with any reasonable terminology, provided it is sufficiently descriptive, which helps me to remember which is which, in talking about it. Who is going to make a proposal? warm regards, Anne -- A. S. Troelstra Faculteit WINS, Plantage Muidergracht 24, 1018 TV AMSTERDAM-NL phone 020-525.5298