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

211–220 of 271 posts

Re: What Gödel Discovered

#211

Post by ProfHewitt »

greatquux wrote: post #196
ProfHewitt wrote: post #193

Earlier quoted context omitted.

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…

I'm going to need someone to come along and write up a layman's summary of this article. :) Does it change the end result of Gödel? Or is it basically the equivalent of saying what some restricted programming languages are doing, that we can get "good enough" results and not have these problems by restricting what we can do in the language?

Hi GreatQuux!

The article linked below explains why [Gödel 1931] did not prove inferential undecidability of Russell's Principia Mathematica and likewise why the formalization of [Gödel 1931] in Lisp proof being discussed is also invalid:

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

However, the article linked above does have a correct proof of inferential undecidability (also known as "inferential incompleteness").

Would be happy to respond to any questions that you might have.

Re: What Gödel Discovered

#212

Post by ProfHewitt »

ethn wrote: post #207
ProfHewitt wrote: post #193

Earlier quoted context omitted.

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

Hi Ethn!

Existence of the [Gödel 1931] proposition I'mUnprovable is inconsistent with the following theorem to the effect that theorems can be used in proofs:

      ⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ

Re: What Gödel Discovered

#213

Post by deanCommie »

Something that is never clear to me - what defines what is an axiom and what is derived from the axiom?

In Russel's PM, `(when (or p p) p)` is considered an axiom, but `=` isn't, and is derived from the other axioms.

But...why not the reverse? The axiom "when either apples or apples, then apples" just seems like another way to state "apples = apples". Why is that not the axiom that other things follow from, then?

Re: What Gödel Discovered

#214

Post by hvis »

nmadden wrote: post #191
hvis wrote: post #189

I've read Godel, Escher, Bach, and I've read this. It's a very nice explanation. But everywhere I see, Godel's theorem is touted as some kind of deep philosophical insight, whereas from what I understand, informally it could be rephrased as "if you have a usable language for mathematical proofs, some phrases in that language must be neither true nor false (i.e. nonsensical)". Nonsensical phrases in our human language…

It’s not so much that they’re neither true nor false (they’re not paradoxes), but that they can be true in some interpretations and false in others. I wrote up some notes about this here: https://neilmadden.blog/2020/11/17/some-incomplete-thoughts-...

Wasn't that proof using a paradox, though? Then that basically really proves the existence of paradoxes. It doesn't disprove the existence of all other kinds of statements, of course.

A statement 'x == 1' might be contextual (with a free variable x), but I think the theory is talking more about statements like

  for all x
  (x + 1)^ 2 == x^2 + 2*x + 1
which is true and does not depend on x. Contrast that with

  for all x
  x == 1
which is obviously false.

But the proof outlined in the article constructed a statement with a free variable, where a substitution with a certain value leads to a statement which is neither true, nor false. That means that the general statement in the proof's example is neither true nor false either.

Sorry about the awkward terminology, BTW, my engineering degree was a decade ago and in a language other than English.

Re: What Gödel Discovered

#215

Post by agency »

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…

This is not vital to the point you’re making but XSS has nothing to do with CSS.

Re: What Gödel Discovered

#216

Post by nmadden »

hvis wrote: post #214
nmadden wrote: post #191

Earlier quoted context omitted.

It’s not so much that they’re neither true nor false (they’re not paradoxes), but that they can be true in some interpretations and false in others. I wrote up some notes about this here: https://neilmadden.blog/2020/11/17/some-incomplete-thoughts-...

Wasn't that proof using a paradox, though? Then that basically really proves the existence of paradoxes. It doesn't disprove the existence of all other kinds of statements, of course. A statement 'x == 1' might be contextual (with a free variable x), but I think the theory is talking more about statements like for all x (x + 1)^ 2 == x^2 + 2*x + 1 which is true and does not depend on x. Contrast that with for all x x…

No, the statements in Gödel’s proofs are not paradoxes.

Substitutions of variables are not the same as interpretations. The interpretation tells you what the nonlogical symbols like *, +, ^, 1, 2, 3 etc mean.

Re: What Gödel Discovered

#217

Post by Liron »

Gehinnn wrote: post #205
Liron wrote: post #201

Earlier quoted context omitted.

> 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 f…

It's Turing complete if you let a human feed a bunch of clicks to proceed along the computation steps. [1] It also allows embedded JS (in some browsers), which is Turing complete. My point is that languages really quickly surpass the Turing complete barrier if you let them do fancy things. Godel realized that proving interesting statements about unbounded natural numbers is quite a fancy thing.

[1] https://stackoverflow.com/questions/2497146/is-css-turing-co...

Re: What Gödel Discovered

#218

Post by Liron »

green_on_black wrote: post #204
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.

Russel and Whitehead's system is well-engineered; that's why it doesn't prove a contradiction (presumably) while your badly engineered system does. The issue is that R&W made their system powerful enough that it's also incomplete, due to the fact that their system contains smartass statements like G that are hell-bent on creating paradoxes if given the chance.

Before Godel's time, people just didn't have enough experience with computers to realize that you have to deal with code injection attacks every time you try to build a powerful platform of any kind. In this case, Godel Numbering is the hack that allows code injection into a formal system that's supposed to just be highly insightful about properties of the infinite world of natural numbers.

Re: What Gödel Discovered

#219

Post by Liron »

agency wrote: post #215
Liron wrote: post #201

Earlier quoted context omitted.

> 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…

This is not vital to the point you’re making but XSS has nothing to do with CSS.

In this case the XSS vector is the fact that CSS allows running JavaScript in some browsers [1], but still, a lot of systems that are supposed to be weak and domain-specific are discovered to be Turing-complete, e.g. Conway's Game of Life.

[1] https://stackoverflow.com/questions/3607894/cross-site-scrip...

Re: What Gödel Discovered

#220

Post by legolas2412 »

redvenom wrote: post #118
jlokier wrote: post #43

Earlier quoted context omitted.

> being able to prove the CH is an incompleteness in ZFC. It's only incompleteness if the CH is true or false at the semantic level, "outside" of the logic system under discussion. But the CH may be neither true or false, semantically, if the meaning of "existence of a set whose cardinality is strictly between that of the integers and the real numbers" strictly depends on the axioms and logic used to define sets and…

This response is not quite right. "It's only completeness [...]" sentence does not make sense. CH is independent of ZFC, period, as proved by Cohen. Talking about 'semantic level' does not make sense. CH is an example of the incompleteness of ZFC. There are models of ZFC in which CH is true and models in which CH is false.

Trying to understand logic. What is a model, and how does it differ from theory?

For specific example, what is a model of ZFC? Is it just another theory, one which includes ZFC and few more axioms? Why not call it a derived theory or a subset theory?

Post reply on HN