Formalised Mathematics - footnotes

1 There are still qualms over the fact that the proof relied on computer checking of cases. We distinguish sharply between ad hoc checking programs like this and the kind of use we propose of computers to prove theorems in a formal deductive calculus.

2 For example, the Z specification language [spivey-understanding], which has been around for many years, is really only now becoming formal in our sense, as a standardization effort clears up ambiguities in its semantics. Indeed, the book just cited discusses four different semantics for 'undefined' expressions.

3 By contrast, some early proofs of the Fundamental Theorem of Algebra, for example, leave some doubt over whether the simple geometric observations they use do in fact fit easily into a symbolic framework.

4 'Separation', or perhaps better 'picking-out' axiom.

5 Chapter V: Of Reason, and Science. 'For as Arithmeticians teach to adde and subtract in numbers [...] The Logicians teach the same in consequences of words [...] And as in Arithmetique, unpractised men must, and Professors themselves may often erre, and cast up false; so also in any other subject of Reasoning the ablest, most attentive, and most practised men, may deceive themselves, and inferre false conclusions.'

6 Frege remarked that 'the comfort of the typesetter is certainly not the summum bonum'.

7 There are related systems, e.g. Quine's NF and ML, presented formally by [rosser-ml], which can prove the Axiom of Infinity, yet are not known to be inconsistent. However precisely because of the perverse way in which infinity is deduced (the Axiom of Choice fails) these are widely distrusted.

8 'I have been ever since definitely less capable of dealing with difficult abstractions than I was before'.

9 For a more detailed discussion of Hilbert's programme, we recommend the penetrating analysis by [kreisel-hilbert].

10 This would amount to a realization of Leibniz's dream, at least if it is restricted to mathematics.

11 True to the practices of informal mathematics that we spend so much energy berating, we shall not state precisely the conditions on a system for Gödel's theorem to apply, and shall sometimes take it for granted later that we are discussing such a formal system, and that it is consistent. This is a reasonable practical assumption.

12 Roughly speaking, a predicate that can be calculated (by proof if need be) for each specific allocation of numeric arguments --- this corresponds to the fact that a 'formal system' must allow an unambiguous algorithmic way of checking whether a purported proof is valid.

13 Though it does refute the stronger form that all these theorems should be provable in a fixed finitistic system. Hilbert's precise agenda was never clear; at first he presented consistency as the objective per se.

14 It seems bizarre to accept P as meaningful while dismissing not P as meaningless. However there is some Popperian justification for this, since a universal statement is refutable by calculation. Anyway, Hilbert's views varied over time and were not always clear, so a detailed exegesis is difficult. Certainly it's necessary to accept universal formulas as meaningful since an assertion of consistency is itself of this form.

15 Later editions included the Axiom of Replacement, giving something closer to ZFC. The author is not sure whether this axiom has ever been used in Bourbaki.

16 This does however suggest the interesting research problem of systematically using non-formal reasoning to obtain new results; perhaps Gödel's theorems indicate that in our reliance on the axiomatic method we're failing to exercise the full potential of our mathematical faculties!

17 However mathematicians are expected to acquire facility at certain kinds of formal manipulations as part of their training, so perhaps the apparent greater difficulty presented by logical formalism is just a question of its familiarity.

18 This apt label is from [mackenzie-proof].

19 The similarity or otherwise of formal proofs to conventional ones, and whether they should really be called 'proofs' at all, have no direct consequences as regards their objective value or persuasive power. Similarly, questions about whether a machine can 'think' have no direct relevance to whether a particular computer program can beat one at chess.

20 For many proof procedures, the proof-theoretic details of Gentzen's results are not really relevant; all that is required is that the provability of existsx. P[x] is equivalent to the existence of some terms ti with P[t1] or ... or P[tn] provable. This result (which together with an explicit construction is essentially Herbrand's theorem) is an easy consequence of Gentzen's Hauptsatz, but it can be derived purely model-theoretically; [kreisel-krivine] give a particularly elegant proof of what they pointedly call the 'uniformity theorem'.

21 See footnote 11 of Prawitz's paper for a bit more detail on the genesis of the idea.

22 Herbrand's thesis (1930) contains what is effectively a unification algorithm. Prawitz's procedure already mentioned also used unification, but since his logic had no function symbols, it was only a special case. Davis apparently used full unification in a proof procedure in 1962, influenced by Prawitz.

23 At an abstract level, viewing clauses as sets (not multisets) of literals, unification is complete without considering factoring. However in proof search, it is necessary to consider it since duplications only appear when the right instantiations are found.

24 Independently discovered by de Bruijn.

25 For more information about this journal, which is surprisingly inexpensive, contact: Fondation Philippe le Hodey, Mizar Users Group, Av. F. Roosevelt 134 (Bte7), 1050 Brussels, Belgium, fax +32 (2) 640 89 68. Also available on the Web from '{

26 For example, the derivative of f(x) = x2 sin(1 / x2) (with f(0) = 0) is Darboux continuous, as are all derivatives, but it is not continuous at x = 0, nor in fact even Lebesgue integrable over any interval including 0.

27 This approach was independently arrived at by the present author and used in the standard library of wellorderings in the HOL system.

28 Zermelo didn't want to do truly formal reasoning, merely to make set-theoretic assumptions explicit.

29 At least in the sense of constructive logic; classical reasoning about algorithms is not the same thing.

30 Described in his Northeastern University notes, which as far as we know remain unpublished.

31 Note that the systems of the pioneers like Frege and Peano were clearly higher order. For example, the basic Peano axioms for natural number arithmetic which Peano took from [dedekind-was] and formalized, give in first order logic only a trivial decidable theory --- it's necessary to include addition and multiplication as primitive to get anything really interesting. Actually Peano used a principle of primitive recursive definition, but did not justify it or even state it explicitly. In this respect his development of arithmetic from the axioms, though formal, represented a big step backwards in rigour from Dedekind.

32 The Axiom of Foundation was not added for this reason --- of course one doesn't make a system consistent by adding an axiom! Rather, it was deemed 'true' of the universe of mathematical sets, or at least a valid simplifying assumption.

33 Even intuitionistically, implication and universal quantification are enough to define all the usual connectives, whereas in first order logic they are all independent except for negation --- see [prawitz-book].

34 Although among computer scientists the opposite is probably true.

35 This asserts that every set is contained in a universe set, i.e. a set closed under the usual generative principles. It was introduced by [tarski-grothendieck], and subsequently popularized by Grothendieck in the 60s --- SGA 4 [grothendieck-sga4] has an appendix on this topic attributed to 'N. Bourbaki'.

36 Though it streamlines some parts of pure set theory: every woset is isomorphic to a von Neumann ordinal, recursion is admissible on a wellfounded class-relation etc.

37 Section III.§3.1, 'The cardinal of a set', footnote.

38 Which is what the original LCF (Logic of Computable Functions) logic did.

39 In a reasonable logic f, being recursive, will be representable, though in general only by a predicate rather than a function.

40 There is also a misunderstanding of terminology outside the LCF community. A tactic, as described by [gordon-lcfbook], is a specific way of supporting backward proof in terms of forward proof; a tactical is a higher order function for combining tactics. In some quarters today the decomposition to primitives is supposed to be the distinguishing feature of a 'tactic'. But this decomposition, which we focus on here, is a separate issue; rather than obliterate the original meaning of 'tactic', we will refer to 'derived rules' without greatly concerning ourselves whether they work forward or backward.

41 We are uncomfortably aware that this resembles the argument that various political systems are good in principle, but merely badly implemented in practice! By the way, [slind-thesis] has remarked that in LCF 'the user controls the means of (theorem) production'.

42 Probably his motivation was more theoretical than practical; it shows that primality testing is in NP as well as co-NP.

43 Some writers use this notion for a Hilbert-style proof system. In that case the definitions are slightly different. Thanks to Seán Matthews and Randy Pollack for discussion of this point.

44 Note that the formalized provability is for the original system, without the reflection rule. Care is needed if instances of the reflection rule are to be nested. Two different approaches are discussed by [knoblock-constable] and by [allen-reflected].

45 By Tarski's theorem we can't actually have a predicate representing truth, but the above axioms say something intuitively close.

46 One may say that the ML programming language is the metalogic of LCF systems, but a peculiarly limited or ultra-constructive one where the only way of proving something exists is to produce it explicitly.

47 The author has been told that an attempt was made to verify in Nuprl the correctness of a Presburger arithmetic implementation, but the researcher involved eventually became discouraged by the difficulty of the proofs.

48 It has been remarked that computer scientists would rather use each other's toothbrushes than each other's notation.

49 The artificial language Interlingua (aka ' latino sine flexione') was, by the way, invented by Peano, whose interest in new languages was not restricted to the mathematical field. Unfortunately, the fact that the few informal parts of his formalized mathematics was written in latino sine flexione must have contributed to their limited impact.

50 And apropos of Halmos's sceptical view of logical symbolism, the author has heard chess players use the Informator abbreviations in conversation, e.g. 'triangle' instead of 'with the idea'.

51 Experience Not Only Doctrine.

52 See

home John Harrison 1996/8/13; HTML by 1996/8/16