I really don't wish to belabour the primes vs. ASCII discussion because: it really is but a trivial implementation detail. You want to have a bijection between formulas and the natural numbers (such that certain operations on formulas, such as composition and extraction of subformulas can be computed). Primes do that, as do ASCII sequences.
> From that, Godel's theorem is an elementary proof by reductio: if arithmetic were decidable, you could solve the halting problem by translating the question of whether or not a program P halts into the question of whether a number N describes a program that halts.
I think you again misunderstand the full implications of Gödel's first theorem.
Gödel's first theorem:
> Any theory of arithmetic that is sufficiently strong and consistent is incomplete.
What you have just proven is a corollary of that theorem, but actually a weaker result:
> Arithmetic truth is not decidable
Gödel's theorem works even if PA is not sound, but merely consistent. And it also works for potential other, unsound theories of arithmetic, as long as they're strong enough and consistent.
Your proof via Turing machines does not: if PA is unsound, and if from PA you derive that the "impossible" program halts (or does not halt), it doesn't tell you anything, because the conclusions of PA can't be trusted. Therefore you can't derive the necessary contradiction.
Again, this matters not only philosophically, but also technically because "If PA is sound, it is incomplete* can't be written as a statement of arithmetic, but "If PA is consistent, it is incomplete" can, and this is the necessary link between the first and the second theorem.
---
I think there's a consistent thread in your comments where you think things are "obvious" and "true" because we can observe them somehow physically (e.g. your assertion that the Halting Problem is "not grounded in axioms, but in physics" - to which I would again object, but let's not go into that), but this is not how mathematics (and logic) work.
It's fine if you don't care about it personally, but Gödel's theorems have deep mathematical and philosophical implications about systems of reasoning which are not dependent on our physical world.
But I don't think this discussion will go anywhere.
> I really don't wish to belabour the primes vs. ASCII discussion because: it really is but a trivial implementation detail
OK, so we agree.
> What you have just proven is a corollary of that theorem, but actually a weaker result: > Arithmetic truth is not decidable
No. My argument does not depend on the soundness of the system. All it depends on is that the system be able to do arithmetic correctly, so it requires consistency (because it needs to be able to identify e.g. "1+1=3" as false), but not soundness. You can throw in as many additional axioms as you like, including false ones. As long as the false axioms do not destroy the system's ability to correctly do arithmetic the proof holds. And this is true for Godel's proof as well.
[UPDATE] I just realized that what I wrote earlier:
> Note that you essentially get soundness "for free"
is misleading at best, and probably just flat-out wrong. I'm actually not quite sure what I was thinking when I wrote that. It might have been something along the lines of, "The fact that we can build TMs is evidence that the mathematical models of TM's are in some sense 'true'", but this is obviously not on point. So I retract that part of my argument.
[END UPDATE]
> systems of reasoning which are not dependent on our physical world
You cannot have systems of reasoning that are not dependent on our physical world. Reasoning is a physical process conducted by physical systems. Mathematicians are physical systems. Symbols are physical things: patterns of ink on paper, or electrons moving around, or vibrations in a medium. Any claim about a system of reasoning is necessarily a claim about a physical system. Platonic ideals do not actually exist, not even in math.
We can imagine situations where this is not the case, but these are counterfactual. We can think about "systems of reasoning which are not dependent on our physical world" just as we can think about Santa Claus or Darth Vader. We can even make factual claims about them, e.g. "Santa Claus has a beard" or "Darth Vader is Luke Skywalker's father". Claims about "systems of reasoning which are not dependent on our physical world" have exactly the same ontological status as claims about Santa Claus and Darth Vader.
The reason that we care about "systems of reasoning" at all is that some "systems of reasoning" correspond to physical reality in ways that give us leverage to navigate that reality more effectively. Absent that, the entire enterprise would be a complete waste of time.
> consistency (because it needs to be able to identify e.g. "1+1=3" as false)
that's soundness, not consistency.
You can build consistent theories of arithmetic in which 1+1=3 is true. The easiest model for such a theory is a structure with a single element.
But that's maybe a bad example, as it's too weak for Gödel's theorems to apply to it. So let's consider instead models of Robinson arithmetic. There are models of Robinson arithmetic, for which the sentence "for all x, Sx != x" is false,[0] even though we clearly want it to be true in the natural numbers. So if we add the axiom "there is an x for which Sx = x" to Robinson arithmetic, we get a theory which is arithmetically unsound, so whatever we derive from it, does not readily apply to Turing machines. Yet, Gödel's theorems apply to this theory just as well (assuming it is consistent, which we can't prove, same as we can't prove it for PA).
I'll leave it at that. We're talking at cross-purposes, since we can't even get terminology straight.
> So let's consider instead models of Robinson arithmetic.
OK.
> There are models of Robinson arithmetic, for which the sentence "for all x, Sx != x" is false
OK. So?
> even though we clearly want it to be true in the natural numbers.
Who is "we"?
> if we add the axiom "there is an x for which Sx = x" to Robinson arithmetic, we get a theory which is arithmetically unsound
OK. So?
> whatever we derive from it, does not readily apply to Turing machines
Why do you think that this does not "readily apply to Turing machines"? Turing machines do not natively do arithmetic. They just write symbols to a tape according to a state transition table.
Do you really believe that writing a proof checker for Robinson arithmetic, with or without your new axiom, is different in any salient way than writing a proof checker for PA?
(And would you please consider the possibility that I might not be a complete idiot?)
> (And would you please consider the possibility that I might not be a complete idiot?)
I do not believe you're an idiot. As a matter of fact, I think you're probably a quite intelligent individual that knows a lot about many topics. Looking at your resume, I do get a strong sense that you're a much better engineer that I ever will be, for example.
I do however think that, when it comes to this topic, you're out of your depth, since you don't seem to be aware of concepts and ideas that are taught in a very introductory course on mathematical logic.
I don't even think you have digested many of the points I've made in my last post - or in previous ones. It seems like you're refusing to engage, opting instead for picking individual sentences apart as if they were devoid of context.
I encourage you to take some time to actually study Gödel's theorems, with all their nuances and the proper historical, mathematical and logical context. The books by Peter Smith seem like a good start: https://www.logicmatters.net/igt/ - I have only read the long one (which I've linked to previously above), but I suppose the short one should be good too.
(And maybe consider that I'm not quite dumb, either. And that mathematical logic is a topic I know a thing or two about.)
It's not your understanding of mathematical logic that I'm questioning, it's your understanding of the theory of computation. In particular, you didn't answer my question:
> Do you really believe that writing a proof checker for Robinson arithmetic, with or without your new axiom, is different in any salient way than writing a proof checker for PA?
> Do you really believe that writing a proof checker for Robinson arithmetic, with or without your new axiom, is different in any salient way than writing a proof checker for PA?
No, and this has exactly nothing to do with my point.
Then why did you bring up RA at all? You must think there is some salient difference between RA and PA with respect to my proof or (I presume) you would not have brought it up. What is it?
For that matter, what is the point you are trying to make? You originally wrote [1]:
> A theory Γ is said to be complete whenever for all sentences we have either Γ ⊨ φ or Γ ⊨ ¬φ.
If you recall, at the time I thought this was a simple mistake on your part, and that what you really meant was "Γ ⊢ φ or Γ ⊢ ¬φ", not "Γ ⊨ φ or Γ ⊨ ¬φ". But you never conceded this. So I'm going to ask you again, is that really what you meant? Because that is not the sense in which the term "completeness" is used in Goedel's incompleteness theorem. The word "complete" is used there to mean syntactic completeness. To quote Wikipedia [2]:
"A set of axioms is (syntactically, or negation-) complete if, for any statement in the axioms' language, that statement or its negation is provable from the axioms (Smith 2007, p. 24). THIS IS THE NOTION RELEVANT for Gödel's first Incompleteness theorem. It is NOT TO BE CONFUSED WITH SEMANTIC COMPLETENESS, which means that the set of axioms proves all the semantic tautologies of the given language." [emphasis added]
I'm trying to give you the benefit of the doubt here, but you really do appear to be confused on this point, particularly since you keep talking about soundness, which is a semantic property, not a syntactic one.
> From that, Godel's theorem is an elementary proof by reductio: if arithmetic were decidable, you could solve the halting problem by translating the question of whether or not a program P halts into the question of whether a number N describes a program that halts.
I think you again misunderstand the full implications of Gödel's first theorem.
Gödel's first theorem: > Any theory of arithmetic that is sufficiently strong and consistent is incomplete.
What you have just proven is a corollary of that theorem, but actually a weaker result: > Arithmetic truth is not decidable
Gödel's theorem works even if PA is not sound, but merely consistent. And it also works for potential other, unsound theories of arithmetic, as long as they're strong enough and consistent.
Your proof via Turing machines does not: if PA is unsound, and if from PA you derive that the "impossible" program halts (or does not halt), it doesn't tell you anything, because the conclusions of PA can't be trusted. Therefore you can't derive the necessary contradiction.
Again, this matters not only philosophically, but also technically because "If PA is sound, it is incomplete* can't be written as a statement of arithmetic, but "If PA is consistent, it is incomplete" can, and this is the necessary link between the first and the second theorem.
---
I think there's a consistent thread in your comments where you think things are "obvious" and "true" because we can observe them somehow physically (e.g. your assertion that the Halting Problem is "not grounded in axioms, but in physics" - to which I would again object, but let's not go into that), but this is not how mathematics (and logic) work.
It's fine if you don't care about it personally, but Gödel's theorems have deep mathematical and philosophical implications about systems of reasoning which are not dependent on our physical world.
But I don't think this discussion will go anywhere.