35 ms·
> Gödel's Incompleteness Theorem: any sufficiently rich formal system, together with an interpretation, has strings which are true but unprovable. This is only
by jstanley 4y ago
> Gödel's Incompleteness Theorem: any sufficiently rich formal system, together with an interpretation, has strings which are true but unprovable.
This is only half of it!
Gödel's Incompleteness Theorem states that any sufficiently rich formal system, together with an interpretation, either has strings which are true but unprovable or has strings which are provable but untrue. Either is possible! In practice people prefer to have true things that can't be proven rather than provable things that are untrue. But either is possible.
- pdonis 4y ago> or has strings which are provable but untrue. Where are you getting this from?
- slowhand09 4y agoCareful lest you be shot with a crab cannon.
- SkyBelow 4y agoIs 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).
- layer8 4y agoSee https://en.wikipedia.org/wiki/Consistency 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.
- teawrecks 4y agoBut 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 agoIf 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 agoWhy 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.
- SkyBelow 4y agoWouldn'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?
- lmm 4y agoYes, 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).
- red_trumpet 4y agoHow can a statement that is unprovable be true? I always had the impression that unprovable means you could add either the statement or its negation as an axiom, and both resulting systems are as consistent as the system you started with
- Twisol 4y agoGood question! In this context, we're relating a system of proofs to the properties of a desired model. If you start from a sufficiently expressive model and try to design a proof system where valid proofs correspond to true properties, then you will either miss some properties (an unproveable truth) or you will have too many proofs (proveable falsehoods). Without biasing for a particular model, we could simply say that every sufficiently expressive proof system admits either zero models or more than one model.
- fao_ 4y agoWithout a telescope I can't prove to you that andromeda is a galaxy, but it is.
- frimsah 4y agofollowing this analogy: is it possible with the proper instrumentation, or axioms, that a mathematical statement might become provable?
- schoen 4y agoYes, you can add more axioms and produce a more powerful system which can resolve more questions. In some cases you actually have a choice about whether to assume that something is true or that it's false (for example you can assume the continuum hypothesis or its negation!), and neither choice on its own produces an inconsistency, but either choice makes a different set of conclusions provable. However, Gödel made explicit in the very first statement of his incompleteness theorem that assuming more axioms cannot ever eliminate incompleteness (except by the extremely undesirable event of eliminating consistency). Gödel shows that, if a set of axioms (including additional axioms on top of your original set) doesn't allow you to prove everything (by virtue of being inconsistent, something called the "principle of explosion"), then there are necessarily statements that those axioms can't resolve the truth of. So you can add more axioms and that will either make your system more powerful or inconsistent (depending on whether you chose inconsistent axioms to add), but you still can't get rid of the incompleteness phenomenon that way!
- a1369209993 4y ago> > Gödel's Incompleteness Theorem: any sufficiently rich formal system, together with an interpretation, has strings which are true but unprovable. Somewhat oddly, this is actually technically correct - a "sufficiently rich" system is one that can distinguish true versus false statements of Peano Arithmetic, and a inconsistent system, by the principle of explosion, can prove any statement, so cannot distinguish statements of Peano Arithmetic (eg, 1+1=2 and 1+1=3 are both provable), and hence is not sufficiently rich. That's a somewhat unintuitive way of looking at it in practice, though.
- skoodge 4y agoThat's only true for systems where the principle of explosion actually holds though, isn't it? So it wouldn't apply to paraconsistent systems. In the end, Gödel is actually giving us a choice: Either accept incompleteness or accept inconsistency. Of course it's true that historically incompleteness has been perceived as the only viable choice, but at least a few paraconsistent logicians like Graham Priest have argued for (non-explosive) inconsistency instead.
- theteapot 4y agoThere are no paraconsistent logicians arguing for explosive inconsistency?! Outrageous.
- picsao 4y ago