Timeline for Regarding Gentzen's note regarding 'Godel-points' (i.e., "Where is the Godel-point hiding?")
Current License: CC BY-SA 4.0
42 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 4, 2019 at 20:27 | answer | added | Thomas Benjamin | timeline score: 0 | |
| Oct 23, 2019 at 19:47 | comment | added | Noah Schweber | Whoops, my apologies: you quoted the theorem correctly and I misread it. There's a crucial distinction between primitive recursive function and primitive recursive functional, and I misread what you wrote. | |
| Oct 23, 2019 at 19:30 | comment | added | Thomas Benjamin | @NoahSchweber: Good Idea. I already did. | |
| Oct 23, 2019 at 2:19 | comment | added | Noah Schweber | Regardless, I still really don't get the point you're driving at re: your original question, and I think this is getting a bit far afield. Maybe it would be better treated in a separate question. | |
| Oct 23, 2019 at 2:18 | comment | added | Noah Schweber | I don't know enough about $T$ to say anything about it, but you've quoted the theorem incorrectly: the primitive recursive functions are the provably total functions of I$\Sigma_1$. PA can prove galactically more - e.g. PA proves that the Ackermann function is total - and indeed there is no snappy characterization of the PA-provably total functions (if there were, diagonalizing out of it would yield a simple combinatorial sentence independent of PA!). As to the relationship between ACA$_0^+$ and TA, ACA$_0^+$ proves "TA exists" in a precise sense - beyond that I don't know what you're asking. | |
| Oct 22, 2019 at 21:19 | comment | added | Thomas Benjamin | (cont.) makes sense, and if not, what would that subsystem of second-order arithmetic be)? (Note: there should be a quotation mark between the second $\mathbb N$ and the period in the previous comment.) | |
| Oct 22, 2019 at 21:14 | comment | added | Thomas Benjamin | @NoahSchweber: As regards $ACA^{+}_0$, since it is the system $RCA_0$ together with the statement that $\omega$th jumps exist, is there a relation between $ACA^{+}_0$ and True Arithmetic? As regards the Dialectica Interpretation, consider the following theorem, allegedly by Godel: "The provably total recursive functions of $PA$ are exactly the primitive recursive functionals of type $\mathbb N$ $\rightarrow$ $\mathbb N$. I guess the question for me would be, can $ACA_0$ interpret all of Godel's system $T$ and if not, what is the weakest strengthening of $ACA_0$ that can (provided that | |
| Oct 21, 2019 at 22:48 | comment | added | Noah Schweber | ATR$_0$ is massive overkill; at a glance I think ACA$_0^+$ suffices. And by "via Godel" I just mean the obvious incompleteness argument that ACA$_0$ can't prove that the naturals satisfy PA since then it would prove its own consistency. (Why would Dialectica be relevant?) | |
| Oct 21, 2019 at 21:24 | comment | added | Thomas Benjamin | @NoahSchweber: What strengthening of $ACA_0$ are you speaking of (possibly $ATR_0$)? And does the proof via Godel you mention in the above comment involve the Dialectica Interpretation? | |
| Oct 20, 2019 at 21:25 | comment | added | Noah Schweber | "Where are the subtleties in seeing this formula as true but unprovable in $ACA_0$?" I don't understand what you're asking - what sort of subtleties are you expecting? I'd say there aren't really any, the statement is just true and the proof (in a strengthening of ACA$_0$) is via Godel. I really don't understand what you're getting at. | |
| Oct 20, 2019 at 20:47 | comment | added | Thomas Benjamin | (cont.) notion of the term 'obvious' as regards $PA$, one seemingly needs to use higher-order concepts in the definition (e.g. $A^{-}_2$($\Sigma^1_1$)). I find it interesting that Hilbert, in "On the Infinite", tries to abstract the theory ($PA$?) from the theory's model (how does satisfaction play a role in such an approach?). If I understand correctly, the notions of satisfaction and truth ( for $\Sigma^0_0$ = $\Pi^0_0$ = $\Delta^0_0$) can be defined in the language of $PA$. This is just 'real' mathematics according to Hilbert. | |
| Oct 20, 2019 at 20:26 | comment | added | Thomas Benjamin | @NoahSchweber: Of course I can see how someone would find $PA$ and classical logic obvious at first (see my comments to (Prof.) Panu Raatikainen). The question for me is: Why? Consider the formula "$<$ $\mathfrak N$, $+$, $\times$ $=$ $>$ $\vDash$ $PA$", where $\mathfrak N$, '$+$', '$\times$, '$=$' are as defined in my question (stroke-notations and operations and relations on them). Where are the subtleties in seeing this formula as true but unprovable in $ACA_0$? I am not asking what the motivation behind $PA$ and classical logic is. I am just noting that in order to have a valid | |
| Oct 20, 2019 at 20:03 | comment | added | Thomas Benjamin | @NoahSchweber No. Please let me finish.... | |
| Oct 20, 2019 at 20:02 | comment | added | Noah Schweber | Wait, are you now just asking what the motivation behind PA and classical logic is? I'm starting to get really confused here. | |
| Oct 15, 2019 at 3:46 | history | edited | Michael Hardy | CC BY-SA 4.0 |
added 10 characters in body
|
| Oct 14, 2019 at 21:48 | comment | added | Noah Schweber | Per my answer, Gentzen is not rigorously defining the term "obvious," that's sort of the point. Gentzen is speaking informally; surely you can see how someone would reasonably find PA and classical logic obvious at first glance, and only later realize that there are subtleties (I think most students of logic follow this path). I think you're making things more confusing than they should be by trying to read too much precise content into Gentzen's remark. | |
| Oct 14, 2019 at 21:45 | comment | added | Thomas Benjamin | (cont.) and the principles of proof obviously preserve correctness?', i.e. how does Gentzen rigorously define the term 'Obvious' | |
| Oct 14, 2019 at 21:42 | comment | added | Thomas Benjamin | (cont.) Consider the following statement: '$<$ $\mathfrak N$, $+$, $\times$, $=$ $>$ $\vDash$ $PA$', where $\mathfrak N$, '$+$', '$\times$, '$+$', are defined as in my question. It is known that '$\vDash$' is definable in the following fragment of second-order arithmetic $A^{-}_2$: $A^{-}_2$($\Sigma^{1}_1$) (see Theorem 7 of Roman Murawski's paper, "Troubles With (the Concept of) Truth in Mathematics", Logic and Logical Philosophy Volume 15, (2006) Pg. 292. Given this, one can rightly ask, "What is the basis of Gentzen's claim that 'the axioms of arithmetic are obviously correct | |
| Oct 14, 2019 at 19:52 | comment | added | Thomas Benjamin | To those who voted to close on the basis of "Unclear on what you are asking": I am simply trying to find the 'Godel-point' that Gentzen claims is 'hidden' given the assumption that Gentzen's statement, 'The axioms of arithmetic are obviously correct, and the principles of proof obviously preserve correctness', is true. | |
| Oct 14, 2019 at 19:32 | history | edited | Thomas Benjamin | CC BY-SA 4.0 |
added quotation marks where needed
|
| Oct 10, 2019 at 21:28 | vote | accept | Thomas Benjamin | ||
| Oct 9, 2019 at 21:06 | comment | added | Noah Schweber | You shouldn't edit your question with continuing questions for specific answerers - comment on their answers instead. | |
| Oct 9, 2019 at 20:02 | history | edited | Thomas Benjamin | CC BY-SA 4.0 |
removed added comment
|
| Oct 9, 2019 at 20:00 | comment | added | Noah Schweber | Yes, it's fine to keep. (And I've updated my answer to address your edits.) | |
| Oct 9, 2019 at 20:00 | comment | added | Thomas Benjamin | @NoahSchweber: So keep it? | |
| Oct 9, 2019 at 19:58 | history | edited | Thomas Benjamin | CC BY-SA 4.0 |
added supplementary note
|
| Oct 9, 2019 at 19:57 | comment | added | Noah Schweber | Ah, I see. Since ACA$_0$ is stronger than WKL$_0$, it follows from that result that ACA$_0$ proves the completeness theorem. That's all Jech needs, but Takeuti's focused on the sharper observation that in fact the completeness theorem is equivalent (over RCA$_0$) to WKL$_0$. | |
| Oct 9, 2019 at 19:56 | comment | added | Thomas Benjamin | @NoahSchweber: That is the reference Jech gave (I am looking at my copy of his paper even as we speak--it is exactly as I wrote it). Considering your comment, should I just delete the reference? | |
| Oct 9, 2019 at 19:47 | history | edited | Thomas Benjamin | CC BY-SA 4.0 |
Added question for Panu Raatikainen
|
| Oct 9, 2019 at 19:40 | comment | added | Noah Schweber | That theorem is explicitly about WKL$_0$ (are you sure you have the right reference?), which is proof-theoretically vastly weaker than PA. In particular, PA proves the consistency of WKL$_0$, and more particularly the first-order part of WKL$_0$ is just I$\Sigma_1$ (the same as the first-order part of RCA$_0$ - indeed, WKL$_0$ is $\Pi^1_1$-conservative over RCA$_0$). | |
| Oct 9, 2019 at 19:36 | comment | added | Thomas Benjamin | @NoahSchweber: Oh by the way: Does Takeuti's Theorem 5.5, p. 443 of his Proof Theory, 2nd edition, refer to $ACA_0$ or to some other conservative extension of $PA$? | |
| Oct 9, 2019 at 19:32 | comment | added | Thomas Benjamin | @NoahSchweber: Thanks. Corrected yesterday | |
| Oct 8, 2019 at 21:44 | history | edited | Thomas Benjamin | CC BY-SA 4.0 |
Corrected the error Noah found and asked two questions regarding a passage in his answer
|
| Oct 7, 2019 at 22:19 | comment | added | Noah Schweber | Yes, that's right (per my answer). | |
| Oct 7, 2019 at 21:25 | comment | added | Thomas Benjamin | @NoahSchweber: Thanks for your helpful comments. Sorry I didn't respond sooner. Would this fix the error: 'It is unprovable in $ACA_0$ (unless it is inconsistent) that there exists a model of $PA$'? Pleas let me know and I will appropriately edit. | |
| Oct 7, 2019 at 19:07 | answer | added | Panu Raatikainen | timeline score: 2 | |
| Oct 7, 2019 at 0:05 | review | Close votes | |||
| Oct 23, 2019 at 3:05 | |||||
| Oct 6, 2019 at 19:47 | answer | added | Noah Schweber | timeline score: 13 | |
| Oct 6, 2019 at 19:24 | comment | added | Noah Schweber | Also, you attribute to Jech the claim "It is unprovable in PA (unless PA is inconsistent) that there exists a model of PA." But Jech does not make this claim, and for good reason: PA can't even express the existence of a model of PA! This is the whole point of passing to the conservative extension $\Gamma$, which is capable of talking about models. | |
| Oct 6, 2019 at 19:17 | comment | added | Noah Schweber | What does it mean to talk about a structure being definable in a theory? Certainly there are models of PA which do not interpret the standard model (indeed, no nonstandard model of PA can interpret the standard model). | |
| Oct 6, 2019 at 18:54 | history | edited | Thomas Benjamin | CC BY-SA 4.0 |
corrected mathjax
|
| Oct 6, 2019 at 18:46 | history | asked | Thomas Benjamin | CC BY-SA 4.0 |