Content deleted Content added
AshtonBenson (talk | contribs) |
AshtonBenson (talk | contribs) |
||
Line 155:
:"Tait in his 1981 paper argued that Hilbert's finitism is formalized by PRA. This conclusion is widely accepted in the f.o.m. literature. I certainly accept it..."
There are many more references than this; the relationship between PRA and finitism has been thoroughly explored in the literature. — Carl <small>([[User:CBM|CBM]] · [[User talk:CBM|talk]])</small> 01:13, 28 August 2009 (UTC)
:: Uh, just as a side note, I don't know if I'd count the FOMlist as a reliable source ;) [[User:AshtonBenson|AshtonBenson]] ([[User talk:AshtonBenson|talk]]) 04:09, 28 August 2009 (UTC)
:I guess I don't understand Astonbenson's notion of "notable", or "important". The following is certainly ''historically'' important. So I'll offer it up:
:Hilbert viewed "recursion" ("primitive", the only kind known at the time he gave his 1928) as the keystone of his formal, axiomatic theory of arithmetic. Hilbert (1926) had conjectured that there might be functions that could not be generated by [''primitive''] recursion, but Ackermann had not yet presented his (1928) novel "double-recursion", nor had Péter (1935) [reference: Kleene 1952:271]. So, Hilbert, in his 1927 ''The foundations of mathematics'' (van Heijenoort pp. 464ff) had only ''primitive'' recursion (based on Peano's successor and induction) at his disposal. He says "Finally, we also need ''explicit definitions'', . . . as well as certain ''recursion axioms'', which result from a general recursion schema. . . . For in my theory contentual inference is replaced by manipulation of signs according to rules; '''in this way the axiomatic method attains that reliability and perfection that it can and must reach if it is to become the basic instrument of all theoretical research'''."(boldface added, p. 467) He goes on about a page later to define what he means by "recursion" (nothing surprising -- the previous calculation is employed in generating the next calculation see p. 468), and after that, he states "In a corresponding way, the recursion axioms are formula systems that are modeled upon the recursive procedure. ¶ These are the general foundations of my theory. To familiarize you with the way in which it is applied I would like to adduce some examples of particular functions as they are defined by recursion." (p. 469) Here he offers examples of simple recursions starting with ι(0)=0; ι(a')=1, [etc].
:: I think this strongly supports my point. Had Ackermann's function been known at the time, we probably would have wound up with some class of functions which includes it (and is closed under composition) as our most-notable class of "obviously" terminating functions (termination being obvious because the termination proof can proceed by induction on the recursive procedure for enumerating all the functions in the class). And in fact I bet we'd call them "the primitive recursive functions." Point being, that name and the notability that goes with it was given to the first-to-be-discovered "large" subset of the total recursive functions which was itself RE. [[User:AshtonBenson|AshtonBenson]] ([[User talk:AshtonBenson|talk]]) 04:09, 28 August 2009 (UTC)
:To sum up, "primitive" recursion provided "the general foundations" of Hilbert's theory that was to be used, in essence, by Goedel a few years later. "Full" recursion was not the driver, "primitive" recursion was. Kleene notes that the formal system ''he'' (Kleene) presents (essentially that used by Goedel 1931) "has function symbols only for the three functions ', +, *. ... This proof [Goedel's "Theorem VII: Every [primitive] recursive relation is arithmetic[al]"] is not essential to our program of formalizing number theory. If it did not succeed, we could have arranged instead that recursion equations for other functions besides + and * should be axioms of the system. ... '''However, it is of some interest that a finite system suffices, the more so that we can get along with the two chief functions + and * of traditional arithmetic, when taken with the logical constants and the predicate =.'''" (boldface added, Kleene 1952:239). Bill [[User:Wvbailey|Wvbailey]] ([[User talk:Wvbailey|talk]]) 02:53, 28 August 2009 (UTC)
| |||