Peano ArithmeticPeano arithmetic is a well-known aiomatization of the natural numbers. There is a constant 0, a function symbol s for the successor or next-integer function. We would intuitively think of s(x) as x+1, but in the Peano axioms, s is fundamental, and is used to defined addition, so successor is not defined in terms of addition. The principle axioms about successor say that it is a one-one function that never takes the value 0. These axoms guarantee that all models of these axioms (including the natural numbers) are infinite; one definition of an infinite set is one that can be mapped one-to-one onto a proper subset. Multiplication is defined in terms of addition. The axioms mentioned so far are listed as follows in clausal form: s(x) != 0. Peano's great insight was that these axioms, plus the principle of mathematical induction, are enough to characterize the natural numbers. The principle of mathematical induction is as follows: if P(0) and for all natural numbers n, P(x) implies P(s(x)), then for all natural numbers z, P(z). What is P in this formula? There are several possible answers to that question, which we will take up in turn. (1) P stands for any formula in the first-order language of 0,s,+, and *. This makes induction an axiom schema (an infinite set of axioms of a certain form) instead of a single axiom. The result first-order theory is usually called PA. (2) P could stand for any formula in a larger first order language. This might be a language in which the variables all range over natural numbers (for instance, we might augment the language with < and > and symbols for other functions, like factorial and exponentiation). Or, it might be a language in which some of the variables are meant to range over sets. Logicians sometimes use "multi-sorted" theories with different kinds of variables, or sometimes they use unary predicates to "relativize" or "restrict" some variables to range only over natural numbers. (3) In a theory that can speak of sets, P might just be taken to be the formula x ε X, where X is a set variable. Then induction becomes a single axiom, but how strong it is then depends on the set existence axioms that are also included. (4) We might interpret P to stand for an arbitrary predicate on the natural numbers. (A predicate is a boolean-valued function.) This is more or less the same as saying P is interpreted to stand for membership in an arbitrary set, since every set of natural numbers determines a predicate and vice-versa. This is the most natural interpretation of induction, but its full meaning is not captured by any of the first-order versions listed above. Computers cannot work with "arbitrary" predicates, but only with predicates defined by some finite term in some language. (5) We can formulate induction in lambda logic if we take P(x) to be Ap(y,x), where y is a variable. Then y will range over all predicates of natural numbers, so we do not need an axioms schema to express induction. A single axiom will be enough. Of course, just as in the set-theoretic interpretation, how strong this is in practice depends on what axioms we add to construct predicates. It is this formulation of arithmetic in lambda logic that concerns us. We have formalized a number of theorems of Peano Arithmetic using Otter-λ, and we now want to discuss the formalization we use. The first step is to express induction in clausal form. This is a step that has nothing to do with lambda logic; one can carry it out in first-order logic, assuming P is a predicate symbol. We therefore simply give the result here; those who want to see how it is done or review how it connects with our usual way of looking at induction, can click the link.
-Ap(z,0) | Ap(y,g(y))) | Ap(y,z). Peano Arithmetic and Typing We do not, in our input files, use a unary predicate N(x) to relativize the axioms of Peano arithmetic. One may worry, then, that we are not studying arithmetic, but a theory whose models are simultaneously models of the lambda calculus and the Peano axioms. We do not want to put a unary predicate N(x) into our files, because it will slow down or possibly prevent the discovery of proofs. Instead, we appeal to implicit typing. You should have already read the two essays on implicit typing:
implicit and explicit typing Here is a beta-correct, lambda-coherent, list of type specifications, lambda-complete with respect to the axioms listed above: list(types).
It follows from the theorems on implicit typing that if we supply a correctly typed negated goal, and Otter-λ finds a proof, then the proof can be correctly typed, and hence can be expressed as a proof in the theory in which the "natural-number variables" in the Peano axioms are relativized to a unary predicate N(x). Only the variable y in the two induction clauses is not a "natural-number variable". Once the variable y has been instantiated, as it will be when Otter-λ finds a proof, the corresponding instance of induction can be expressed in PA. For example, when proving the associativity of addition, y will get instantiated to lambda(x,a+x=x+a), which corresponds to taking P(x) to be a+x=x+a in the PA version of induction. Hence, proofs found by Otter-λ using the untyped axioms listed above do indeed necessarily translate to proofs in PA. Just as in the group theory example discussed in the essay implicit and explicit typing with lambda unification, the axiom system listed above is contradictory in lambda logic, because like every other function, successor has a fixed point. We can prove the existence of some constant c such that s(c) = c. But on the other hand, we can prove by induction that for all x, s(x) != x: the basis case s(0) != 0 is an axiom, and for the induction step, if s(s(n)) = s(n), then since successor is one-to-one, s(n) = n, contradicting the induction hypothesis. But, as explained op.cit. for the group theory example, all is well, because Otter-λ will not find the fixed-point construction from correctly typed axioms, and indeed from correctly typed axioms it will find proofs that can be translated into PA. This is not just an empirical fact, it is a theoretical consequence of our theorems on implicit typing.
|