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

What Gödel Discovered

stopa.io

Post reply on HN
Print view View original

201–210 of 271 posts

Re: What Gödel Discovered

#201

Post by Liron »

daralthus wrote: post #197
Liron wrote: post #180

People act like Godel’s Incompleteness Theorem is all about how formal systems are limited in their level of “insight about truth”. But actually it’s just the same observation as the Halting Problem: you have a system that tries to reason about the behavior of other systems (like Turing Machines or axiomatic set theory), but it can’t possibly always introspect about its own behavior because you can also configure it…

Because of the halting issue you cannot summarise reality into a set of axioms and rules. Which is the original purpose of mathematics. Therefore you cannot say mathematics is right or true without adding at the end: "this actually could all be wrong".

> Because of the halting issue you cannot summarise reality into a set of axioms and rules

Conway's Game of Life is a kind of reality summarized into axioms and rules, and most likely our universe/multiverse is on track to being similarly summarized. The halting issue doesn't get in the way of that achievement...

Once you have the intuition for why the Halting Problem (i.e. fortune teller paradox) is obvious, then Godel's proof is just an XSS attack on axiom systems whose designers think they're only "about numbers", like how CSS is designed to be about styling but it's also Turing-complete and vulnerable to XSS.

Russel and Whitehead were trying to simultaneously (1) invent a system capable of proving highly insightful claims about the infinite space of numbers, like "there doesn't exist a number between 1 and infinity with property P" but (2) not a system that can encode a Turing-equivalent agent that creates paradoxes if it tries to predict its own future.

Godel was just the first to point out that condition (2) was already met just by supporting Peano Arithmetic, the same way a modern computer science undergrad can point out that CSS is Turing-complete or your regex-based HTML validator is vulnerable to XSS attacks.

Re: What Gödel Discovered

#202

Post by Gehinnn »

ozankabak wrote: post #182

So if we have a theory expressive enough to make statements about ordinary (Peano) arithmetic, we can always form a self-referential statement within the framework of this theory which we can not prove or disprove. So far, so good. Here is my question: What happens if we restrict/weaken the theory to preclude self-referential statements? Obviously, we will lose our ability to express certain arithmetic statements whi…

It is very hard to detect self-referential statements and restricting yourself to "non-self-referential statements" might be quite severe.

Given a set of "domino" tiles - each having a top and a bottom. Each top and bottom has some word on it - these words can only use the letters "a" and "b". You can duplicate domino tiles and also align tiles so that all tops and all bottoms are aligned.

Now, given a finite set of such tiles, can you say whether there is an alignment so that all tops concatenated, read from right to left, equal all bottoms concatenated?

In fact, given such a set of tiles S, you can easily create a formula P(S) that is true iff such a valid alignment does not exist. Obviously this formula is true for some sets of tiles and false for others.

Now the funny thing: Given a (correct) fixed theory T in which you can state P(S) for every S and in which proofs can be computationally checked, there must be infinitely many S so that P(S) is true, but cannot be proved in T. Thus such theory T is incomplete.

Where is the self-reference?

This problem is also known as the Post correspondence problem (PCP). The halting problem can be reduced to it, which is not decidable. If T was complete, you could enumerating all proofs and see whether they correctly proof P(S) or its negation. Due to its completeness you would eventually find a proof for either of them and thus you could decide the halting problem.

Re: What Gödel Discovered

#203

Post by [deleted] »

JesseMeyer wrote: post #194

"This meant that no formal system, could prove by itself, that it could only produce true statements. " I see this generalization often, that Godel showed that all formal systems share this restriction, but doesn't the formal system have to be at least be able to express the properties of integers? Is the ability to formally express integers relatively a particularly demanding constraint on choice of axioms?

[deleted]

Re: What Gödel Discovered

#204

Post by green_on_black »

Liron wrote: post #180

People act like Godel’s Incompleteness Theorem is all about how formal systems are limited in their level of “insight about truth”. But actually it’s just the same observation as the Halting Problem: you have a system that tries to reason about the behavior of other systems (like Turing Machines or axiomatic set theory), but it can’t possibly always introspect about its own behavior because you can also configure it…

While this is true, it is surprising that is it impossible to engineer a system to be complete and consistent about arithmetic, as opposed to systems which are not engineered well, like your 2nd paragraph.

If I take "1 is even", "1 is odd" and "no number can be even and odd" as my axioms, then there is obviously a problem, but of my own doing.

Re: What Gödel Discovered

#205

Post by Gehinnn »

Liron wrote: post #201
daralthus wrote: post #197

Earlier quoted context omitted.

Because of the halting issue you cannot summarise reality into a set of axioms and rules. Which is the original purpose of mathematics. Therefore you cannot say mathematics is right or true without adding at the end: "this actually could all be wrong".

> Because of the halting issue you cannot summarise reality into a set of axioms and rules Conway's Game of Life is a kind of reality summarized into axioms and rules, and most likely our universe/multiverse is on track to being similarly summarized. The halting issue doesn't get in the way of that achievement... Once you have the intuition for why the Halting Problem (i.e. fortune teller paradox) is obvious, then Go…

CSS is not turing-complete - it is as turing-complete as a simple TXT file. Deciding whether some sequence of bytes resembles a CSS file is very possible. Deciding whether a stylesheet can be successfully applied to a website is also decidable. Of course, it is undecidable whether a certain pattern emerges if a stylesheet is applied to an infinitely large HTML file. But then, it is also undecidable whether some TXT file appears in an infinitely large HTML file.

Re: What Gödel Discovered

#206

Post by stopachka »

amboo7 wrote: post #163
stopachka wrote: post #129

Earlier quoted context omitted.

That's pretty rude of you. I didn't read that essay, but I did reference about 4 essays / books that I did read :). Went through the quanta article -- it seems reasonably different (doesn't go deep on how proof, subst, work, etc) -- I suspect the similarities stem from both of us reading Nagel and Newman's book.

Ok, then I apologize, it seemed very similar and recent.

Cheers!

Re: What Gödel Discovered

#207

Post by ethn »

ProfHewitt wrote: post #193
xyzzyz wrote: post #7

I’m a mathematician who spent many hours thinking about Goedel theorem and adjacent topics. The author in a self-deprecating way says that he’s not a mathematician, but just a programmer. Bear no mind to that: this is one of the best popular expositions of Goedel theorem I’ve seen. Everything is very accurately explained, there are no silly mistakes and untruths one often sees mentioned in context of Goedel theorem,…

Dear xyzzy, Unfortunately, you missed that the author's proof does not actually prove inferential undecidability (sometimes called "inferential incompleteness") of Russell's Principia Mathematica for the following reason: The [Gödel 1931] proposition *I'mUnprovable* does **not** exist in Principia Mathematica because it violates restrictions on orders of propositions that are necessary to avoid paradoxes (such as Rus…

Secondly, in the PM-Lisp it doesn't necessarily prove that theorem a proves b, it just shows that b can be a successor of the formulas in a

Re: What Gödel Discovered

#208

Post by unknown_apostle »

ProfHewitt wrote: post #195
dwohnitmok wrote: post #60

I thought I replied to this post, but I guess not and my reply ended up being a top-level reply, which is just as well. I will just mention my main two quibbles to this otherwise excellent post and others like it so that other people who embark on introductory posts to Godel's results don't fall into the same trap. 1. Please don't bring the notion of truth into an introductory explanation (such as in the section "Pow…

Dear dwohnitmok, Actually, powerful strongly-typed theories used in Computer Science can prove their own consistency! See the following article for for how this is done: https://papers.ssrn.com/abstract=3603021 As you pointed out, such a proof does not mean that it is not operationally possible to derive a contradiction using axioms and rules of inference. Instead our confidence in the consistency of a powerful stron…

I looked up your papers... Then I noticed you have also worked on paraconsistent logic. So to just boldly go on a completely new tangent and ask a question I have long sought to ask: do you know a good introduction text for paraconsistent logic, for a graduate level computer science student?

Re: What Gödel Discovered

#209

Post by ProfHewitt »

unknown_apostle wrote: post #208
ProfHewitt wrote: post #195

Earlier quoted context omitted.

Dear dwohnitmok, Actually, powerful strongly-typed theories used in Computer Science can prove their own consistency! See the following article for for how this is done: https://papers.ssrn.com/abstract=3603021 As you pointed out, such a proof does not mean that it is not operationally possible to derive a contradiction using axioms and rules of inference. Instead our confidence in the consistency of a powerful stron…

I looked up your papers... Then I noticed you have also worked on paraconsistent logic. So to just boldly go on a completely new tangent and ask a question I have long sought to ask: do you know a good introduction text for paraconsistent logic, for a graduate level computer science student?

Hello Unknown_apostle,

Thanks for looking at the articles!

The most up to date analysis of paraconsistent logic starts on page 11 of the following article:

https://papers.ssrn.com/abstract=3603021

Re: What Gödel Discovered

#210

Post by ianandrich »

mensetmanusman wrote: post #177

This is amazing. Two thoughts: 1) It seems that the black/white formalism of ‘ a statement can be only true or false ‘ causes issues. Have people tried introducing additional options for verifiability, e.g. ‘true / false / maybe?’ or something that points to uncertainty à la Heisenberg? 2) It would be really interesting for the author to continue the line of reasoning to help add insight to Gödel’s ontological proof.…

Apparently someone had the following thought.

"Everyone when faced with the dilemma of having either an unsound or incomplete formal system chooses incompleteness. What happens when we allow for unsoundness and treat this notion as first class?"

There has been a slow burn on paraconsistent logics going back to the 80s or so now.

https://en.wikipedia.org/wiki/Paraconsistent_logic

I seem to recall at least one where one of the states was something analogous to a maybe/don't know.

Post reply on HN