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

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

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

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.

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"

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)).

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