(1) Gödel (well, Gödel, Church, Tarski, Rosser, etc.) showed a bit more than what you are implying. He showed that, for any consistent system containing enough arithmetic (i.e. extending Robinson's arithmetic), the set of theorems of that system is not identical to the set of truths of that system. So, if we just move one level up and claim that truth is provability in a higher system, this won't do, because the theorem will reapply at the higher level separating these sets again. — Nagase
There would only be a contradiction if Gödel claimed that his own theorem was unprovable. Fortunately, he was not an idiot, and therefore did not claim that. What he did claim was that some truths are unprovable (his own theorem not being among those). And the reason why some truths are unprovable was sketched in my first post in this thread, namely the theorems are all capable of being listable by an algorithm, whereas no algorithm can list all truths. Hence, there are truths that will not appear in the list of all theorems, hence, not every truth is a theorem. Again, note that, in this version, no mention is made of a specific unprovable statement, so your reasoning about the "meta-cognitive" level does not apply. — Nagase
I don't think Löb's theorem supports the constructivist position. That's because truth is generally taken, prima facie to obey the capture and release principles: if T('S'), then S (release), and, if S, then T('S') (capture). But what Löb's theorem shows is that proof does not obey the release principle. So there is at least something suspicious going on here. — Nagase
Moreover, one can show that the addition of a minimally adequate truth-predicate to PA (one that respects the compositional nature of truth) is not conservative over PA. Call this theory CT (for compositional truth). Then CT⊢∀x(Sent(x)→(Prov(x)→T(x)))CT⊢∀x(Sent(x)→(Prov(x)→T(x))), where "T" is the truth predicate. As a corollary, CT proves the consistency of PA. So truth, unlike provability, is not conservative over PA. — Nagase
Finally, you have yet to reply to my argument regarding the computability properties of the two predicates, namely that one does have an algorithm for listing all the theorems of PA, whereas one does not have an algorithm for listing all the truths of PA. So the two cannot be identical. — Nagase
think you are focusing too much on the fact that theoremhood is not strongly representable in PA, with the consequence that you are ignoring the fact that it is weakly representable in PA. Indeed, while theoremhood is not computable, it is computably enumerable. In other words, there is an algorithm which lists all and only theorems of PA. It exploits the fact that, given your favorite proof system, whether or not a sequence of formulas is a proof of a sentence of PA is decidable. Call the algorithm which decides that "Check Proof". Here's an algorithm which lists all the theorems of PA, relative, of course, to some Gödel coding:
Step 1: Check whether n is the Gödel number of a sequence of formulas of PA (starting with 0). If YES, go to the next step. Otherwise, go to the next number (i.e. n+1).
Step 2: Decode the sequence of formulas and use Check Proof to see if it is a proof. If YES, go to the next step. Otherwise, go back to Step 1 using as input n+1.
Step 3: Erase all the formulas in the sequence except the last. Go back to Step 1, using as input n+1.
This (horrible) algorithm lists all the theorems, i.e. if S is a theorem of PA, it will eventually appear in this list. Obviously, this cannot be used to decide whether or not a given formula is a theorem, since, if it is not a theorem, then we will never know it isn't, since the list is endless. But, again, it can be used to list all the theorems. My point is that there is nothing comparable for the truths, i.e. there is no algorithm that lists all the truths. In fact, by Tarski's theorem, there can be no such algorithm. So, again, the two lists (the list of all the theorems, the list of all the truths) are not the same, whence the concepts are different. — Nagase
The upshot of all this is that, in my opinion, constructivists should resist the temptation of reducing truth to provability. Instead, they should follow Dummett and Heyting (on some of their most sober moments, anyway) and declare truth to be a meaningless notion. If truth were reducible to provability, then it would be a constructively respectable notion. But it isn't (because of the above considerations). So the constructivist should reject it. (Unsurprisingly, most constructivists who tried to explicate truth in terms of provability invariably ended up in a conceptual mess---cf. Raatikainen's article "Conceptions of truth in intuitionism" for an analysis that corroborates this point.) — Nagase
I've never come across, nor contemplated tracing the proof of something like the fundamental theorem of calculus back to its set theoretic roots. — jgill
What do you mean to communicate here? — fishfry
Do you wish math would go back to the mid nineteenth century before the age of formalization? — fishfry
I know you think I'm a dinosaur of a mathematician — jgill
you often announce your ignorance of virtually everything outside of your specialty, and most of the standard undergrad math curriculum. — fishfry
I only wish to tell you that with your background, every single thing that's been discussed on this forum that you think is beyond you, is actually trivially within your capabilities and knowledge. — fishfry
Get involved in philosophical discussions about knowledge, truth, language, consciousness, science, politics, religion, logic and mathematics, art, history, and lots more. No ads, no clutter, and very little agreement — just fascinating conversations.