## Abstract

Returning to old ideas of Kreisel, I discuss how the mathematics of proof theory, often combined with tricks of the trade, can occasionally be useful in extracting hidden information from informal proofs in various areas of mathematics.

## 1. Notions of proof, prior to proof theory

### (a) Proofs in mathematics

I take the basic subject matter of these Proceedings to be mathematical proofs, as presented in the style traditional for the last two hundred years, i.e. in books or journals, in a variety of languages (usually natural languages with extra formalism specific to mathematics). Mathematical knowledge is communicated and certified between specialists using such proofs. There are other less formal methods of demonstration, in conversations or seminars, and there are surely situations, say in low-dimensional topology, where one might use various gestures to communicate the basic idea (and this would suffice for experts).

Proofs in this sense presuppose earlier proofs, and a proof is supported by a complex scaffolding, some of it erected thousands of years ago. Progress in the subject depends not only on the emergence of proofs of new results, or new proofs of old results, but also on artistry in the structuring of proofs. Proofs have to be learned, remembered at least in broad outline and later fruitfully combined with other proofs and ideas, to go further. Many remarks at the meeting had to do with the issues of visualizability and memorability, and it was clear that these are central issues for mathematicians, but much less so for computer scientists right now.

### (b) Proofs of novel complexity

We are talking here of traditional, informal proofs. Several talks from this Discussion Meeting (notably those of Aschbacher (2005) and MacPherson) bear on specific contemporary proofs of novel complexity. At issue is the reliability of such proofs. This is not the first time in the history of mathematics that such concerns have been prominent, but I do not think that we face anything that deserves to be called a crisis. It seems to me likely that we will see in the near future other proofs of the kind described by McPherson, and that we will simply become accustomed to them. Aschbacher predicts that we will see before long other classifications with the complexity of that for finite simple groups.

In some cases there is a component of computer assistance, without which one would not have a proof at all. In such cases, generally, there is a trace of dissatisfaction in the mathematical community at the presence of the large-scale computational component, and a hope that another proof will be found free of such components. As McPherson reports, the mathematical editors of Annals of Mathematics were unable to convince themselves of the correctness of the computer component of Hales' proof, and delegated the responsibility for checking that component to the computer science community. One hopes that this kind of situation will not become the norm. After all, in principle there seems no great purely mathematical difficulty in proving the correctness of the algorithms used by Hales. Presumably the problem is rather that the algorithms are not presented in a mathematically perspicuous way. Given a clear presentation, can these correctness proofs be more than simple inductive proofs? It may be that the anxiety comes rather from fear of dependence on correctness of hardware. There are presumably quite general methods for establishing probabilities of failure of devices of this kind, not at all specific to computers assisting mathematical activity. For example, depending on one's point of view, one may fear more such failure in a military or transportation situation than in a mathematical proof. Some of us may even fear a systematic failure in our own hardware.

Another situation, discussed at this meeting, concerns the classification theory of finite simple groups, where it has not been unreasonable to doubt that there has been a complete proof at all, or at least to be unsure as to when a proof has finally been obtained. Here the issue is not at all the presence of computational assistance in the proof. One is dealing rather with a large-scale proof with many highly technical, conventional modules, not all of which had been thoroughly checked at the time of the announcement of the classification. What is needed here is a map of the proof, with clear evidence that each region is under control. It seems to me unlikely that, for either of the cases above, much would be gained by further formalizing or automation of the proofs.

### (c) Idealized proofs

With the development of mathematical logic over the last 150 years, a new idealized notion of proof emerged, that of a fully formalized proof on the basis of axioms. Whatever was controversial in the so-called foundational debates of the period from Frege to Godel, one could not deny, unless one were an intuitionist with a Brouwerian epistemology, that one had an algorithm for translating the majority of conventional mathematical statements into the semantics of one of the formalisms deriving from that debate, and that moreover one could go onto translate (again mechanically in principle) classical informal proofs into formal proofs of some accepted formal system (Principia, ZFC, or first-order Peano, etc.). I personally doubt that these translations are faithful to the creative processes of mathematics, and I deny that they constitute a case that set theory, in some form a common feature of almost all the axiomatic systems involved, is thereby established as ‘the’ foundation for mathematics. But I do believe that over a wide range these translations do map informal proofs to formal proofs, and that one can exploit this, even if one remains queasy about set theory, as foundation or otherwise.

That there is a long way to go from an informal proof to a formal ‘Hilbertian’ proof is clear, and probably few major theorems of the last 200 years have ever been fully formalized in this way. There is, however, a third possibility, namely the use of systems like Isabelle, which yield completely formalized proofs mechanically, and have instructions corresponding quite closely to the informal instructions, lemmas, definitions and other strategies of ordinary proofs. Good accounts are given in Constable's (1998) and Avigad's (2004).

Mackenzie (2005) gives an illuminating account of new uses of the term ‘proof’, in connection with the broad enterprise of computer verification. Moreover, as I had known from my own experience, there is considerable legal interest in issues of identity of these modern proofs. Philosophers and proof theorists have touched on the issue of a general theory of identity of proofs, but I personally regard this discussion as premature. I make some remarks on this later.

### (d) Hilbert's formalism

Via the above loose translation, proofs themselves became the subject matter of a part of mathematics, and one could, at least if one were Hilbert, imagine significant mathematical proofs about proofs and provability. It was clear that formal proofs are finite combinatorial entities like numerals, and thus one expected proofs about them to involve inductions, perhaps even very simple inductions. Only later would one realize that there are important arguments about proofs that require distinctly nonclassical combinatorics and inductions. On the one hand, it must have been clear from the outset that one needs sufficiently strong axioms to prove certain commonplace things. For example, no one ever seriously thought that one can derive much number theory from the axioms for commutative rings, and indeed one can prove this by the kind of model theory Hilbert used in the foundations of geometry (Shepherdson 1964). Hilbert had the imagination to see that one could not exclude, on the basis of anything known at the time, that one could prove the formal consistency of strong mathematical systems in very weak ones, such as primitive recursive arithmetic. Interesting as this mathematical possibility was, it has certainly been overemphasized, and this has distracted attention from more rewarding aspects of proof theory. The goal of my talk is to give a simple account, aimed at nonspecialists, of the significance for working mathematicians of the proof theory initiated by Hilbert. The account will be very selective, and indeed will involve neither recent proof theory nor a detailed account of classical proof theory.

### (e) Incompleteness

From my present perspective, the First Godel Incompleteness theorem is almost a peripheral result in proof theory. It is better regarded as a result in the theory of provability or computability, rather than having anything to do with the fine structure of formalized proofs. The results are of striking generality, and have little to do with the individual deductive or semantic mechanisms of particular formal axiomatic systems, and indeed the essence of the First Incompleteness theorem is surely to be found in such abstract discussions of recursion theory as Smullyan's (1961). Even the Second Incompleteness theorem can be suggestively analysed axiomatically, in terms of appropriate algebraic structures, and modal logic, as has been done in the theory of the provability predicate in such works as (Boolos 1993), and had been done in less generality much earlier by Hilbert and Bernays (1934, 1939). The Second Incompleteness theorem gets interesting twists in the case of strengthenings of ZFC, where one shows, e.g. that one cannot prove the existence, in a system *S* say, of a certain large cardinal, because that would allow one to prove the formal consistency of *S* in *S*. This is certainly a useful check on alleged proofs of existence, but little more.

Inevitably, people have tried to miniaturize the Godel machinery to get insights on *P*=NP, but with limited success. Of course new information has been uncovered, notably the failure of bounded arithmetic with total exponentiation to prove even consistency of the feeble system *Q* (Paris & Wilkie 1987). Note that in contrast this system proves Matejasevic's theorem, and e.g. the prime number theorem.

### (f) Completeness

Godel's Completeness theorem of 1930 has a different flavour. This is sensitive to the formal system used, though the method is very general, extending to all sorts of logics, some useful for computer science. The usual method of proof is to show that if something is not provable, then there is a structure, built from the syntax of the language using a relation of provable equivalence, in which the formula comes out false. One is not constructing a proof, or doing anything with the fine structure of proofs. Rather one is arguing by contradiction. Moreover, one knows, by the general technology of Incompleteness, that there are unprovable formula whose negation has no recursive model. It is noteworthy that two distinguished mathematicians, Herbrand and Skolem, were somehow blocked from (the simple proof of) the Completeness theorem by ideological constraints around the notion of truth. In this connection, one should read Cohen (2005), where he gives a related, but ultimately different, perspective on Skolem's role.

### (g) How Incompleteness evolved

Developments subsequent to Godel, refining the form of definition of the basic notions of recursion theory, and culminating in Matejasevic's theorem (Davis *et al*. 1976), show that the incompleteness phenomena go right down to sentences expressing the unsolvability of diophantine equations. This is at least startling, to see how set theoretic principles affect what one can prove about diophantine equations. Note that the diophantine incompleteness known now involves high-dimensional varieties, but it cannot be excluded, on the basis of present knowledge, that it goes right down to curves. This is a deplorable possibility (Shafarevic's gloomy joke) as it would have negative implications for major conjectures in arithmetic.

One of the most beautiful descendants of the First Incompleteness theorem is Higman's (1961), characterizing the finitely generated subgroups of finitely presented groups. This result is surely significant for group theory, but depends on methods that originated in proof theory.

### (h) Unprovability theory

The work of Godel and Cohen on the Continuum Hypothesis (CH) and the Axiom of Choice (AC) is not really proof theory, though it is certainly of the first importance for provability in systems of set theory. Cohen's work is of even greater importance, as having provided a flexible general method for constructing models of set theory. It has revived a flagging subject, and led to 40 years of spectacular activity (in combination with other methods). In the cases of both Cohen and Godel, one got much more than mere independence from their proofs.

I cannot resist mentioning a couple of cases where these results are relevant to mathematics apparently remote from set theory. Serre had in the 1950s, after his famous work on homotopy groups (Serre 1953), raised the issue as to whether one might really need the axiom of choice to prove the kind of statements he had proved. Serre had noted the use of Choice in connection with a homology/cohomology ‘duality’. Kreisel clarified the matter to Serre's satisfaction, thus. Over some weak system, the statements are formally equivalent to arithmetical statements, where the quantifiers range over only integers (finite ordinals, elements of *ω*). Serre's proof was, by inspection, in ZFC. Now, if there were a model *M* of ZF in which the statement failed, it would also fail in the model of constructible elements of *M*, because of its syntactic form, and so it would fail in a model of the axiom of choice. But Serre had a proof that it held in any model of ZFC. So it holds in all models of ZF, so there is a proof from these axioms, by Godel. Note that there is a recipe for translating Serre's proof into one not using ZFC, but Serre probably had no need to see this proof.

An important point here is the need to pay attention to the syntactic form of the assertion. This is always going to be relevant for interesting results.

A related example would use CH instead, showing that it cannot have any significance as far as provability of arithmetical results in ZFC is concerned. Examples of the use of this (worth knowing, though the method is not currently in use) are in Ax & Kochen (1965).

I do not know if anyone has ever worried about using the negation of AC or CH in number theory, but from the details of Cohen's method one sees that these are also eliminable, because Cohen's method does not extend the integers of models of set theory.

My second example also concerns the axiom of choice, this time its role in Deligne's monumental (Deligne 1980). At some point Deligne would get by more easily if he had an embedding of the *p*-adic numbers in the complexes (something which clearly exists by the axiom of choice). Deligne declares that AC is repugnant to him, and explicitly notes that all he needs in his subsequent proof is the embedding of any finitely generated subfield of the *p*-adics in the complexes. The proof of this involves just the basic combinatorics of elementary field theory, and certainly does not use AC. One should note, too, that the construction of the *p*-adics does not use the axiom of choice). On the other hand Deligne somehow has to survey his extremely complex proof, and convince himself that this is all he need. The latter is not in doubt, but tedious (even in principle) to demonstrate formally.

Now, Kreisel's argument would have sufficed for Deligne's purposes, provided two things:

The conclusion he wanted is arithmetical;

His proof is in ZFC.

Both aspects are delicate. Deligne's most general conclusion is about constructible sheaves, and is perhaps not arithmetical. But his applications to nonprojective varieties are certainly arithmetical, so that at least for these Kreisel's argument would apply provided the whole proof was done in ZFC. It is probable that in all cases Deligne's argument can be adapted, by working in a suitable *L*[*A*]. Such an exercise seems worthwhile.

That his proof is in ZFC seems clear to me, but remarks in (Browder 1976) attributed to Manin suggest that some experts have not been quite sure about this.

Deligne is, of course, right in suspecting that some trace of AC is needed to embed the *p*-adics in the complexes. Cherlin and I checked (unpublished) that in Solovay's famous model (Solovay 1970) there is no such embedding, by showing that the embedding would have to be continuous.

### (i) Provability theory

Another aspect of provability theory not often given the same prominence as the Godelian phenomenon is that there are many cases now where one has a complete, intelligible (and sometimes recursive) set of axioms for a natural mathematical domain, usually geometrical. Examples are algebraically closed fields, real closed fields, *p*-adic fields, and various fields with analytic functions. Easy arguments use this fact to give nontrivial uniformities and/or recursive bounds sometimes not evident to the original provers of the theorems. Moreover, the bounds and algorithms coming from this area are generally relevant for computer science, though perhaps not for automated deduction.

A recurring issue at our meeting was Hales's proof of Kepler's Conjecture. It is important to stress that the point at which Hales needs computer assistance is for a proof of a statement in high-dimensional semi-algebraic geometry, one of the most important subjects where one has a Completeness theorem. In principle one can effectively find a proof of Hales's semi-algebraic result, if it is true, from purely algebraic axioms. Unfortunately, one knows that in the general case the waiting time for a proof is unrealistically long. However, logicians and computer scientists have uncovered much information on this topic, and it may be worthwhile to see if any of the accumulated insights are useful in cross-checking the Hales result or in shortening its proof.

An essential point in the above, and in most of what follows, is the unsystematic nature of the applications. One has to know a fair bit of the subject matter, and understand the proofs therein, before one can apply logical principles to get something interesting. In particular, most of the applications are done without recourse to any axiomatic system with general objectives.

We turn now to genuine proof theory, and not just provability theory.

## 2. Proof theory

### (a) The fundamental theorems

Modern proof theory begins with the *ϵ*-theorem of Hilbert, and becomes applicable in the work of Herbrand (1930) and Gentzen (1969). This work is of permanent importance (it seems to me) in the face of the Godelian phenomenon. The importance for computer science can hardly be disputed. I am concerned here rather with the relevance to existing mathematical proofs.

Herbrand's work was not readily assimilated, but it is now at the base of the proof theory of computer science (where more general notions of proof or verification are en vogue). The essential feature of his method is that provability from universal axioms of an ∀∃ sentence implies that a finite disjunction of quantifier-free instantiations is proved. This is almost trivial model theoretically in first-order logic, but the formal version can be extended to general shapes of axioms, provided one passes to suitable extensions by function symbols, and has proved both powerful and suggestive. A typical case is the following (from page 120 of Girard (1987)):

2.1 *Let A be a formula in prenex form, for instance**with R quantifier-free*. *let f and g be two new function letters with f unary and g binary*. *The A is provable in predicate calculus iff there are terms U*_{1},…,*U*_{n}, *W*_{1},…,*W*_{n} (*using the letters f and g*) *such that**is a propositional tautology*.

Model-theoretically, with the axiom of choice assumed, this is utterly trivial, and easily generalized. But the theorem has nothing to do with the axiom of choice. It is purely combinatorial and tells one that one cannot have a predicate calculus proof without having provability of a formal Herbrand disjunction. It is noteworthy that in applications (see for example Luckhardt's work discussed later) the mere knowledge that some disjunction should be looked for has been helpful in obtaining hidden bounds in proofs. Of course, the combinatorics of the Herbrand terms is in general beyond control, and indeed the proof theory of such terms is still not at a point where applications of this aspect have been obtained. The work on unification, arising from resolution, may be regarded as a special case, but little positive has been obtained.

Gentzen's work on cut-elimination and the subformula property, has been pushed much further by both mathematical logicians and computer scientists. The work of both, and their followers, has allowed applications of proof theory to mathematics. This is not the place to go into an account of the sequent calculus, and an explicit statement of what is cut-elimination. It is surely better to quote Girard (1987), p. 95:

Roughly speaking, a cut-free proof is a proof from which all formulas which are ‘too general’ have been banished. General formulas in a proof carry the ideas of the proof: it is only because we have general formulas that we can have short and intelligible proofs; when, in the Hauptsatz, we eliminate all these general formulas, we increase the length and obscurity of the proof: for that reason, cut-free proofs are unlikely objects for mathematical practice. Their interest lies somewhere else: these proofs are very interesting to study, because their general properties are very important.

Of course, this is not precise, but it is suggestive. For the formal details of the Hauptsatz, and all sorts of interesting asides, one can consult Girard's frequently intemperate (Girard 1987).

For an account of the connections between the two methods, see Girard (1987), p. 122.

Much nonsense has been pronounced about Gentzen's work, even by extremely distinguished people. Consistency is not really the main issue at all. He did reveal fine structure in the unprovability of consistency of PA, as a consequence of much deeper general methodology. It is not a question of proving the consistency of induction on *ω* by something evidently stronger. The real point is that the ordinal *ϵ*_{0} has a very simple primitive recursive representation, and yet we cannot prove in PA the principle of induction for a specific quantifier-free predicate on *ϵ*_{0}. This principle is almost as clear intuitively as that for induction on *ω* for simple predicates. Gentzen showed, by what remain deep mathematical ideas, that this principle proves the consistency of PA, and, moreover, opened the way for later people to observe that one can give a satisfying answer to the question of the nature of the provably total functions of PA (in the technical sense of Bucholz & Wainer (1987)). They have to be recursive, but obtainable by a scheme of recursion on an ordinal less than *ϵ*_{0}. This led to an intelligible form for such functions (Kreisel–Wainer hierarchy), and later refinements to subsystems of PA (and a research programme related to *P*=NP). Kreisel spotted the phenomenon, and made the basic observations, which had a strong influence on major work such as that of Ketonen and Solovay. Many later workers identified similar behaviour for other systems (including higher-order systems, e.g. Godel's *T*).

In summary, Gentzen laid bare the fine structure of provability in predicate calculus, and then in some very specific and important systems (such as PA), going much deeper than Godel. But of course one had to start afresh in seeking similar analyses for stronger (or, much later, weaker systems) whereas one had the Godel analysis for all natural systems. It is to be stressed that much of the later heroic work of this nature has not given any spin-off in terms of hidden information.

This development provoked Kreisel's memorable question:

What more do we know when we have proved (or have a proof of) a sentence *A* in system *S*, rather than mere truth (if the system is a conventionally motivated one)?

A typical answer is that depending on the syntactic form of the sentence, we may get rate of growth information on witnesses for its existential quantifiers. This is certainly potentially valuable.

### (b) Complex methods in arithmetic

Godel proved that passage to second-order arithmetic (in the axiomatic sense) increases our stock of provable first-order formulas (e.g. consistency statements). But this alone left open the possibility that proofs of arithmetical statements via complex analysis (doable in second-order arithmetic) could be replaced by first-order proofs. An example, of doubtful significance, is the elementary proof of the prime number theorem. I do not know what new information one gets from that over a classical complex analysis proof. Moreover, the elementary proof generalizes, to Dirichlet situations, with difficulty, and beyond that not at all. So it is a concrete question as to whether there is a more subtle Godel phenomenon in analytic number theory. One has to formulate the question sensibly, of course. The model theory of sine on the reals codes second-order arithmetic, and so suitably interpreted proves consistency of PA or indeed second-order arithmetic. This is not what is intended! Rather, is there something in all the interesting, mainstream proofs, using complex analysis, which allows one to reproduce them (no doubt with loss of beauty and intelligibility) in first-order arithmetic (say PA)? The fact is that there is. The first examples are due to Kreisel in the early 1950s (Kreisel 1951, 1952). The lack of detail in his discussions has been noted by Feferman in a very useful article (Feferman 1996), but to me the matter has always been clear enough. I have not seen the need to bring in general purpose formal systems and prove the conservative nature of Konig's Lemma, though there is a point to this. It is equally obvious that other more ad hoc methods work.

As discussed by both Luckhardt and Feferman in ‘Kreiseliana’ (Odifreddi 1996), Kreisel sketched an argument for the effective content of Littlewood's famous result showing that the difference between pi(*x*) and li(*x*) changes sign infinitely often. Here there are some little formal-logical tricks, which, when used by one familiar with Littlewood's proof, provide bounds (not very sharp, of course, but this was never the issue). It seems to me that this proof of Littlewood is readily converted to one in bounded arithmetic plus total exponentiation, and this alone would yield iterated exponential bounds, with the length of the tower coming from a careful analysis of the inductions used in the proof.

### (c) Isabelle

We have recently been told that the prime number theorem has been done in the system Isabelle. I guessed, on hearing this, correctly, that it must be the elementary proof, i.e. the least suggestive one. It turns out that Isabelle does not have a complex number library. But then, is it doing number theory, nearly 200 years since complex analysis began to show in number theory? I do not wish to quibble here. But there is an important point. The proof formalized is one which is certainly doable in bounded arithmetic plus exponentiation, and one gets the impression that Isabelle can code this sort of thing almost routinely. But it does not deal naturally with geometric or topological arguments, and thereby is well out of step with modern number theory.

It is regrettable that one did not really have time at the meeting to get an extended statement of the goals of this kind of automatic theorem proving. Barendregt introduced the basics (and referred to the prime number theorem) but we must wait for a subsequent meeting to get a clear sight on the goals of this proof enterprise. My impression is that those making the most serious contributions to the enterprise of this kind of automatic theorem proving are not making any grand claims, and readily acknowledge that one is rather a long way from having a ‘library’ useful either for basic education in complex analysis or for more advanced algorithmic purposes.

### (d) From mere truth to effective bounds

Sometimes one has a problem posed by high-level practitioners, such as Weil's on whether one could obtain bounds in Hasse's Norm theorem. I came to this question by noting, to my surprise, that Serre (1997), settled for a general recursive argument to decide when something is a norm. I worked out primitive recursive bounds by going through (partially with Kreisel) an analysis of class field theory, with its appeal to both analysis and cohomology. Both caused me lots of pain, particularly the use of Herbrand quotients in cohomology, where crucial information gets cut away. (It is notable that the function field case of class field theory is much more explicit than the numberfield case.) When I had finished, it was pointed out to me that Siegel, in a late paper, had given much better bounds, via geometry of numbers, just using the fact that the theorem was true, but without appealing to any particular proof. Thus there is a lesson here. Sometimes one does not need to do deconstruction on a proof to get constructive information about what has been proved, or is true.

### (e) Unwinding

Kreisel has been the main contributor to ‘unwinding’. This is the activity of taking an informal mathematical proof, giving an analysis of where it is proved (i.e. in which formal axiomatic system), and doing some thought experiments on that proof to give sharper information on what is being proved (usually more than the original prover thought). The thought experiments involve varied means, which Kreisel compared to the means of applied mathematics. It is not easy, and perhaps not even worthwhile, to formalize/systematize them. It is, on the other hand, at least healthy for mathematics if some people know these techniques very well, and look out for areas in which to apply them.

### (f) Texts on unwinding

There are a number of interesting texts about this approach, not uniformly appreciative. There are the papers of Feferman and Luckhardt in ‘Kreiseliana’, and the recent lectures of Avigad (2004) at ASL 2004 on proof mining. These cover the majority of the applications. It is fair to say that there are not many applications after 50 years. But then, there are few applications of topos theory, or model theory of sheaves, to geometry. That is no reason to abandon the teaching of such material. In both cases, applications will come only when the material is familiar to people who know also the intended area of application. Without this combination of expertise, nothing is to be expected.

The commentators on unwinding list all of Kreisel's efforts and the recent papers refer also to the work of Kohlenbach. Neither refers to the paper by Kreisel & Macintyre (1982), concerning the conditional proofs giving effective estimates in finiteness theorems in number theory from the assumption of effective estimates in Roth's theorem. Even granted that the promised sequel to that paper has not been written, this seems a bit strange. Contrary to the title, we did not advocate the informal method of algebraization as a replacement for unwinding methods more closely linked to proof theory. We did, however, wish to point out, for the particular situation of Siegel's theorem, there are serious limitations of the methods based only on proof theory, and that one does better by an ad hoc treatment based partially on algebraizing (which may involve axiomatizing) the complicated mix of methods that go into the proofs of the Finiteness theorems. The treatment in Serre's (1997) was congenial to us, and we fitted our analysis to it.

From the perspective of this paper, the mathematical significance of proof theory is that it provides methods, which can, if used with discretion, reorganize informal proofs so that they yield more information. Thus, I disregard the other side of the matter that there are some beautiful and difficult theorems in proof theory, serious mathematics with no applications in mind. And, above all, I pass over in silence any thought that proof theory has significance for foundations of mathematics. That mathematics can be formalized, and that much of it can be axiomatized, is a basic discovery, essential to know, but not deep knowledge.

## 3. Unwinding

### (a) Examples

Kreisel has brought unwinding to bear on:

analytic number theory;

number of solutions to diophantine problems;

bounding solutions to diophantine problems;

bounds in Hilbert's 17th Problem;

bounds in polynomial ideals.

Girard has brought proof theory to bear on proofs of van der Waerden's theorem using dynamical systems (and this might be relevant even for primes in arithmetic progression, etc.).

Luckhardt has applied Kreiselian tricks, involving the Herbrand formalism, to the issue of number of solutions in Roth' theorem.

Kohlenbach has used serious proof theory on problems in modern approximation theory.

There is no time here (especially in the context of a Discussion Meeting) to go through details of each case (Feferman does run through the differences between cases) though I will say a little. Avigad's lectures and Kohlenbach's papers (Kohlenbach 2001; Kohlenbach & Olivia 2003*a*,*b*) provide the most systematic account I know. I personally am partial to the fulminating account given by Girard. I stress only the diversity of the problems, and the common feature that one is not dealing with a fully formalized proof here, but an informal conception of a full formalization of such a proof, to which one applies the general technology of the proof theory of Herbrand, Gentzen, Godel, Kreisel and others.

As said before, the difference from other points of view here is that one concentrates on seeing what more logic can reveal from the mere existence of a proof in a particular system. There is nothing in the method that casts light on the use of computational auxiliaries.

### (b) Fully formalized proofs

Avigad has an interesting article which contains a reasoned account of Isabelle and the like. There is no question of these systems existing to find new mathematical theorems. Rather they are designed to provide intelligible intermediaries, proofs of existing results presented not in the impenetrable armour of Hilbertian proof (as if they could be!) but rather in some natural evolving formalism that corresponds to low-level mathematical communication (but using higher-level instructions!!). This still leaves the question as to why they communicate the obscure proof and not the clear one.

### (c) Girard unwinding

What I want to communicate in this meeting on the nature of proof is merely that one can apply the technical tools of mathematical logic to extract hidden and valuable information from complex proofs. These proofs need not be fully formalized, but a sine qua non of the method is an ability to understand in what, preferably weak, system the informal proof has a formal counterpart. For this you need to understand the proof. For example, if you use compactness or completeness, you should know something about the logical complexity of the predicates to which you apply these principles. Here you have to unwind the proof, or perhaps modify slightly, and then unwind. In effect, you have to be aware of a small number of systems in which the bulk of current mathematics can be carried out (ZFC is far too strong), and then you need to know some specifics of their proof theory. With this repertoire, you are in a position to extract useful information from informal proofs. However, it does not seem crucial right now to be expert on ordinal aspects of the theories, though one can well imagine that abstract invariants of proofs can at some point be valuable.

It is a somewhat startling fact that one can, as Girard does, use cut-elimination on a portion of an informal proof. This is possible, because he has a clear view of a formal system in which that part of the proof can be formalized, and he understands perfectly the algebra of cut-elimination, so can apply it ‘in a higher order way’. Essentially he restructures the proof to a formal induction in arithmetic.

What does Girard do? He begins with the memorable proof, by Furstenberg and Weiss, using dynamical systems, of the van der Waerden theorem on arithmetic progressions. From the mere truth of that theorem one gets the existence of a function *W*(*p*, *k*) such that given any partition of the set 0,…,*W*(*p*, *k*)−1 into *k* classes then one of the classes contains an arithmetic progression of length *p*. Of course, there are then many such functions, and the question is whether *W* can be chosen to have better properties, e.g. in terms of computability or rate of growth.

That *W* can be chosen recursive is general nonsense and essentially useless. That *W* can be chosen to have growth rate around that of the Ackermann function has been known for a long time, and can be read off from any elementary proof. After the unwinding efforts I will describe below, Shelah (1988) showed that *W* can be chosen primitive recursive, and indeed low in the Kreisel–Wainer hierarchy. Later still, the work of Gowers, using analytic methods, got even better bounds. The bounds by the last two authors are far better than those unwound by Girard, but this is not the point. It is not obvious how to extract bounds from Furstenberg–Weiss, and Girard shows how proof-theoretic tricks of the trade, in the hands of a master, enable one to get bounds.

There seems to me no point, in a brief discussion paper, embarking on an outline of Girard's proof, especially as he gives a lively, explicit account in Girard (1987). The essential point is to break down the proofs of the high-level dynamics proofs, done for general spaces *X*, into a series of proofs in arithmetic, which take account of the specific *X* needed at each stage of the conventional inductive proof (powers of the space used in the deduction of van der Waerden occur in this unwinding). He made his task easier by a series of ‘astuces’, making small observations that would gain Fursstenberg–Weiss nothing, but are crucial for keeping down the complexity of unwinding. Thus, he makes uses of certain symmetry arguments, and the fact that his space *X* is ultrametric, to avoid complicating the induction, and thereby the unwinding. After this preparation, Girard has a memorable geometrical picture. The process introduces other cuts, but he has managed things so they will have no dynamical significance. After the elimination of the dynamical systems components he gets a bound of Ackermann type for the van der Waerden theorem. What he has unwound is really a minor (from the dynamics viewpoint) variant of Furstenberg–Weiss. I again stress that it is not the quality of the bounds that matter, but the fact that a skilled proof theorist, using in an imaginative way classic theorems of the subject, can get bounds that eluded the first generation of mathematicians who gave noncombinatorial proofs of van der Waerden. It is no surprise that methods more closely tied to the subject matter will eventually do better than a powerful general method.

Girard, later in the book, does another, quite different unwinding, using the so-called no-counterexample interpretation. This method was first popularized by Kreisel, though it has its origins in work of Godel from the 1930s (It can be derived by either the method of Herbrand or the method of Gentzen.). This time he analyses directly the Furstenberg–Weiss proof via minimal dynamical systems. There is still a cut-elimination that can be done, but not on the proof of existence of minimal systems. On that he uses a sequence of no-counterexample interpretations, thus opening the way to bounds. These turn out to be at a level above that of the Ackermann function! This confirms a moral of Kreisel that small differences in a proof can make an enormous difference to the information one can extract. This is not, of course, catastrophe theory for proofs!!

Girard's accounts of his two unwindings are illuminating and very explicit, but his method is perhaps a bit special. The general shape of applicable result from proof theory is that if something is proved then in truth it has a very special Skolemization or Herbrandization maybe involving higher-order functionals. This may or may not have to do with a cut-elimination. Moreover, one can often make a proof in a prima facie strong system work in a much weaker system, so that for example one gets iterated exponential bounds by doing a proof in bounded arithmetic plus exp (in particular, it seems that all of Hardy & Wright (1979) can be codified there, including the elementary proof of the prime number theorem—what is different about the Isabelle proof?). In still other cases, one is on the non-Godelian side of the fence, and one can use fast elimination, etc., to get bounds systematically—of course in general inferior to those got by specific methods like cohomology.

The vigilant reader may have noticed that I have mentioned only briefly the functional interpretations deriving from Godel. They are somewhat unwieldy in practice because of the iterated implications (though, as we see below, there are contexts where they work very well). I leave it to the reader to ponder the remarks of Girard (1987), concerning the place of this interpretation in Godel's opus.

### (d) Identity of proofs

Though it may well be worthwhile (even for lawyers) the attempt to formalize notions of identity of proofs are not discussed here. When an important theorem has many proofs (e.g. quadratic reciprocity) mathematicians will want to compare the merits of these proofs. It is unlikely to be worthwhile to consider all 153 proofs of quadratic reciprocity, but most number theorists would agree that quadratic reciprocity is a part of a greater theory, class field theory, and that in turn part of a greater (Langlands theory) and thus one is mainly interested in proofs that generalize. This is one of the defects of the elementary proof of the prime number theorem, that it does not generalize widely, and moreover it suppresses sight of e.g. zeta functions. It can very well be that a special proof has other virtues, e.g. for computational complexity. Recall the example of Sylevster's proof of infinitude of primes (Woods 1981). It does not appeal to entities of exponential growth, almost uniquely among such proofs (at least in the sense of appeal that logicians use).

The main point here is that we do not at the moment have any clear sense of the extra information concealed in different proofs of the same theorem, especially if these proofs are formalized in the same Hilbertian system. It is good to draw attention to these things, as Kreisel has often done, but it is certainly premature to attempt to formulate any philosophy of such matters. It is already important to note, as Kreisel does, and Girard does, that small differences in proof can make a great difference to what can be extracted.

### (e) Kohlenbach's work

Kohlenbach's papers provide a detailed account of the technicalities of unwinding, first for Cebychev's theorem, and subsequently for more complex problems. But as always the idea is to get some formal simplification proved, and then be able to bound something usefully. This would have to happen in the Littlewood case for Kreisel to have had real success there. One does not expect general considerations to provide such bounds, and real work will always be needed. What is significant is that the proof-theoretic manipulations give a real advantage (definitely for Kohlenbach).

The functional interpretations are descended from Herbrand's theorem. This has an almost trivial model-theoretic proof, in a useful special case. But the general case is typically daunting to all but proof theorists. Moreover, the Godel functional interpretation is for intuitionistic systems, again not exactly attractive to classical mathematicians.

Herbrand's theorem can be extended to higher complexity formulas by the devices of Skolemization and Herbrandization, though this is not how Herbrand did it. There is a useful account in Buss's (1998) survey, giving the link to staples of computer science, such as resolution and unification. But the essential point is that if something is provable in certain systems, it has a proof which gives more in the way of witnessing existential quantifiers, and is thus natural/explicit. Put differently, it reveals a nontrivial uniformity.

Kreisel has repeatedly pointed out that classical proof theory has not achieved any serious combinatorial analysis of the Herbrand terms, and that one is unlikely to go much deeper in unwinding unless one has some perhaps quite elementary methods for reasoning about this kind of thing.

The Godel functional interpretation translates intuitionistic higher-order arithmetic into a quantifier-free axiom system for primitive recursive functionals of higher type. The recursion is purely formal. In particular it provides yet another consistency proof for PA, and one may wonder what the point/need of that is/was. The point emphasized here, and derived from Kreisel, is that it is at least equally rewarding to see what this translation gives as a tool for extracting bounds from proofs.

On the one hand, it subsumes the no-counterexample interpretation as used by Girard. On the other, it is the method that Kohlenbach uses in his unwinding of much of classical approximation theory. A perhaps temporary advantage of Kohlenbach's work is that the bounds obtained are better than any others known.

Finally, there is the Herbrand technique used by Kreisel and later Luckhardt (1996) to bound the number of solutions in diophantine problems in cases when one does not have any bound on the location of the solutions. In fact such situations in diophantine geometry seem to be the norm in practice. In Cohen's talk he described such situations as providing most of the very few genuinely nonconstructive proofs in mathematics. Typical examples are Siegel's theorem or Faltings theorem, where effective estimates are known for the number of zeros, and where logic proofs can usually get this too. In the unwindings of this kind, so far, one does not need to pay any attention to the formal system in which the result was proved. Rather one looks for a Herbrand form that is being proved. In practice one finds one, and one knows what one needs on the growth rate. Then, even for the classical proof Luckhardt beats the Davenport–Roth bound, and for the Esnault–Viehweg proof Luckhardt was able to get by logical devices the same bound as Bombieri–van der Poorten. That he did not do better is not the point. But it is an important part of the description of the particular tricks of the trade used here that no real proof theory is used, only the guiding principle that one will be well prepared to get a bound for the number if one gets a Herbrand form with sufficiently good growth rate. Naturally one hopes to combine this with higher technology from proof theory to do better, but no hint of how to proceed thus has been found.

## 4. Closing remarks

My main impression of the meeting is that the mathematicians and computer scientists did not really get close to understanding each other (despite many illuminating exchanges). The problems go well beyond those concerning strategies in theorem proving by mathematicians and the strategies of the artificial intelligence community. I, as a mathematical logician, operate closer to the borders than most participants at the meeting, and I have been left with a sense of having missed something basic. I chose to talk on the use of precise theorems from Hilbertian proof theory formal proof to extract hidden information from informal mathematical proofs. I have tried to reflect on the enterprise, explicitly championed by Hales on his website, of producing fully formalized proofs of important results in geometry. Hales is quite explicit that he sees this as the only way of convincing the mathematical community of the correctness of his entire proof of the Kepler Conjecture. One thing that worries me is that we seem to have no theory underlying this enterprise, and this it is difficult to relate it to other formal activities in proof theory. Moreover, I rather doubt that complete formalization will satisfy many mathematicians.

There are some references I wish to add for those who would like to look a bit further in the directions set in this paper. One is a rich discussion by Kreisel (1990) on logical aspects of computation. The others are from Hales and the enterprise of full formalization. They state clear enough goals, but leave me with a sense of having missed something. They are the statements about Flyspeck, and that about the QED Project.1

I cannot imagine any useful sequel to our meeting in which the above discussions are not pursued.

## Footnotes

One contribution of 13 to a Discussion Meeting Issue ‘The nature of mathematical proof’.

- © 2005 The Royal Society