Timeline for Was "arithmetical translation" (coding in the Goedel sense) ever a part of Hilbert's Program?
Current License: CC BY-SA 3.0
28 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 26, 2022 at 15:08 | comment | added | Thomas Benjamin | @TimothyChow: Having time to reflect on your comment, I heartily concur. Thanks. | |
| Feb 10, 2016 at 17:15 | answer | added | Thomas Benjamin | timeline score: 0 | |
| Jan 29, 2016 at 12:48 | vote | accept | Thomas Benjamin | ||
| Jan 28, 2016 at 19:28 | answer | added | Thomas Benjamin | timeline score: 0 | |
| Nov 30, 2015 at 12:46 | comment | added | Thomas Benjamin | @AndreasBlass: Very helpful. Thanks. | |
| Nov 30, 2015 at 12:07 | comment | added | Andreas Blass | For example, the usual definition of the Ackermann function can easily be reformulated as a higher-type primitive recursion. I'd expect the type-0-to-type-0 functions obtainable in Gödel's system to be the same as those that are provably recursive in PA. | |
| Nov 30, 2015 at 12:05 | comment | added | Andreas Blass | The following is not guaranteed; I'm working from old memories. Gödel's Dialectica system has, at the lowest level, the natural numbers, not numerals, though I doubt it makes much difference. I don't recall there being any Gödel numbering in this paper, but if there is then I'd expect the Gödel numbers to be numbers, not another sort of entity. (That is, after all, one of the main points of Gödel numbering.) The primitive recursive functionals of finite type are that happen to map type 0 to type 0 not just the primitive recursive functions. (Continued in next comment) | |
| Nov 30, 2015 at 4:23 | comment | added | Thomas Benjamin | (cont.) over objects of type 0, what exactly makes these 'primitive recursive functionals' 'non-finitary' over 'higher-type objects', in Goedel's opinion? | |
| Nov 30, 2015 at 4:21 | comment | added | Thomas Benjamin | @AndreasBlass: Some questions regarding Goedel's primitive recursive functionals of finite types. 1. Are the numerals |, ||,|||,... objects of type 0? 2. Do Goedel's primitive recursive functionals reduce to the primitive recursive functions over objects of type 0? 3. Are the numerals |,||,|||,... construed as Goedel 'numerals' objects of the same type as the numerals |,||,|||,...? 4. If not, are the numerals construed as Goedel numerals different objects than the numerals themselves. 5. If Goedel's primitive recursive functionals reduce to the primitive recursive functions | |
| Nov 27, 2015 at 12:34 | comment | added | Andreas Blass | I can't imagine a genuinely higher-type system that would be finitary in Hilbert's sense, but one could view Gödel's Dialectica paper as an attempt in that direction. The title of that paper describes the higher type system there as an extension of the finitary position. (Of course, one could argue that all sorts of non-finitary things are extensions of finitism, but I think Gödel's intention was to suggest that he has not deviated too much from finitism, while conceding that his system is not strictly finitary.) | |
| Nov 27, 2015 at 12:33 | comment | added | Mauro ALLEGRANZA | I agree; I would have written "can be due to the reading of H ...". My suggestion is : the basis of arithmetization is to consider expressions, formulae, proof as finite sequences of symbols, i.e. finite "concrete" objects, like strokes. Thus, if primitive recursive arithmetic can treat "concrete" objects like numerals (i.e. finite strings of symbols), it can as well treat syntactical stuff. | |
| Nov 27, 2015 at 10:05 | comment | added | Thomas Benjamin | (cont.) Goedel's theorems). If one were to take footnote 48a seriously, one might look for finitary higher type methods (that could actually be recognized as finitary), and use these to produce Hilbert's desired consistency theorem (perhaps Goedel did this already). Any current higher-type recursion theory that might possibly qualify? | |
| Nov 27, 2015 at 9:59 | comment | added | Thomas Benjamin | (cont.) Ann. 95, p. 184), while, in every formal system, only countably many are available. Namely, one can show that the undecidable sentences which have been constructed here always become decidable through adjunction of sufficiently high types (e,g, of the type $\omega$ to the system $P$). A similar result holds for the axiom systems of set theory." This suggests to me, that, while arithmetization of finitary methods is certainly possible, it may be the same confusion of types that led to Russell's Paradox (though in the case of arithmetization it led to trhe happier result of | |
| Nov 27, 2015 at 9:43 | comment | added | Thomas Benjamin | (cont.) For the latter presupposes only the existence of a consistency proof carried out by finitary methods, and and it is conceivable that there might be finitary methods that cannot be represented in $P$ (or in $M$ or $A$)." What might these be? Goedel (I believe) gives us a clue in footnote 48a of the same paper: "The true reason for the incompleteness which attaches to all formal systems lies, as will be shown in Part II of this paper, in the fact that the formation of higher and higher types can be continued into the transfinite (cf. D. Hilbert, "Uber das Unendliche", Math. | |
| Nov 27, 2015 at 9:25 | comment | added | Thomas Benjamin | @AndreasBlass: The Goedel quote you refer to is contained in his paper "On Formally Undecidable Propositions of Principia Mathematica and Related Systems I " on page 37 of Martin Davis' book, The Undecidable. It reads as follows: "It should be expressly noted that Theorem XI (and the corresponding results about $M$ and $A$) [the second incompleteness theorem and that incompleteness theorem being applied to $M$ and $A$ ; $M$ being the systems of set theory and $A$ the system of classical mathematics --my comment] in no way contradicts Hilbert's formalistic standpoint. | |
| Nov 27, 2015 at 4:00 | comment | added | Thomas Benjamin | @MauroALLEGRANZA: Luckily for me a translation of "On the foundations of logic and arithmetic" (by Beverly Woodward) exists in van Heijenoort, and I have been reading through it (hopefully carefully enough). However, the notion that 'provability is an arithmetical relation' just does not jump out at me in his paper. In what way do you hold that the notion of provability being an arithmetical relation is due to its content? | |
| Nov 26, 2015 at 20:49 | comment | added | Timothy Chow | @ThomasBenjamin : Arithmetization does not give the 'meaningless formulae' meaning. At most, arithmetization gives numbers a new meaning; numbers now refer to certain strings of meaningless symbols. The symbols themselves remain meaningless. | |
| Nov 26, 2015 at 16:42 | comment | added | Andreas Blass | I've heard that the "much less" part of my previous comment, i.e., the observation that Hilbert's finitary reasoning can be formalized in second-order (or even first-order) arithmetic, was due not to Gödel but to von Neumann. Apparently Gödel originally said that his result doesn't destroy Hilbert's program, but I don't know whether that was really his opinion or just a very junior Gödel being polite to superstar Hilbert. | |
| Nov 26, 2015 at 16:39 | comment | added | Andreas Blass | As far as I know, what Hilbert wanted was to prove the consistency of strong systems (at least what we'd now call second-order arithmetic) by using very weak assumptions --- finitary reasoning about the combinatorial structure of statements in the strong system (ignoring any meaning those statements might have, or, better, pretending that they have no meaning). Gödel shot that idea down by showing that consistency of strong statements cannot be proved even in those strong systems, much less by finitary reasoning. | |
| Nov 26, 2015 at 14:32 | review | Close votes | |||
| Nov 27, 2015 at 0:03 | |||||
| Nov 26, 2015 at 14:30 | history | edited | David Roberts♦ | CC BY-SA 3.0 |
Added link to Bernays' paper
|
| Nov 26, 2015 at 13:59 | comment | added | Mauro ALLEGRANZA | ... It is possible that the seminal idea of proving that "provability [is] an arithmetical relation" can be due to Hilbert's paper On the foundations of logic and arithmetic (1904). | |
| Nov 26, 2015 at 13:56 | comment | added | Mauro ALLEGRANZA | I do not think that we can find a cite from Hilbert's writings stating that arithmetization (or any other form of coding) of some first-order theory in itself was a part of his program. But I suggest this "line of thought" : Godel's basic insight is that (letter to Balas, around 1970) : "(and this is the decisive point) it follows from the correct solution of the semantic paradoxes i.e., the fact that the concept of “truth” of the propositions of a language cannot be expressed in the same language, while provability (being an arithmetical relation) can. Hence true $\ne$ provable." ... 1/2 | |
| Nov 26, 2015 at 12:30 | comment | added | Thomas Benjamin | (cont.) replaced by manipulation of signs according to rules..." This from Stefen Bauer-Mengelberg's translation of Hilbert's "On the Infinite" from van Heijenoort, pg 381), wasn't that done because the mathematical community could agree that finitary rules and finitary methods were valid? | |
| Nov 26, 2015 at 12:21 | comment | added | Thomas Benjamin | @AndrejBauer: But that is the point of my question. Have we any justification to say that from Hilbert's writings on logic and foundations, of whatsoever nature, that "Goedel did exactly what Hilbert wanted" by arithmetizing the system? That would seem to imply that Hilbert expected there to be a self-verifying fragment of mathematics that the rest of mathematics could be proved consistent with. Is there any indication of this expectation in his writings? Also, regarding the treatment of formal systems as 'formula games' manipulated by 'finitary' rules ("hence contentual inference is | |
| Nov 26, 2015 at 11:01 | comment | added | Andrej Bauer | I suppose there is a conclusion to my remark: and so, Gödel did exactly what Hilbert wanted. He took the formal system, arithmetized it (thereby completely ignored the intended meaning of the symbols) and proved a neat result. It just happened to be a result not anticipated by Hilbert. | |
| Nov 26, 2015 at 10:59 | comment | added | Andrej Bauer | This is a bit of an off-remark, but I felt like saying it, I hope you can forgive me. As a mathematician I always read Hilbert's saying that "it is all a formal game" as a plan of attack on how to prove consistency: forget any semantics or meaningful content that a formal theory might carry and consider just the bare formalism – then analyse the formalism with combinatorial methods which pay no attention to the intended maning. As such, this is not a philosophical credo but rather a common mathematical technique known as "let's view thing from another angle". | |
| Nov 26, 2015 at 8:20 | history | asked | Thomas Benjamin | CC BY-SA 3.0 |