Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Gödel, Escher, Bach: an in-depth explainer

alignmentforum.org

Post reply on HN
Print view View original

201–210 of 252 posts

Re: Gödel, Escher, Bach: an in-depth explainer

#201

Post by chriswarbo »

thayne wrote: post #172
schoen wrote: post #165

Earlier quoted context omitted.

> But one of those two must be true, you just can't prove it. Three alternative accounts: * Both the CH and ¬CH mathematical universes really exist, so we just have to choose which one we're more interested in at a given time. Like one might say there are the "reall numbers" and the "realle numbers", both valid and interesting constructions which humanity was just slow to recognize the distinctions between (because t…

sure, but if you ignore any connection to the real world or platonic truth and are just talking about within the ZFC formalism, then `CH ∨ ¬CH` is a true statement, even though it is impossible to prove either `CH` or `¬CH`.

> within the ZFC formalism, then `CH ∨ ¬CH` is a true statement

It's also a provable statement (via excluded middle)

Re: Gödel, Escher, Bach: an in-depth explainer

#202

Post by adastra22 »

dudeguy3301 wrote: post #173
adastra22 wrote: post #158

Earlier quoted context omitted.

I was talking about Gödel, not Goldbach: > The proof of Gödel's result's involves very carefully formalizing what statements and proofs mean so that they can be encoded as statements about arithmetic. He then shows there is a statement with encoding G that says "The statement with encoding G cannot be proved" – if it is true, then it cannot be proved. Sorry I meant to quote this bit at the beginning of my comment. Pa…

wait, so you are casually dismissing Gödel's work as a logical "gotcha"? don't premise opinions about complex proofs on other peoples woefully impoverished and misrepresented explanations of said proofs that is disrespectful and very very very short sighted. also, go read up (...on Gödel, Cantor, Turing, Tarski, etc...)

Please try to give the people you talk to the benefit of the doubt, and read carefully what you are responding to.

My training is as an applied physicist. We physicists have an interesting relationship with math. Obviously math is essential to the work that we do, but the physical world decides whether the math is right, not the other way around. Our mathematical models technically permit things like negative mass, time flowing backwards, or magnetic monopoles. But that doesn't mean tachyons, time machines, or fundamental magnetic particles exist--they don't, so far as we know. So I'm trained to actively disregard non-physical, not relevant mathematical implications. I'm sorry if this offends a pure mathematicians sensibilities, but pragmatically it is very useful.

Or take a different field: in computational semantics, a branch of formal linguistics, there are many models for inferring a formal logical statement from an example written sentence or spoken utterance, and then determining the validity (truth) of the statement. These models get caught up on stuff like "This sentence is false." What's the truth value for that sentence? If it is true then it must be false, and if it is false then it must be true. Error, validity of this statement can't be determined! But hey, it turns out that in practice this basically never happens unless the speaker is really confused, misspeaks, or deliberately evasive. Real sentences don't have this self-referential, circular logic structure because that's not how people think or communicate.

Now "this sentence is false" goes back to the greeks, IIRC, and Gödel's theorem is slightly different. Gödel's main work is in the formalization of proofs and proof systems, and I don't want to take away from that in any way. But the incompleteness theorem always seems to be explained through these sorts of self-referential examples and I have yet to ever see it reduced to a practical problem with real-world implications. Hence my question. Does Gödel's incompleteness theorem actually constrain a real world application of proof systems, where we tend to be interested in non-cyclical logical arguments?

Re: Gödel, Escher, Bach: an in-depth explainer

#203

Post by adastra22 »

wikfwikf wrote: post #188
machina_ex_deus wrote: post #181

Earlier quoted context omitted.

The Continuum hypothesis is independent of ZFC. It is the first of Hilbert's 23 problems.

This is the best example - before it was shown that the Continuum Hypothesis was unprovable, many people believed, like the GP, that only uninteresting and artificial statements could be shown to be unprovable. The CH is undoubtedly meaningful, natural, and of huge interest to (a subset of) mathematicians.

What are the practical applications of CH?

Re: Gödel, Escher, Bach: an in-depth explainer

#204

Post by trashtester »

gsinclair wrote: post #199
red_trumpet wrote: post #182

Earlier quoted context omitted.

What do we actually mean by saying "statement S is unprovable"? Do we mean "there is no prove for S" (which includes the case that S is provably false), or do we mean "there is no proof for S and there is no proof for its converse"? Because if you show that the converse of Goldbach's conjecture is not provable, you have actually proven Goldbach's conjecture (since you have shown that there is no counterexample!). >Th…

> What do we actually mean by saying "statement S is unprovable"? Do we mean "there is no [edited:] proof for S" (which includes the case that S is provably false), or do we mean "there is no proof for S and there is no proof for its converse"? By “converse” I think you mean “negation”. A statement being unprovable means we will never know whether it is this or false. > Because if you show that the converse of Goldba…

> Nope: demonstrating that (the opposite of Goldbach’s conjecture) is unprovable is logically equivalent to demonstrating that (Goldbach’s conjecture) is unprovable. It means we’ll never know either way.

I think this is false. If you find a number N that is not the sum of two primes, you did disprove Goldbach's conjecture. Any such number would be smaller than infinity, and so there would only be a finite set of primes smaller it to check for.

So basically, if Goldbach's conjecture turns out to be false it IS going to be PROVABLY false.

Only if Goldbach's conjecture is actually true will it be the case that it is impossible to prove its negation. But if it is ALSO unprovable (but STILL true) you will NOT be able to prove that the negation is unprovable, because that would mean that there doesn't exist ANY number N that disproves the conjecture, so would prove the unprovable original conjecture....

Consider the statement "All swans are white", but you live in a universe with an infinite number of swans.

Lets assume that there exists at least one black swan. Proving the statement false is trivial once you find the first black swan.

However, if all swans in the given universe ARE white, and you have no way of inspecting every one, you can never PROVE that they are all white. Also you can NOT prove that it is impossible to prove the negation.

Re: Gödel, Escher, Bach: an in-depth explainer

#205

Post by trashtester »

black_knight wrote: post #63
red_trumpet wrote: post #51

Earlier quoted context omitted.

How 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

> How can a statement that is unprovable be true? If you are a platonist and believe in some preferred model where every statement is decided this makes perfect sense. For the rest of us, this just means that in a sufficiently complex system there will be undecided statements. Which is not such a big surprise – but a rather awesome technical exercise!

Undecided is not quite the same as true. My understanding is that there can be statements that are necessarily true within a given set of axioms, but still unprovable using a proof of limited length.

Re: Gödel, Escher, Bach: an in-depth explainer

#206

Post by didericis »

wikfwikf wrote: post #190
didericis wrote: post #160

Earlier quoted context omitted.

You don’t need to go through every possible element in that infinite uncountable set to prove that relationship, though. You can create an arbitrary demonstration that you can then manipulate in your head. Once you see that water demonstration you can inuit how that relationship must persist at different sizes. Again, that doesn’t really count as a “proof” by modern standards, but it’s how the ancient greeks thought…

But your brain is, presumably, doing finitely many cognitive steps, so it seems that a proof you can understand can also be expressed finitely?

That’s a really deep question. If our brains are like digital computers, then yes, that’d be true. But they could be like analog computers, quantum computers, or something we don’t yet have the ability to describe.

Re: Gödel, Escher, Bach: an in-depth explainer

#207

Post by wikfwikf »

didericis wrote: post #206
wikfwikf wrote: post #190

Earlier quoted context omitted.

But your brain is, presumably, doing finitely many cognitive steps, so it seems that a proof you can understand can also be expressed finitely?

That’s a really deep question. If our brains are like digital computers, then yes, that’d be true. But they could be like analog computers, quantum computers, or something we don’t yet have the ability to describe.

The problem with this theory is: what is the part of a geometric proof which cannot be described or validated using a classical, discrete computer? There is no such step. All parts of mathematics which mathematicians are able to agree on can be so described. There is no scope for our brains taking in an analog measurement, doing an analog measurement step on it, and using it to confirm the truth of a mathematical statement.

Of course, this is not an argument that our brains are absolutely finite and classical. Perhaps analog computations is required for an appreciation of beauty, or quantum physics is necessary for us to fall in love. But we seem to be able to check math proofs without them.

Re: Gödel, Escher, Bach: an in-depth explainer

#208

Post by bedman12345 »

cruegge wrote: post #196
bedman12345 wrote: post #183

Earlier quoted context omitted.

Yeah but second order logic itself is incomplete. ZFC doesn't have a single model, too, btw. In the end unprovable sentences exist because there are multiple models satisfying your axioms.

What I meant to say is that multiple models are not the only reason for something to be true but unprovable, the incompleteness theorem also holds in more general conditions. Concerning multiple models of ZFC: I'm always confused by such statements about the foundations of set theory itself, they seem weirdly self-referential. ZFC certainly can't prove that it has multiple (or even any) models. Does such a statement…

You simply use "intuitive mathematics", in other words: no formalization. That's at least what I got when I read books on set theory.

Löwenheim-Skolem implies the existence of a countable model of ZFC. https://en.m.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skole...

"What I meant to say is that multiple models are not the only reason for something to be true but unprovable, the incompleteness theorem also holds in more general conditions." I can't give a clean rebuttal for this, but I believe this to be profoundly mistaken. It might be technically correct though, depending on how you'd formalize this statement. To formalize math you need a logic that has some properties: it should be decidable whether a proof is correct, you should be able to write it down, it should not be contradictory. If you take these together the only way a statement is unprovable, is if it is independent from the axioms, i.e. there exist multiple models.

Re: Gödel, Escher, Bach: an in-depth explainer

#209

Post by kubanczyk »

trashtester wrote: post #204
gsinclair wrote: post #199

Earlier quoted context omitted.

> What do we actually mean by saying "statement S is unprovable"? Do we mean "there is no [edited:] proof for S" (which includes the case that S is provably false), or do we mean "there is no proof for S and there is no proof for its converse"? By “converse” I think you mean “negation”. A statement being unprovable means we will never know whether it is this or false. > Because if you show that the converse of Goldba…

> Nope: demonstrating that (the opposite of Goldbach’s conjecture) is unprovable is logically equivalent to demonstrating that (Goldbach’s conjecture) is unprovable. It means we’ll never know either way. I think this is false. If you find a number N that is not the sum of two primes, you did disprove Goldbach's conjecture. Any such number would be smaller than infinity, and so there would only be a finite set of prim…

> if all swans in the given universe ARE white, and you have no way of inspecting every one, you can never PROVE

Yes, you can. Math is not physics. Pythagoras was able to prove his theorem about every triangle in the universe without inspecting every triangle in the universe. The trick is that "the universe" is not the physical universe, it's just a choice of axioms.

Re: Gödel, Escher, Bach: an in-depth explainer

#210

Post by didericis »

wikfwikf wrote: post #207
didericis wrote: post #206

Earlier quoted context omitted.

That’s a really deep question. If our brains are like digital computers, then yes, that’d be true. But they could be like analog computers, quantum computers, or something we don’t yet have the ability to describe.

The problem with this theory is: what is the part of a geometric proof which cannot be described or validated using a classical, discrete computer? There is no such step. All parts of mathematics which mathematicians are able to agree on can be so described. There is no scope for our brains taking in an analog measurement, doing an analog measurement step on it, and using it to confirm the truth of a mathematical sta…

I think mathematical intuition might be some kind of weird analog calculation, but yes, I can’t think of an actual visual proof that cannot also be described in discrete formal terms and validated with a computer. There might be examples out there somewhere, but I don’t know of any.
Post reply on HN