4 ms·

But isn't something defined as true in a system iff it can be proven in said system? So the only way "proven but untrue" makes sense is if there is a contradict

But isn't something defined as true in a system iff it can be proven in said system? So the only way "proven but untrue" makes sense is if there is a contradiction, no?

layer8 4y ago
If the statement “This statement cannot be proven” cannot be proven in the system, does that make the statement untrue just because it cannot be proven in the system? Seems not. Truth is defined by a model or interpretation of the system, not by the system. As TFA explains, the Incompleteness Theorem showed that truth and provability must be considered as separate notions.
edanm 4y ago
> But isn't something defined as true in a system iff it can be proven in said system? No. You can build a really trivial system and know things about it "from the outside", so to speak, even if they can't be proved within the system itself. Godel's work is exactly about showing the difference between something being actually true, and something being provable within a system. Let's take a not-real example: we know there are infinitely many primes. If you define arithmetic formally, you can fairly easily prove that there are infinitely many primes. But, in theory, it could be something that isn't provable, but is still true; true because you can always actually generate more primes, but unprovable because there is no way to build a proof out of the axioms of arithmetic to show this. Now, this isn't true about the infinitude of primes, because it can be proved within arithmetic. But there are lots of other statements that we have't proved yet - and theoretically, any one of them could end up being unprovable. E.g. Goldbach's conjecture or the 3n+1 theorem - they might be actually true but something we can't prove within the way we've defined arithmetic.
bmacho 4y ago
Why not? E.g.: if ZFC is consistent, then ZFC+~Con(ZFC) is consistent as well, where ~Con(ZFC) is the statement that there is a contradiction in ZFC. Now, ZFC+~Con(ZFC), which is a perfectly good axiom system, consistent and can talk about anything, can prove that the Turing machine that searches for a contradiction in ZFC halts (just apply the axiom ~Con(ZFC)), but it doesn't make it true.

But isn't something defined as true in a system iff it can be proven in said system? So the only way "proven but untrue" makes sense is if there is a contradiction, no?

layer8 4y ago

If the statement “This statement cannot be proven” cannot be proven in the system, does that make the statement untrue just because it cannot be proven in the system? Seems not. Truth is defined by a model or interpretation of the system, not by the system. As TFA explains, the Incompleteness Theorem showed that truth and provability must be considered as separate notions.

edanm 4y ago

> But isn't something defined as true in a system iff it can be proven in said system? No. You can build a really trivial system and know things about it "from the outside", so to speak, even if they can't be proved within the system itself. Godel's work is exactly about showing the difference between something being actually true, and something being provable within a system. Let's take a not-real example: we know there are infinitely many primes. If you define arithmetic formally, you can fairly easily prove that there are infinitely many primes. But, in theory, it could be something that isn't provable, but is still true; true because you can always actually generate more primes, but unprovable because there is no way to build a proof out of the axioms of arithmetic to show this. Now, this isn't true about the infinitude of primes, because it can be proved within arithmetic. But there are lots of other statements that we have't proved yet - and theoretically, any one of them could end up being unprovable. E.g. Goldbach's conjecture or the 3n+1 theorem - they might be actually true but something we can't prove within the way we've defined arithmetic.

bmacho 4y ago

Why not? E.g.: if ZFC is consistent, then ZFC+~Con(ZFC) is consistent as well, where ~Con(ZFC) is the statement that there is a contradiction in ZFC. Now, ZFC+~Con(ZFC), which is a perfectly good axiom system, consistent and can talk about anything, can prove that the Turing machine that searches for a contradiction in ZFC halts (just apply the axiom ~Con(ZFC)), but it doesn't make it true.