5 ms·

> Godel's First Incompleteness Theorem isn't particularly interesting, can be proved fairly easily (to an average high-schooler)[1] I don't agree. The more mod

> Godel's First Incompleteness Theorem isn't particularly interesting, can be proved fairly easily (to an average high-schooler)[1] I don't agree. The more modern result of incomputability has certainly decreased the importance of the first incompleteness theorem, but the idea of unprovability is still important. And I don't think its a result that most high-schoolers can prove (with rigor). I would like to point out that your reference does not in fact even prove it (even informally). It only proves that there are incomputable functions. Such a function does allow you to make an unprovable statement, but that is an extra step at least as large as the given proof. There are a bunch of important details to the formal proof (as Godel wrote) that are not easy. The method to find a fixed point of the unprovable statement is definitely not something I could repeat from memory. Understanding why the "certain amount of elementary arithmetic" is one of the details I feel is important to understanding the theorem.

dvt 8y ago
> Such a function does allow you to make an unprovable statement, but that is an extra step at least as large as the given proof. Not at all. An unprovable statement is, in fact, exactly such a non-computable function. Supposing S is a non-computable function, all we need is a meta-logical jump from "computing S(x)" to "checking if the statement 'S(1) = 0' is correct" -- the latter of which is also trivially not possible (because S is not computable).
- ginnungagap 8y ago
  I'm confused by your statement, there's plenty of not computable functions for which we know whether S(1)=0 is true or not
  - dvt 8y ago
    We might know it†, but we can't prove it† (because proving it implies computing it). † The knowing is external to the system at hand, and the proving is internal to the system at hand. I go into detail about this in my blog posts linked above.
    - ginnungagap 8y ago
      Define (inside the system) the function S(1)=14 and S(n+1)=g(n) for all n\geq1 where g is any function which is not computable. I'm not convinced you can jump from "the function is uncomputable" to "the system cannot determine a single value of the function"
      - dvt 8y ago
        I see what you're saying, and yeah, I think you're right. You can construct a non-computable function S(n) that returns n when n is even, but does something non-computable when n is odd (kind of like f_bar). Of course, we're not really interested in these degenerate cases where n is even, but rather in the cases where we know that there's some kind of answer we can't prove in the system. I gave "S(1) = 0" as an example (you can replace '1' with whatever argument ends up being non-computable in your case, maybe S(2)).
    - niklasd 8y ago
      To add to what the other commenter said: Isn't the Busy beaver function uncomputable and we still can obtain some values for small n and prove that they are correct [1]? So I'm not sure it only applies to some special cases, I think several relevant incomputable problems might have this characteristic. [1] https://en.wikipedia.org/wiki/Busy_beaver#Non-computability https://en.wikipedia.org/wiki/Busy_beaver#Non-computability
- thethirdone 8y ago
  > An unprovable statement is, in fact, exactly such a non-computable function In any rigorous logic it is not. An unprovable statement is a non-existent value whereas the non-computable function is a mapping to a non-existant value. Sure there are ways of turning one into another (however there is not an isomorphism), but that does not make them the same. > all we need is a meta-logical jump from "computing S(x)" to "checking if the statement 'S(1) = 0' is correct" -- the latter of which is also trivially not possible (because S is not computable). As the other comments point out, you can't check just one case. f bar's definition makes it computable at a bunch of functions. The lecture you linked in the article actually has a follow up where it goes into showing that a formal language would be able to prove any computable function's value. It isn't hard, but it requires some thought.
  - dvt 8y ago
    > ... but that does not make them the same I need to check my undergrad metalogic notes, but I think they are "almost" the same. You might be right though, it's a very nuanced point you're making. IIRC, Godel and Lob used the "|- Prov(...)" (or Bew(...)) predicate to essentially make them the same.
plopilop 8y ago
The number of functions (or rather programs) is countable though, as we can think of them as Turing machine. A Turing machine is a set of the form (states, transitions). Given that a Turing machine has finite number states and transitions, there are countably many such machines. So indeed, we reach a contradiction, but the hypothesis was : > To make things even easier, we can just throw out programs that loop infinitely or don’t return a 1 or a 0 so the contradiction tells us that \bar f is not in this set. More specifically, \bar f may loop infinitely at some point, I guess it does loop when you feed \bar f to itself.

dvt 8y ago

> Such a function does allow you to make an unprovable statement, but that is an extra step at least as large as the given proof. Not at all. An unprovable statement is, in fact, exactly such a non-computable function. Supposing S is a non-computable function, all we need is a meta-logical jump from "computing S(x)" to "checking if the statement 'S(1) = 0' is correct" -- the latter of which is also trivially not possible (because S is not computable).

ginnungagap 8y ago
I'm confused by your statement, there's plenty of not computable functions for which we know whether S(1)=0 is true or not
- dvt 8y ago
  We might know it†, but we can't prove it† (because proving it implies computing it). † The knowing is external to the system at hand, and the proving is internal to the system at hand. I go into detail about this in my blog posts linked above.
  - ginnungagap 8y ago
    Define (inside the system) the function S(1)=14 and S(n+1)=g(n) for all n\geq1 where g is any function which is not computable. I'm not convinced you can jump from "the function is uncomputable" to "the system cannot determine a single value of the function"
    - dvt 8y ago
      I see what you're saying, and yeah, I think you're right. You can construct a non-computable function S(n) that returns n when n is even, but does something non-computable when n is odd (kind of like f_bar). Of course, we're not really interested in these degenerate cases where n is even, but rather in the cases where we know that there's some kind of answer we can't prove in the system. I gave "S(1) = 0" as an example (you can replace '1' with whatever argument ends up being non-computable in your case, maybe S(2)).
  - niklasd 8y ago
    To add to what the other commenter said: Isn't the Busy beaver function uncomputable and we still can obtain some values for small n and prove that they are correct [1]? So I'm not sure it only applies to some special cases, I think several relevant incomputable problems might have this characteristic. [1] https://en.wikipedia.org/wiki/Busy_beaver#Non-computability https://en.wikipedia.org/wiki/Busy_beaver#Non-computability
thethirdone 8y ago
> An unprovable statement is, in fact, exactly such a non-computable function In any rigorous logic it is not. An unprovable statement is a non-existent value whereas the non-computable function is a mapping to a non-existant value. Sure there are ways of turning one into another (however there is not an isomorphism), but that does not make them the same. > all we need is a meta-logical jump from "computing S(x)" to "checking if the statement 'S(1) = 0' is correct" -- the latter of which is also trivially not possible (because S is not computable). As the other comments point out, you can't check just one case. f bar's definition makes it computable at a bunch of functions. The lecture you linked in the article actually has a follow up where it goes into showing that a formal language would be able to prove any computable function's value. It isn't hard, but it requires some thought.
- dvt 8y ago
  > ... but that does not make them the same I need to check my undergrad metalogic notes, but I think they are "almost" the same. You might be right though, it's a very nuanced point you're making. IIRC, Godel and Lob used the "|- Prov(...)" (or Bew(...)) predicate to essentially make them the same.

plopilop 8y ago

The number of functions (or rather programs) is countable though, as we can think of them as Turing machine. A Turing machine is a set of the form (states, transitions). Given that a Turing machine has finite number states and transitions, there are countably many such machines. So indeed, we reach a contradiction, but the hypothesis was : > To make things even easier, we can just throw out programs that loop infinitely or don’t return a 1 or a 0 so the contradiction tells us that \bar f is not in this set. More specifically, \bar f may loop infinitely at some point, I guess it does loop when you feed \bar f to itself.