Is there a distinction between saying a system has something that is provable and untrue and saying the system is self contradictory (and the more generalized layman interpretation that the system is wrong).
See https://en.wikipedia.org/wiki/Consistency. Under the syntactic definition of consistency, a self-contradiction simply means that a particular statement and its logical negation can both be proved in the system. That doesn’t say anything about the truth of the statement.
Wouldn't the 'truth' of a statement be depending upon the axioms of where you are making the statement. Thus something proven is true and if the negation is proven it is false, and thus a system able to prove both is self contradictory and even basic logic no longer applies, thus we lose any real world application.
The opposite a system which has true statements we can't prove is still useful, even if there might be some problems we won't ever be able to solve. But a system which can prove both a statement and its negation loses meaning.
Or does it? Naïve set theory, despite Russel's paradox, and language in general, despite the local equivalent of "This statement is a lie." is still a useful tool, so maybe the same applies even to more formal systems?
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?
> 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.
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.
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.
Yes, very much so. I think of the incompleteness theorem as saying that the language of mathematics is rich enough to express questions that are too complex to answer. That's a lot less worrying than there being contradictions (questions that we can prove are both false and true).
