"But it seems like any sentence can be laid upon mathematical structure. It doesn’t matter that Godel found/made one that speaks of truth outside the formalism. Any and every sentence is possible right? Just change the word and letter numberings to different primes. ... It seems like I could enco...
See this thread for an outline of all the actually crucial points regarding the incompleteness theorems. Indeed, Godel coding is not at all crucial, and is simply irrelevant in some cases. Also, the fact that one needs to recognize that provability in a given formal system can be expressed as an FOL statement about naturals/strings is precisely why I think it is pedagogically better to use TC rather than PA−/Q as an example base theory, so that Godel coding is unnecessary.
How can I understand when compared to the honeycomb example, where the specific mathematical structure (hexagonal top with rounded base) is doing the explaining? The number 6 is intrinsic. Nothing seems intrinsic if “(“ could be 7 or 8 and “)” v.v. I don’t think Godel’s proofs depend on that choice. Don’t I need some necessary connection somewhere to make any meta mathematical claim? (Still hung up on what role encoding is playing I guess)
@user21820 Thanks for the relevant material. And that encoding may not be the only way to understand.
@Hypnosifl: By the way, you can also see from the linked post that, contrary to your last sentence, the generalized incompleteness theorems relativize, meaning that they apply even to uncomputable formal systems. That is, you can replace "program" in that post by "program using O" for any fixed oracle O. For example, let S be TC plus all true Π1-statements about strings. Then S can reason about programs that use the halting oracle H, and S also has a proof verifier program using H. Thus by the linked proof, S will be unable to prove or disprove some statement about a program that uses H.
It's not a big issue though; for the general public it may be okay not to talk about uncomputable formal systems since they probably do not even grasp ordinary formal systems. It's just worth noting. =)
@JKusin: You're welcome. If you want to understand what is the deal with Godel encoding, in my opinion you must first understand the computability-based proof I gave, and then you can see that for certain kinds of formal system S you need encoding if you want to show "S can reason about programs". That's essentially the only place you need the encoding.
@user21820 - I was thinking specifically of the original form of the incompleteness theorem which was about arithmetic--when you relativize it to uncomputable systems, presumably it's not about finding a theorem in first-order arithmetic that the system cannot prove, is it something else like second-order arithmetic, or does it no longer involve an arithmetical Godel statement at all, maybe more like a proof that any oracle machine must have its own halting problem? (or at least closely related to that idea, some reasonably straightforward consequence of it perhaps)
It's still first-order arithmetic! The statement the S in my above comment cannot prove is a Π2-statement about strings! I have no idea what you're talking about in the rest of your comment. Also, I hope you are not the one who downvoted my Math SE post. It seems to me that Phil SE is quite hostile towards proper logic in general, and this is why I rarely contribute here.
@user21820 No, I didn't downvote your other answer. As for your comment, I don't understand how this could apply to arbitrary non-computable oracle machines--isn't there an oracle machine that can execute the ω-rule along with the ordinary inference rules of first-order logic, which according to the site I linked in my other answer is enough to evaluate the truth-value of every possible WFF in first-order arithmetic? Or are you only saying Godel can be relativized to oracle machines less powerful than this?
@Hypnosifl "he came up with a way of proving by construction that for any metamathematical statement about provability within an axiomatic system, one could find a corresponding arithmetical statement S such that S will be true if and only if the metamathematical statement is true”. This makes me think of Searle's dropping a hammer can be a computation, and which computation is up to us. Does it compute G, the duration of a musical note, the number 1? I feel like in both cases nothing necessary is carrying us from object to meta. There’s too much choice involved. (1/2)
@Hypnosifl Like no single number or specific finite collection of numbers is necessary to make a Godel construction, as any other set of numbers would work (instead of 1-12 for ~, (,), and 17+ for variables, etc) Therefore anything meta is just as good as anything else almost. (2/2)
@Hypnosifl: No. What I wrote was correct, and it really applies to arbitrary oracle programs. Your formal system that has the ω-rule is actually nothing more than Th(ℕ), and it has a proof verifier program that uses the ω-th Turing jump (but this ω is unrelated to the ω-rule), which I shall subsequently denote as H[ω]. But Th(ℕ) cannot reason about programs that use H[ω]! This is exactly why the incompleteness theorem fails to apply to Th(ℕ), as expected.
@user21820 - As I said, I'm asking specifically about statements in first-order arithmetic--are you saying that there's a statement S in first-order arithmetic that corresponds to an assertion about "programs that use the ω-th Turing jump", and therefore that this oracle machine can't judge the truth-value of S? Wouldn't that contradict the claim that this oracle machine is powerful enough to derive all of true arithmetic, which involves assigning the correct truth-value to every WFF in first-order arithmetic, including S?
@Hypnosifl: I don't think you understood the proof. Read the linked post carefully, and replace every "program" in that post by "program using O" (as I said above), and you will not find an error. Then observe that you cannot apply the theorem to Th(ℕ) because you cannot demonstrate a suitable translation of the relevant kind of statements about programs using O that satisfies the stated condition "Th(ℕ) can reason about programs using O". It is not up to me to provide such to you; it's up to you.
In contrast, the example S that I gave above (TC plus all true Π1-statements about strings) does satisfy "S can reason about programs using H", and it is easy to show the required translation (because an execution of a program using H is just a finite trace where each step may have an associated call to H). In particular, "P halts on X and outputs Y" translates to a Σ2-statement about strings. If you can't figure out the details, let me know.
@user21820 Honestly I'm not sure if I have the background knowledge to follow the proof or the motivation right now, I'm just asking questions to try to clarify what you're saying in layman's terms for the purpose of correcting my answer, not arguing for any kind of error in your proof. When you say "you cannot apply the theorem to Th(ℕ)", does that mean the proof does not claim there is any WFF in first-order arithmetic that this machine is unable to prove? BTW, when I asked how the proof could "apply" to arbitrary machines I didn't mean it was making incorrect claims about these machines.
@Hypnosifl: You only need to have basic knowledge of programming and FOL to understand the first half of that linked post up to "explicit independent sentence". Sorry, there is no such thing as "layman terms" when it comes to incompleteness. Since my proof is correct, it obviously will not claim that Th(ℕ) is unable to prove some true arithmetical sentence. As I said, the incompleteness theorem applies to a system T if you can provide a suitable translation of the relevant kind of statements about programs that satisfies the stated conditions including "T can reason about programs".
"Program" can be replaced by "program using O" for any fixed oracle, and this does not affect the proof at all. In CS we say that the proof relativizes. You are missing the point that the incompleteness theorem can only be applied if two conditions both hold: (1) T has a proof verifier program; (2) T can reason about programs. If you make O powerful enough so that you satisfy (1), you may very well be unable to satisfy (2).
Maybe you don't get what it means for T to prove "The program P halts on input X.". Full details: Let Prog be the set of programs. Take any V∈Prog. Let Prov(φ) ≡ ∃x∈Str ( V(φ,x) = 1 ), for any φ∈Str. Take any out∈Prog×Str^2→Str and neg∈Str→Str such that ∀P∈Prog ∀X,Y∈Str ( P halts on X and outputs Y ⇒ Prov(out(P,X,Y)) ∧ ∀Z∈Str ( Z ≠ Y ⇒ Prov(neg(out(P,X,Z))) ) ). Then the linked proof of the Rosser incompleteness theorem shows ∃P∈Prog ∃X,Y∈Str ( Prov(out(P,X,Y)) ⇔ Prov(neg(out(P,X,Y))) ).
Oh I forgot to say that out,neg must be computable by a program. For the example system S I gave above, such functions out,neg exist, so the general incompleteness theorem applies to S even though S is not computable.
Discussion on answer by Hypnosifl: Ne…
Discussion on answer by Hypnosifl: Ne…