^{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 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 x. P[x] is equivalent to the existence of some terms t_{i}
with P[t_{1}] ... P[t_{n}] 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
'{*http://math.uw.bialystok.pl/~Form.Math/*

^{26} For example, the derivative of f(x) =
x^{2} sin(1 / x^{2}) (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
** http://saxon.pip.com.pl/MathUniversalis/contents.html**.