8 ms·

What Gödel Discovered (2020)

86 points by behnamoh 4y ago

buggythebug 4y ago
- behnamoh 4y ago
  Not the author, but Lisp is very much relevant. His code is available in Clojure, which is a nice modern language.
  - ngcc_hk 4y ago
    Really? Any GitHub?
    - stopachka 4y ago
      This was an accompaniment I wrote, to encode and decode godel numbers: https://github.com/stopachka/godel-numbers https://github.com/stopachka/godel-numbers
  - iLemming 4y ago
    > Lisp is very much relevant Lisp will always be relevant since it's based on math. For it to become irrelevant we need to discover or invent a completely new kind of math, and we simply haven't evolved to that point.
- ngcc_hk 4y ago
  It is quite hard to understand Godel language or vm. We have a whole book try to get to the bottom of this. Lisp being God’s programming language (which God might use php but that is another story) it should have a go.
- mxkopy 4y ago
  In what manner had LISP hurt you ?
- wudangmonk 4y ago
  My issue is with Kurt Gödel, he did not use Rust therefore his "proof" not correct. Its 2022, why are we still using these old and antiquated languages?.
ngcc_hk 4y ago
It is a virtual machine he built. Btw any reason why Russel cannot detect this barber cannot shave himself who does not shave any one who shave himself? He should not known(without this) that self referral has an issue and hence if one apply his principal Mathematica on itself it is doom. Why he does not think that way given he got this?
- Kranar 4y ago
  The barber's paradox can not be expressed in Principia Mathematica (PM). PM defines a theory of sets, classes, 2-classes, 3-classes, etc... so that members of an N-class can only contain elements that are of type K-classes where K < N. The barber's paradox can not be formulated in such a theory. Consequently PM does not have an issue with the barber's paradox. PM is incomplete in that there are truths that can be expressed but can not be proven, but there are no known paradoxes/inconsistencies. From a programming point of view PM is like a statically typed programming language. If something type checks in PM then it's correct. But as anyone who programs in Rust can tell you, sometimes you know that something is correct but it's a pain to find a way to express it in the language's rigid type system and sometimes it's simply impossible to express that a program is correct using the language's rigid type system. That's the problem that PM has and the sense in which PM is incomplete.
sedivy94 4y ago
This might be a repost but it’s one of my favorites. Thank you!
sdwr 4y ago
Easier to spot the trick when it's all written in code. "There-is" is a huge overreach from a computational perspective, opens the door for "this sentence is false" type logical knots and unbounded complexity. I know its the first lesson in discrete math, but "there exists a _" makes no sense from an algorithmic perspective. How do you find it?
- KhoomeiK 4y ago
  Not an expert but the proof is in fact entirely constructive and witnesses to the existential statement are constructible. https://math.stackexchange.com/questions/448527/are-the-g%C3%B6dels-incompleteness-theorems-valid-for-both-classical-and-intuitionis https://math.stackexchange.com/questions/448527/are-the-g%C3...
- Kranar 4y ago
  There's no overreach whatsoever and you can eliminate "there exists" altogether without any loss of expressivity. "There exists a number X such that P(X) is true." is nothing more than a short hand for "It is false that for all numbers X, P(X) is false." In other words, if you accept that it's possible to reason about "for all" then you must accept that it's possible to reason about "there exists" since all "there exists" does is assert that a property is not false for every number.
  - thrown_22 4y ago
    I don't think OP was saying that "for all" is any more meaningful from a computational perspective than "there exits". The point is that both are higher order functions that return an answer for any function on all natural numbers (or inputs in a more general setting).
    - Kranar 4y ago
      In that case I'd argue the objection has nothing to do with "for all" or "there exists" but rather reasoning about infinite sets.
dang 4y ago
Related: What Gödel Discovered - https://news.ycombinator.com/item?id=25115746 https://news.ycombinator.com/item?id=25115746 - Nov 2020 (259 comments)
deleted 4y ago
[deleted]

86 points by behnamoh 4y ago

behnamoh 4y ago
Not the author, but Lisp is very much relevant. His code is available in Clojure, which is a nice modern language.
- ngcc_hk 4y ago
  Really? Any GitHub?
  - stopachka 4y ago
    This was an accompaniment I wrote, to encode and decode godel numbers: https://github.com/stopachka/godel-numbers https://github.com/stopachka/godel-numbers
- iLemming 4y ago
  > Lisp is very much relevant Lisp will always be relevant since it's based on math. For it to become irrelevant we need to discover or invent a completely new kind of math, and we simply haven't evolved to that point.
ngcc_hk 4y ago
It is quite hard to understand Godel language or vm. We have a whole book try to get to the bottom of this. Lisp being God’s programming language (which God might use php but that is another story) it should have a go.
mxkopy 4y ago
In what manner had LISP hurt you ?
wudangmonk 4y ago
My issue is with Kurt Gödel, he did not use Rust therefore his "proof" not correct. Its 2022, why are we still using these old and antiquated languages?.

It is a virtual machine he built. Btw any reason why Russel cannot detect this barber cannot shave himself who does not shave any one who shave himself? He should not known(without this) that self referral has an issue and hence if one apply his principal Mathematica on itself it is doom. Why he does not think that way given he got this?

Kranar 4y ago
The barber's paradox can not be expressed in Principia Mathematica (PM). PM defines a theory of sets, classes, 2-classes, 3-classes, etc... so that members of an N-class can only contain elements that are of type K-classes where K < N. The barber's paradox can not be formulated in such a theory. Consequently PM does not have an issue with the barber's paradox. PM is incomplete in that there are truths that can be expressed but can not be proven, but there are no known paradoxes/inconsistencies. From a programming point of view PM is like a statically typed programming language. If something type checks in PM then it's correct. But as anyone who programs in Rust can tell you, sometimes you know that something is correct but it's a pain to find a way to express it in the language's rigid type system and sometimes it's simply impossible to express that a program is correct using the language's rigid type system. That's the problem that PM has and the sense in which PM is incomplete.

sedivy94 4y ago

This might be a repost but it’s one of my favorites. Thank you!

sdwr 4y ago

Easier to spot the trick when it's all written in code. "There-is" is a huge overreach from a computational perspective, opens the door for "this sentence is false" type logical knots and unbounded complexity. I know its the first lesson in discrete math, but "there exists a _" makes no sense from an algorithmic perspective. How do you find it?

KhoomeiK 4y ago
Not an expert but the proof is in fact entirely constructive and witnesses to the existential statement are constructible. https://math.stackexchange.com/questions/448527/are-the-g%C3%B6dels-incompleteness-theorems-valid-for-both-classical-and-intuitionis https://math.stackexchange.com/questions/448527/are-the-g%C3...
Kranar 4y ago
There's no overreach whatsoever and you can eliminate "there exists" altogether without any loss of expressivity. "There exists a number X such that P(X) is true." is nothing more than a short hand for "It is false that for all numbers X, P(X) is false." In other words, if you accept that it's possible to reason about "for all" then you must accept that it's possible to reason about "there exists" since all "there exists" does is assert that a property is not false for every number.
- thrown_22 4y ago
  I don't think OP was saying that "for all" is any more meaningful from a computational perspective than "there exits". The point is that both are higher order functions that return an answer for any function on all natural numbers (or inputs in a more general setting).
  - Kranar 4y ago
    In that case I'd argue the objection has nothing to do with "for all" or "there exists" but rather reasoning about infinite sets.

dang 4y ago

Related: What Gödel Discovered - https://news.ycombinator.com/item?id=25115746 https://news.ycombinator.com/item?id=25115746 - Nov 2020 (259 comments)

deleted 4y ago

[deleted]