
Re: Devlin adn Recursion
Posted:
Nov 28, 2011 3:09 PM


Dave L. Renfro wrote (in part):
http://mathforum.org/kb/message.jspa?messageID=7616654
> I'll look through some of my stuff at home (where I'm > leaving for right after posting this) this weekend and > try to come up a better understanding of whether this is > something relevant for, say, a rigorous treatment of real > analysis in which the Peano axioms are dealt with, or only > relevant in hardcore mathematical logic and set theory work.
I looked at some things yesterday, but rather than answer the question I raised, I'll just toss out some of what I found.
******************************************************* *******************************************************
Abraham A. Fraenkel, "Abstract Set Theory", 2nd edition, 1961.
>From a footnote on p. 180:
The definitions of addition and of other operations were for the first time strictly based [for the first time rigorously established] in Dedekind 1888 [...] Peano's procedure (from 1889 on, cf. Peano 1895) is not sufficient as long as it is not supplemented by a new primitive symbol for addition or by an appropriate rule of inference; othewise one has, as here in Theorem 7, to prove that _a_function_exists_ which satisfies Peano's recursive definition.
Among the references that Franekel then provides are the following two: A. Church, [review of a book], Journal of Symbolic Logic 17 (1952), 199200; Beth, "The Foundations of Mathematics", 1959, chapter 6.
******************************************************* *******************************************************
Ivor GrattanGuinness, "The Search for Mathematical Roots. 18701940", 2000.
>From p. 106:
To found arithmetic suitably Dedekind treated mathematical induction with a new level of sophistication. [...] It legitimated inductive _proofs_ in arithmetic by providing a justification for inductive _definitions_; for it guaranteed the existence of a means by which [...] Despite all the concern with the foundations of arithmetic in the succeeding decades, the profundity of this section of Dedekind's booklet [1888] was not appreciated. [footnote] The classic location for an appreciation of Dedekind's treatment of inductive definitions is the textbooks on foundations of analysis by Edmund Landau (1930a, preface and ch. 1), where he acknowledged an idea by Laszlo Kalmar. However, he [Landau] made the point already in his obituary of Dedekind, in a version for which he thanked Zermelo (Landau 1917a, 5657). [Nachrichten der Königlichen Gesellschaft der Wissenschaften zu Göttingen, Geschäftliche Mitteilungen, pp. 5070.]
******************************************************* *******************************************************
Leon Henkin, "On mathematical induction", American Mathematical Monthly 67 #4 (April 1960), 323338.
Near top of p. 328:
We may phrase this observation by saying that the _axiom_ of mathematical induction does not itself justify _definitions_ by mathematical induction. [footnote] This fact was clearly brought out by Dedekind in his famous book: Was sind und was sollen die Zahlen? (See "Bemerkung," paragraph 130, section 9.)
>From p. 338 (last paragraph of the paper):
While the method of presenting the material in this paper may have some claim to originality, several of the proofs which were given are well known to mathematicians. In particular, this is true of the two proofs (one given in detail, the other outlined) of Theorem I. According to Professor Alonzo Church, the origin of the first proof goes back to the Hungarian mathematician L. Kalmar, while the idea of the second proof should be credited to P. Lorenzen, and D. Hilbert and P. Bernays, who discovered the proof independently and published their work nearly simultaneously. The proof of Theorem II is given by E. Landau who credits it to L. Kalmar. However, Landau fails to note the significance of the fact that the proof does not use Axioms P1 and P2.
******************************************************* *******************************************************
Two of the most detailed _mathematical_references_ I was able to find are Enderton's book (his set theory book, not his logic book I mentioned previously in this thread) and Hrbacek/Jech's book. Each gives a careful discussion of the existence proof.
Herbert B. Enderton, "Elements of Set Theory", 1977.
See pp. 7078. A section titled "Digression" on p. 76 begins with the following sentence: "There is a classic erroneous proof of the recursion theorem that people have sometimes tried (even in print!) to give."
Karel Hrbacek and Thomas Jech, "Introduction to Set Theory", 3rd edition, 1999.
See Sections 3.33.4 (pp. 4655).
>From p. 47 of Hrbacek/Jech. (Recall that a sequence in a set X is, mathematically, a function from the set of natural numbers into the set X.)
(a) The sequence s: N > N is defined by
s_0 = 1; s_{n+1} = n^2 for all n [belonging to] N.
(b) The sequence f: N > N is defined by
f_0 = 1; f_{n+1} = f_n x (n+1) for all n [belonging to] N.
The two definitions, in spite of superficial similarity, exhibit a crucial difference. The definition of s gives _explicit_ instructions how to compute s_x for any x [belonging to] N. More precisely, it enables us to formulate a property P such that
s_x = y if and only if P(x,y);
namely, let P be "either x = 0 and y = 1 or, for some n [belonging to] N, x = n + 1 and y = n^2." The existence and uniqueness of a sequence s satisfying (a) then immediately follows from our axioms:
s = {(x,y) [belonging to] N x N  P(x,y)}.
In contrast, the instructions supplied by the definition of f tell us only how to compute f_x _provided_ that the value of f for some smaller number (namely, x  1) was already computed. It is not immediately obvious how to formulate a property P, not involving the function f being defined, such that
f_x = y if and only if P(x,y).
We might view the definition (b) as giving _conditions_ the sequence f ought to satisfy: "f is a function on N to N which satisfies the 'initial condition': f_0 = 1, and the 'recursive condition': for all n [belonging to] N, f_{n+1} = f_n x (n + 1)." Such definitions are widely used in mathematics; the reader might wish to draw a parallel, e.g., with the implicit definitions of functions in calculus. However, a definition of this kind is justified only if it is possible to show that there exists some function satisfying the required conditions, and that there do not exist two or more such functions. In calculus, this is provided for by the Implicit Function Theorem. We now state and prove an analogous result for our situation. [They go on to state and prove "The Recursion Theorem".]
******************************************************* *******************************************************
Each of the following book reviews by Reuben Louis Goodstein (19121985) gives some worthwhile comments about these issues, for those who want to keep digging into this topic.
Review of A. A. Fraenkel "Abstract Set Theory", Mathematical Gazette 38 #323 (February 1954), 5455.
Review of J. B. Rosser "Logic for Mathematicians", Mathematical Gazette 38 #325 (September 1954), 224227.
Review of H. A. Thurston "The Number System", Mathematical Gazette 41 #336 (May 1957), 158159.
Review of B. K. Youse "The Number System", Mathematical Gazette 50 #374 (December 1966), 436437.
******************************************************* *******************************************************
Here's a proof of existence. It's not the general recursion theorem result proved in Enderton and Hrbacek/Jech (cited above), but rather it's specifically written for the special case of addition in PA.
Let S be the successor function and N be the set of positive integers. For better readability, instead of S(2) and S(S(g(3))) I'll write S2 and SSg(3). Let E be the set of positive integers n such that there exists (no claim of uniqueness being made) a function f_n: N > N such that
(a) f_n(1) = Sn
(b) f_n(Sk) = Sf_n(k) for each k = 1, 2, 3, ...
We prove that E = N by induction. To this end we will prove that 1 belongs to E and, if n belongs to E then Sn belongs to E.
[[ proof that 1 belongs to E ]]
Define f_1 = S. Then (a) and (b) are readily verified. (The verifications are easy, but there is something to be done, namely prove the above equations hold when n = 1 and f_1 = S.)
[[ proof that n belongs to E implies Sn belongs to E ]]
Since n belongs to E (induction hypothesis), there exists (at least one) function f_n that satisfies (a) and (b) above. Let f_{Sn} = Sf_n (composition of S and f_n, with f_n being taken first).
proof that (a) holds for f_{Sn}:
f_{Sn}(1) = Sf_n(1) [definition of f_{Sn}]
= SSn [induction hypothesis: (a) holds for f_n]
Note that we've shown f_j(1) = Sj for j = Sn, so we've shown that (a) holds for f_{Sn}.
proof that (b) holds for f_{Sn}:
Let k be any (fixed choice of a) positive integer. Then
f_{Sn}(Sk) = Sf_n(Sk) [definition of f_{Sn}]
= SSf_n(k) [induction hypothesis: (b) holds for f_n, so f_nS = Sf_n]
= Sf_{Sn}(k) [definition of f_{Sn}]
Note that we've shown f_j(Sk) = Sf_j(k) for j = Sn, so we've shown that (b) holds for f_{Sn}.
Now define m + n to be the value of f_n(m).
Now check (easy) that + is defined on all pairs of natural numbers and we have the property (m,n) = (m',n') implies m + n = m' + n'.
******************************************************* *******************************************************
Dave L. Renfro

