(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
Add it as a new axiom. That's my understanding too.If so, we would need patch system X with either the statement that's unprovable (P) or another one with which we can prove P - call this new system Y. The catch is that the problem of unprovable true statements will recur in the new system Y too and so on. — TheMadFool
I'll yield to Nagase, but it seems to me that truth is not always that important - even that truth cannot be well-defined. More it is, does the claim in question work. And words like "necessary" don't help, unless used and understood as terms of art with a determinate meaning.IF proof isn't necessary for truth then, how do we distinguish between truths and falsehoods? The universal response to claims people make is to ask for proof. — TheMadFool
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
It seems to me that at the level of the absolute, you have being and not-being - and that's it! Kindly, patiently, and briefly educate me on the utility and value - and meaning - of your observation. I get (I'm pretty sure I get) Godel, at the level of his paper on undecidable propositions.is that the absolute consistency of PA isn't knowable, or even intelligible. As an absolute notion, undecidability is meaningless. — sime
Infallible maybe, but certainly incomplete, in the elementary sense that it only includes - if even it does that - just those propositions that stand as the conclusion of proofs. What will it do for propositions that aren't the conclusions of proofs? Call them non-theorems? And if by theorem you mean exactly that - proved propositions - then it would appear you miss G and G' and G'', and so forth.It is obviously infallible, since Check Proof is infallible. — 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.