4 ms·
> 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
by 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.