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

What Do Gödel's Incompleteness Theorems Mean?

quantamagazine.org

Post reply on HN
Print view View original

61–70 of 72 posts

Re: What Do Gödel's Incompleteness Theorems Mean?

#61

Post by pdonis »

kenjackson wrote: post #55
pdonis wrote: post #22

Earlier quoted context omitted.

> I always thought that the incompleteness theorems says, there are theorems that are true or false in all models but cannot be proved to be so. As the GP points out, that's not what Godel's incompleteness theorem actually shows. Although it's a common misconception (one which unfortunately is propagated by many sources that should know better). The key point of the incompleteness theorem is that it shows that (at le…

I think you’re right that "true in all models but unprovable" is not accurate. By Godel’s completeness theorem if a FO sentence is true in every model of the axioms then it is provable from those axioms. But I don’t think incompleteness is best described as saying "no first-order axioms can pin down a single model" That’s more about non-categoricity/compactness/Lowenheim–Skolem.

> That’s more about non-categoricity/compactness/Lowenheim–Skolem.

As I understand it, the proof of the Lowenheim-Skolem theorem requires the axiom of choice, but the proof of the two Godel theorems does not. That would make a difference for people who are doubtful about the axiom of choice.

Re: What Do Gödel's Incompleteness Theorems Mean?

#62

Post by [deleted] »

renticulous wrote: post #58
alan-crowe wrote: post #30

As a child, I noticed that the proofs of mathematical theorems were esoteric knowledge, known only to a few adults. I struggled to follow even the simplest proofs, and hoped that one day I might learn to create a proof or two of my own. This was not only a high aspiration, but a dangerous one. I saw no reason why certain knowledge of a true fact would be accessible to humans via proof. Any-one who embarked on the que…

Universe is the Godel sentence in the limit of all possible mathematics. Hence it exists and is True. Fix axioms, we get a Godel sentence G1. Add G1 to axioms, we get G2. So on and so forth. In the limit of this process, we have our Universe.

[deleted]

Re: What Do Gödel's Incompleteness Theorems Mean?

#63

Post by AxEy »

alan-crowe wrote: post #30

As a child, I noticed that the proofs of mathematical theorems were esoteric knowledge, known only to a few adults. I struggled to follow even the simplest proofs, and hoped that one day I might learn to create a proof or two of my own. This was not only a high aspiration, but a dangerous one. I saw no reason why certain knowledge of a true fact would be accessible to humans via proof. Any-one who embarked on the que…

> The real problem turns out to be the combinatorial explosion inherent in unstructured search through the Herbrand universe. One needs Unification and one needs a still missing ingredient to give search a sense of direction.

Shameless plug: I put together a Jupyter notebook walking through the use of Herbrand Universes for a semi-decision procedure for first order logic: https://github.com/aetilley/harrison-rust/blob/main/Herbrand...

Re: What Do Gödel's Incompleteness Theorems Mean?

#64

Post by whattheheckheck »

marojejian wrote: post #2

Interesting points in here. e.g. that Godel didn't think this scrapped Hilbert's project totally: >Gödel believed that it was possible to redefine what we mean by a formal mathematical framework, or allow for alternative frameworks. He often discussed an infinite sequence of acceptable logical systems, each more powerful than the last. Every well-formulated mathematical question might be answerable within one of them…

I wonder if thats why agile is best. We can never fully "prove" the program as theory building

Re: What Do Gödel's Incompleteness Theorems Mean?

#65

Post by alexwwang »

alan-crowe wrote: post #30

As a child, I noticed that the proofs of mathematical theorems were esoteric knowledge, known only to a few adults. I struggled to follow even the simplest proofs, and hoped that one day I might learn to create a proof or two of my own. This was not only a high aspiration, but a dangerous one. I saw no reason why certain knowledge of a true fact would be accessible to humans via proof. Any-one who embarked on the que…

To put it simple, my understanding to this theorem is that we can not design and implement a program without any bugs.

So it indicates me to think about the boundaries while I design and build a system. These boundaries will protect us from those unsolvable constraints.

Re: What Do Gödel's Incompleteness Theorems Mean?

#67

Post by coldtea »

kkylin wrote: post #46
alan-crowe wrote: post #30

As a child, I noticed that the proofs of mathematical theorems were esoteric knowledge, known only to a few adults. I struggled to follow even the simplest proofs, and hoped that one day I might learn to create a proof or two of my own. This was not only a high aspiration, but a dangerous one. I saw no reason why certain knowledge of a true fact would be accessible to humans via proof. Any-one who embarked on the que…

I really do think the incompleteness theorems deserve the attention they get, not just because of what they say about efforts to formalize mathematics and because of the historical context -- remember Gödel numbers came (just) before Turing and the first recognizably modern electronic computers. That numbers can represent things that are not numbers was (IMO) a revolutionary idea. Having said all that, I'd taken math…

>That numbers can represent things that are not numbers was (IMO) a revolutionary idea.

When it first appeared, sure. But it wasn't with Godel and Turing that this happened.

Re: What Do Gödel's Incompleteness Theorems Mean?

#68

Post by coldtea »

alexwwang wrote: post #65
alan-crowe wrote: post #30

As a child, I noticed that the proofs of mathematical theorems were esoteric knowledge, known only to a few adults. I struggled to follow even the simplest proofs, and hoped that one day I might learn to create a proof or two of my own. This was not only a high aspiration, but a dangerous one. I saw no reason why certain knowledge of a true fact would be accessible to humans via proof. Any-one who embarked on the que…

To put it simple, my understanding to this theorem is that we can not design and implement a program without any bugs. So it indicates me to think about the boundaries while I design and build a system. These boundaries will protect us from those unsolvable constraints.

>that we can not design and implement a program without any bugs.

If we don't include the compiler and runtime, sure we can.

Godel's theorem is about formal axiomatic mathematical systems with certain properties like the ability to do basic arithmetic.

Re: What Do Gödel's Incompleteness Theorems Mean?

#69

Post by alexwwang »

coldtea wrote: post #68
alexwwang wrote: post #65

Earlier quoted context omitted.

To put it simple, my understanding to this theorem is that we can not design and implement a program without any bugs. So it indicates me to think about the boundaries while I design and build a system. These boundaries will protect us from those unsolvable constraints.

> that we can not design and implement a program without any bugs. If we don't include the compiler and runtime, sure we can. Godel's theorem is about formal axiomatic mathematical systems with certain properties like the ability to do basic arithmetic.

As long as you make use of axiomatic theorem to design a system, you will make a friend with Gödel. It’s not just a problem of compiler or runtime. :)

Re: What Do Gödel's Incompleteness Theorems Mean?

#70

Post by LegionMammal978 »

empath75 wrote: post #27
seanhunter wrote: post #12

As far as I can see people always radically exaggerate the effect of the incompleteness theorems. It seems interesting that any nontrivial axiomatic system has statements which are true but unprovable but to say that derails Hilbert’s project seems just obviously untrue when you can for example join math postgrad programs now which are focused on formalisation. [1] So formalisation is very much still going on, probab…

> the vast vast majority of statements in any axiomatic system are going to be decidable This is just flatly untrue, in the strictest possible sense, and even in the generous definition of "statements that mathematicians care about", that is going to be very heavily biased towards questions that are decidable, because the questions that are likely to be decidable are the ones that they can even reason about to begin…

To be fair, in the most literal sense, the vast majority of syntactically-valid statements in a typical FOL encoding will be trivial. One of my side-projects has been trying to find the shortest statements independent of ZF and some of its fragments. In fact, for every slightly nontrivial statement that requires actually building a construction, there are billions more that can be instantly solved via a few simplifications, and statically pruning the search tree a bit is the best we can do.

To actually get independence, we need very rigid statements that don't allow any simple way to fudge a solution or counterexample. If anything, statements that mathematicians (and programmers) care about are biased toward undecidability, simply because they're extremely biased toward nontriviality. We put in the hard work of building towers of rigid definitions to that effect.

Post reply on HN