A Lost Proof

Christoph Benzmüller¹
Manfred Kerber²

ABSTRACT

We re-investigate a proof example presented by George Boolos which perspicuously illustrates Gödel's argument for the potentially drastic increase of proof-lengths in formal systems when carrying through the argument at too low a level. More concretely, restricting the order of the logic in which the proof is carried through to the order of the logic in which the problem is formulated in the first place can result in unmanageable long proofs, although there are short proofs in a logic of higher order. Our motivation in this paper is of practical nature and its aim is to sketch the implications of this example to current technology in automated theorem proving, to point to related questions about the foundational character of type theory (without explicit comprehension axioms) for mathematics, and to work out some challenging aspects with regard to the automation of this proof - which, as we belief, nicely illustrates the discrepancy between the creativity and intuition required in mathematics and the limitations of state of the art theorem provers.

1.  Introduction

Higher-order logic allows quantification over function and predicate variables and thus provides a far more expressive language than first-order logic. It was Bertrand Russell [Russell02,Russell03] who first pointed out in 1902 that in connection with the unrestricted comprehension principlesThese principles assure the existence of certain functions, we will come back to them in Subsection 2.1. this may allow for paradoxes.Paradoxes occur equally in first-order axiomatisations of set theory with unrestricted comprehension principles. The most prominent example is the set of all non-self-containing sets (also called Russell's paradox). As a possible solution Russell suggested a few years later in [Russell08] a theory of types as a basis for the formalisation of mathematics that differentiates between objects and sets (or functions) consisting of these kinds of objects. This idea was also taken up by Alonzo Church in 1940, who introduced a formulation of type theory [Church40], also called simple theory of types, based on Russell's ideas which is taken as a basis formalism in many modern higher-order theorem provers. Church's lambda calculus and his theory of types also opened the door for the propositions as types idea and constructive type theory.

TPS [andrews00:systemdescr,andrews:tatpsfctt96], Hol [Gordon85], Omega [OwRu92], Omega [BenzmuellerEtAl:otama97], lambda-Clam [CADE98*129], Leo [BeKo:LAHOTP98] are interactive and automated higher-order provers based on the simple theory of types. Some prominent provers working for constructive type theory are uprl [Constable86], COQ [CoqMan95], and LEGO [luo92:legoproofdevelsystem].

Automating proof search in higher-order logic is a very challenging enterprise, such that the above systems all provide facilities to combine interaction with automation. The idea is that the interactive human provides the crucial proof steps while simple subgoals are handled automatically by the prover. Of course, many non-trivial proofs can be already automated in higher-order logic and the most impressive record in this sense is given by the theorems proven automatically with TPS [andrews00:systemdescr,andrews:tatpsfctt96]. A well known and very simple example illustrating the expressiveness and elegance of automated higher order theorem proving is Cantor's theorem, where the diagonalisation argument, in form of a lambda-term, is synthesised by higher-order unification. For further and more impressive examples we refer to [andrews:tatpsfctt96].

However, as we will discuss below Boolos' example perspicuously demonstrates the limitations of current first-order and higher-order theorem proving technology. As we will illustrate, with current technology it is not possible to find his proof automatically, even worse, automation seems very far out of reach. Let's first give a high-level description why this is so. Firstly, Boolos' proofs need comprehension principles to be available and it employs different complex instances of them. It is important to note here that theorem provers based on Church's theory of types typically assume that the comprehension principles can be completely avoided due to the power of higher-order unification and the existence of lambda-terms. First-order theorem provers use no comprehension principle nor typically any other definition principle to introduce new concepts. Secondly, the particular instances of the comprehension axioms cannot be determined by higher-order unification but are so-called Eureka-steps which have to be guessed. However the required instantiations here are so complex that it is unrealistic to assume that they can be guessed, for instance, by blindly applying the primitive substitution principle [andrews:tatpsfctt96], by splitting rules [Huet72,Huet73b], or by concisely representing them so that new ones can be generated during the proof search [Kerber94-ECAI]. Here it is where human intuition and creativity comes into play, and the question arises how this kind of creativity can be realised and mirrored in a theorem prover.

In the following we concentrate on the classical notion of higher-order logic and, in particular, on the simple theory of types, that is, a classical higher-order logic based on Church's simply typed lambda-calculus [Church40]. For an introduction to the pure simply typed lambda-calculus we refer to [Barendregt84].

Even though our viewpoint here is from classical higher-order logic the problem is more general and applies to constructive type theory [Martin-Loef84] and other approaches as well.

2.  Automating Higher-Order Proof Search

In the rest of this section, we briefly discuss some specifics of theorem proving in higher-order logic.

2.1.  Comprehension

The theorem proving approaches from above as well as the systems mentioned in the introduction therefore avoid the infinitely many comprehension axioms altogether.

2.2.  Primitive Substitution

In Huet's resolution approach the splitting rules address this problem, which are replaced in Andrews' work [Andrews:ocahol89] by the more elegant primitive substitution principle. Splitting or primitive substitution blindly instantiates free set variables at literal head positions with a most general binding (partial binding) that imitates a logical connective, that is, with a most general formula that introduces a logical connective as head. For instance, the set of most general bindings for head variable p of the literal p(Y) from above is p <-- lambda z . NOT  b¹(z), p <-- lambda z . b²(z) v b³(z), p <-- lambda z . FORALL w _beta . b⁴(z,w) where b^1,2,3 _{i  ->  o} and b⁴ _{i  ->  ( beta  ->  o)} are new free head variables. Since there are infinitely many universal quantifiers in the simple theory of types (one for each type beta ) splitting and primitive substitution are infinitely branching. And as new free predicate variables are introduced they are recursively applicable to the results of their application. From an abstract point of view they realise a blind enumeration of all formula schemes in the Herbrand universe.

Clearly an unrestricted blind enumeration in this sense is practically infeasible. [andrews:tatpsfctt96] therefore explains how this problem is handled in the TPS prover, which instead of a blind enumeration works with some selectively chosen instances.

2.3.  Extensionality

3.  "A Curious Inference"

In this section we take a closer look at this example and shed light on the question why a comprehension axiom of second-order logic is needed and even first-order with definition principle wouldn't suffice to generate short proofs.

Boolos assumes an inference system in the first-order predicate calculus with identity and function symbols s (unary) and f (binary).

1. FORALL  n.  f(n,1)=s(1)
2. FORALL  x.  f(1,s(x))=s(s(f(1,x)))
3. FORALL  n. FORALL  x. f(s(n),s(x))=f(n,f(s(n),x))
4. D(1)
5. FORALL  x. (D(x) ->  D(s(x)))
        hence
6. D(f(s(s(s(s(1)))),s(s(s(s(1))))))

Notice that there is no induction principle available. If it were available there would be a proof in two steps, namely because of (4) and (5), we would get FORALL  x. D(x) by induction and hence D(f(s(s(s(s(1)))),s(s(s(s(1)))))) by FORALL-elimination.

Actually, there is a relatively easy but enormously long proof. f is an Ackermann function and it is possible to prove the conclusion by f(s(s(s(s(1)))), s(s(s(s(1)))))-1 many application of Modus ponens from (4) with (5) to come to (6). Function f as defined in (1)-(3) grows extremely fast and hence f(s(s(s(s(1)))),s(s(s(s(1))))) is a very big numberNumber in the sense that f(s(s(s(s(1)))),s(s(s(s(1))))) unravels into the successive application of a very big number of s's to 1; in fact, Boolos shows that this number is at least the result of an exponantial stack 2^(2***2) containing 64K `2s' in all. such that there is no chance to actually perform so many applications with all computation power ever.

A proof in second-order logic makes use of comprehension axioms, in particular, of the following twoIn the comprehension schema in Subsection 2.1 we employed = to cover the general case. Here N is a predicate and N(z) a term of type o such that = can be replaced by  <->  by boolean extensionality as introduced in Subsection 2.3.: EXISTS  N. FORALL  z. N(z) <-> (FORALL  X. X(1) & FORALL  y. (X(y) ->  X(s(y))) ->  X(z)) EXISTS  E. FORALL  z. E(z) <-> (N(z) &  D(z))

With this comprehension principle Boolos proves strong lemmata which can be viewed as conditional induction principle of the kind: "assumed the induction principle holds for number z - corresponding to N(z) - then we can show for any predicate X a property X(z) by induction."

The proof goes as follows; first you establish the following lemmata:

Lemma 1: N(1), FORALL  y. (N(y) -> N(s(y))), N(s(s(s(s(1))))), E(1), FORALL  y. (E(y) -> E(s(y))), and E(s(1))
Proof sketch: These are easy consequences of the axioms.

Lemma 2: FORALL  n. N(n) -> FORALL  x. (N(x) -> E(f(n,x)))
Proof sketch:

• Define M(n) <-> (FORALL  x. N(x) -> E(f(n,x)). We want FORALL  n. (N(n) -> M(n)). Enough to show M(1) and FORALL  n. (M(n) -> M(s(n))), since then from N(n) follows M(n) by definition of N(n) as N(z) <-> (FORALL  X. X(1) & FORALL  y. (X(y) -> X(s(y))) ->  X(z)) We can instantiate X by M, in particular, the definition of N does not refer to M and is a proper definition.

Boolos' proof makes a couple of times use of the comprehension principle:

Boolos' example - as well as Gödel's results - show that even for cases in which it is sufficient to stay completely in first-order logic in principle, it may not be sufficient in practice.

4.  Implications, Questions, and Challenges

4.1.  Implications for existing Higher-order theorem proving approaches

Of course, theoretically there are the extensionality axioms which contain higher order variables. Furthermore, in our particular case one could think of adding some new axioms like FORALL b_o . EXISTS N _{alpha ⁿ ->  o} . FORALL zⁿ . N(zⁿ) = b instead of all comprehension axioms. The idea would be to leave the particular structure of the terms to the right open at the beginning and to employ primitive substitution to generate respective instances for b (which may depend on z) during proof search. A third option is to introduce free variables via the following tertium non datur axiom FORALL b_o . b v NOT  b Whereas it seems to be impossible to derive the required comprehension axioms from the extensionality axioms by applying the primitive substitution principle, this is far more promising in the latter cases. However, as remarked in Subsection 2.2, without guidance, primitive substitution just subsequently enumerates formula schemes, such that this would differ only slightly from a direct enumeration of all comprehension axioms (for terms B of type o).

As remarked in Subsection 2.1 current approaches typically completely avoid the comprehension axioms (in practical applications the extensionality axioms and the tertium non datur axiom are avoided as well). Thus, Boolos elegant higher-order proof is not supported in these approaches. However, there exist completeness proofs for them ensuring that any formula that is valid in Henkin semantics can indeed be shown as such. Of course, the intractable first-order proof for Boolos' examples can theoretically be synthesised, so the example is not a counterexample to, but an example of these completeness result. It demonstrates well what completeness means, namely that practically a proof may not be found since proofs are prohibitively long. While this is clear for problems which do not have short proofs, Boolos' example has a practically tractable (with respect to its size) higher-order proof. It gets lost, however, in standard higher-order theorem proving because the comprehension schemes (or alternative axioms) are not available. Hence the question arises whether it makes sense at all to avoid the comprehension principles in the simple theory of types if this has the side effect that some tractable proofs get lost thereby. Especially in systems aiming at supporting non-trivial mathematics, where similar elegant proof constructions are potentially required this could be a serious problem.

4.2.  Why is Boolos' example so challenging

• Firstly, this problem cannot be solved by simply following the obvious path. In order to recognise that and to try to avoid the trap of following myriads of modus ponens rules, one would either have to know a priori that an Ackermann function is involved and brute force won't lead to success, or after a while - on reflection of the progress - one would recognise that a brute force approach is not promising.
• Secondly, a human mathematician can recognise that the problem would be easy, if the induction principle were given. This again - as in the previous point - requires explicit knowledge of this principle. If somebody doesn't know the induction principle he/she has almost no chance to invent the trick.
• Thirdly, the insight that with induction the problem would be simple gives some chance to speculate the idea to prove the theorem in the form of assumed reasoning of the type: " assume we had an induction principle for a particular number, then we could prove a particular statement. Since we don't have it, we assume it by a predicate N, which is defined by a comprehension axiom." This is certainly a very sophisticated reasoning step, and to our knowledge no system currently available is able to do it. The attempts to lemma speculation are all much more direct and the lemma speculated is the one that is needed to continue search.
• Fourthly, the way how the comprehension axioms are formed in the proof is quite systematic and they are closely related to the problem. It would be necessary to follow a similar line of systematic exploration.
• Fifthly the problem will remain difficult even if the questions above are answered, since on the one hand a new approach with defining new concepts has to be applied, and on the other hand it has to be applied not only once, but several times. This is a significant problem, since typically it is not so clear in an automated theorem prover whether it makes progress towards a solution. In some way in Boolos' proof it seems to be very clear that there is progress towards a proof, since the formulae to be shown in the sub-statements are getting smaller. Automated theorem provers would need an introspection capability and some better - more high-level - criterion for progress.

5.1.  How to find a solution?

• Firstly, it is clear that we need pretty high-level reasoning. Proof planning (as introduced by Bundy [Bundy88]) is such a high-level form of reasoning. It would be necessary to build high-level methods which can address the type of problem we try to address.
• Proof planning links in with a different observation from above, namely that a lot of knowledge is necessary to attack the problem successfully. Unfortunately, most systems seem not to benefit from big amounts of data, but get confused, since they can't see the wood for the trees. A better way to structure knowledge bases seem to be an issue to address here.

• We already pointed to the importance of reflection. An experienced deductionist would certainly derive in an initial problem analysis the insight that monotonous modus ponens applications will not be successful here while an unexperienced person would reflect on the unsuccessful object level proof attempts in order to come up with a similar conclusion soon later. It thus could be sensible to develop theorem provers which not only construct proofs or proof plans at object level but in parallel also reflect on their object-level proof search in order to built up a kind of meta-level understanding for the problem at run time. Proof critics as discussed in [IreBun:puofiip95] can be seen as a first step in this direction. Combined with an agent-based framework as discussed in [benzmueller01] respective proof critical agents could work in parallel with the proof agents on object level.
• Another very important issue is to study re-representation in detail, that is, not to work with the problem as it is, but to restructure it first. Pólya gave the advise [Polya62, vol.2, p.80]: " Of course you want to restate the problem (transform it into an equivalent problem) so that it becomes more familiar, more attractive, more accessible, more promising.". McCarthy put up the mutilated checkerboard problem and its reformulations as a challenge problem [McCarthy64].
• Selecting useful comprehension axioms is the same question as to form interesting concepts as done in Colton's work [Colton00]. For that reason it would be interesting to study how the work on concept formation can be integrated into a theorem proving framework.
• Human mathematicians are strongly guided in their proof search by models. It may be worthwhile to study how the selection process of suitable comprehension axioms can be guided by semantic, model-based techniques [Kerber94-CADE-WS-Model].

6.  Conclusion

Therefore we think that Boolos example will remain a very challenging problem for automation for the foreseeable future. Because of its perspicuity it is however well suited to speculate and investigate what kind of mechanisms (such as abstraction and reflection) will be required to fruitfully tackle it.

References

• [andrews00:systemdescr] Peter B. Andrews, Matthew Bishop, and Chad E. Brown. System description: Tps: A theorem proving system for type theory. In David A. McAllester, editor, Proceedings of 17th International Conference on Automated Deduction, volume 1831 of LNCS, pages 164-169. Springer, June 2000.

• [andrews:tatpsfctt96] Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and Hongwei Xi. TPS: A theorem proving system for classical type theory. Journal of Automated Reasoning, 16(3):321-353, 1996.

• [Andrews71] Peter B. Andrews. Resolution in type theory. Journal of Symbolic Logic, 3(36):414-432, 1971.

• [Andrews72] Peter B. Andrews. General models and extensionality. Journal of Symbolic Logic, 37(2):395-397, 1972.

• [Andrews72b] Peter B. Andrews. General models, descriptions, and choice in type theory. Journal of Symbolic Logic, 37(2):385-394, 1972.

• [Andrews86] Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, 1986.

• [Andrews:ocahol89] Peter B. Andrews. On Connections and Higher Order Logic. Journal of Automated Reasoning, 5:257-291, 1989.

• [Barendregt84] Hendrik P. Barendregt. The Lambda Calculus - Its Syntax and Semantics. North Holland, 1984.

• [BenzmuellerEtAl:otama97] C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier, W. Schaarschmidt, J. Siekmann, and V. Sorge. Omega Mega: Towards a mathematical assistant. In William McCune, editor, Proceedings of the 14th Conference on Automated Deduction, LNAI, Townsville, Australia, 1997. Springer Verlag.

• [benzmueller01:compar] C. Benzmüller. Comparing approaches to resolution based higher-order theorem proving. Synthese, An International Journal for Epistemology, Methodology and Philosophy of Science, 129, 2001. To appear.

• [benzmueller01] C. Benzmüller, Mateja Jamnik, Manfred Kerber, and Volker Sorge. An agent based approach to reasoning. KI-2001, 2001. To appear.

• [BenKoh:ehor98] C. Benzmüller and M. Kohlhase. Extensional higher-order resolution. In Kirchner and Kirchner [CADE98].

• [BeKo:LAHOTP98] C. Benzmüller and M. Kohlhase. Leo - a higher-order theorem prover. In Kirchner and Kirchner [CADE98].

• [boolos98:logiclogicandlogic] George Boolos. Logic, Logic, And Logic. Harvard University Press, 1998.

• [Bundy88] Alan Bundy. The use of explicit plans to guide inductive proofs. In Ewing Lusk and Ross Overbeek, editors, Proceedings of the 9th CADE, pages 111-120, Argonne, Illinois, USA, 1988. Springer, LNCS 310.

• [Constable86] Robert L. Constable, S. Allen, H. Bromly, W. Cleaveland, J. Cremer, R. Harper, D. Howe, T. Knoblock, N. Mendler, P. Panangaden, J. Sasaki, and S. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.

• [Colton00] Simon Colton, Alan Bundy, and Toby Walsh. Automatic invention of integer sequences. In Henry Kautz and Bruce Porter, editors, AAAI-2000, Austin, Texas, USA, 2000. AAAI Press, MIT Press.

• [CoqMan95] C. Cornes, J. Courant, J.-C. Filliâtre, G. Huet, P. Manoury, C. Mu noz, C. Murthy, C. Parent, Ch. Paulin-Mohring, A. Saibi, and B. Werner. The Coq proof assistant reference manual, version 5.10. rapport technique 177, INRIA, July 1995.

• [Church40] Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56-68, 1940.

• [Goedel36] Kurt Gödel. über die Länge von Beweisen. Ergebnisse eines mathematischen Kolloquiums, 7:23-24, 1936.

• [Gordon85] Mike Gordon. HOL: a machine oriented formulation of higher-order logic. Technical Report 68, University of Cambridge, Computer Laboratory, July 1985.

• [Henkin50] Leon Henkin. Completeness in the theory of types. Journal of Symbolic Logic, 15(2):81-91, 1950.

• [Huet72] Gérard P. Huet. Constrained Resolution: A Complete Method for Higher Order Logic. PhD thesis, Case Western Reserve University, 1972.

• [Huet73b] Gérard P. Huet. A mechanization of type theory. In Proceedings of the Third International Joint Conference on Artificial Intelligence, pages 139-146, 1973.

• [Huet75] Gérard P. Huet. An unification algorithm for typed lambda -calculus. Theoretical Computer Science, 1:27-57, 1975.

• [IreBun:puofiip95] Andrew Ireland and Alan Bundy. Productive use of failure in inductive proof. Special Issue of the Journal of Automated Reasoning, 16(1-2):79-111, 1995.

• [JePi72] D. C. Jensen and Thomasz Pietrzykowski. A complete mechanization of (Omega )-order type theory. In Proceedings of the ACM annual Conference, volume 1, pages 82-92, 1972.

• [Kerber94-CADE-WS-Model] Manfred Kerber. How to use a first-order model generator for adjusting problem formulations of higher-order logic. In Ricardo Caferra, Chris Fermüller, Alex Leitsch, and Tanel Tammet, editors, Proceedings of the CADE-Workshop on Automated Model Building, pages 22-25, Nancy, France, 1994.

• [Kerber94-ECAI] Manfred Kerber. On the translation of higher-order problems into first-order logic. In Tony Cohn, editor, Proceedings of the 11th ECAI, pages 145-149, Amsterdam, The Netherlands, August 1994. John Wiley & Sons, Chichester, England.

• [CADE98] C. Kirchner and H. Kirchner, editors. Proceedings of the 15th Conference on Automated Deduction, number 1421 in LNAI, Lindau, Germany, 1998. Springer Verlag.

• [luo92:legoproofdevelsystem] Z. Luo and R. Pollack. Lego proof development system: User's manual. Technical report, Department of Computer Science, Edinburgh University, 1992.

• [McCarthy64] John McCarthy. A tough nut for proof procedures. AI Project Memo 16, Stanford University, Stanford, California, USA, 1964.

• [McCune97] William McCune. Solution of the Robbins problems. Journal of Automated Reasoning, 19(3):263-276, 1997. see also http://www.mcs.anl.gov/home/mccune/ar/robbins/.

• [Martin-Loef84] Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.

• [OwRu92] S. Owre, J. M. Rushby, and N. Shankar. PVS: a prototype verification system. In D. Kapur, editor, Proceedings of the 11th Conference on Automated Deduction, volume 607 of LNCS, pages 748-752, Saratoga Spings, NY, USA, 1992. Springer Verlag.

• [Polya62] George Pólya. Mathematical Discovery - On Understanding, Learning, and Teaching Problem Solving. Princeton University Press, Princeton, New Jersey, USA, 1962/1965.

• [CADE98*129] Julian Richardson, Alan Smaill, and Ian Green. Proof planning in higher-order logic with lambdaclam. In Kirchner and Kirchner [CADE98], pages 129-133.

• [Russell02] Bertrand Russell. Letter to Frege. Printed in [vanHeijenoort67], 1902.

• [Russell03] Bertrand Russell. The principles of mathematics. Cambridge University Press, Cambridge, England, 1903.

• [Russell08] Bertrand Russell. Mathematical logic as based on the theory of types. American Journal of Mathematics, XXX:222-262, 1908.

• [vanHeijenoort67] Jean van Heijenoort. From Frege to Gödel : a source book in mathematical logic 1879-1931. Source books in the history of the sciences series. Harvard University Press, Cambridge, MA, USA, 3rd printing, 1997 edition, 1967.

• [Wolfram93] David A. Wolfram. The Clausal Theory of Types. Cambridge University Press, 1993.