4 ms·

The halting problem applying to all systems is not the same as the halting problem being relevant to all claims about halting of systems (unless those claims ca

The halting problem applying to all systems is not the same as the halting problem being relevant to all claims about halting of systems (unless those claims can also be rigorously proven to match the conditions of the generalized halting problem first). I.e. I'm not trying to say the halting problem does not apply to these systems in general, I'm saying it doesn't apply to the specific claims being made about these systems. As an example of the type of thing I'm saying: one can show an algorithm which multiplies a real number by 2 cannot guarantee the output will be an even number for all inputs. Separately, one can create and prove a algorithm which takes an integer number greater than 0 and multiplies it by 2 will always meet the very same guarantee. In this scenario it clearly did not matter the first proof of lack of guarantee applied to all algorithms using real numbers, the more restricted subset of real numbers could make a guarantee. Specifically to the halting problem and Bend again: It's not about an algorithm which can definitely answer yes or no for any program+input. The given claim/condition from Bend is simpler: it blocks mistakes (because it only accepts provably valid proofs, not because it can prove every input one way or the other). > Yes, but that's not what's being claimed. My objection was to the original claim, not this restatement. It blocks AI mistakes, it only accepts ones able to be proven. Nothing in that claim says it will prove every input one way or the other, that's just an assumption which you rightly showed could not be a reasonable interpretation of the title. It might also be prudent to ask the author if they really mean they interpretation you take before declaring the problem as beginner's lacking understanding of a foundational theory in computer science. > No non-trivial computer program is "feasibly provable." That's what the Halting Problem makes impossible. What's your definition of "non-trivial" here and how did you derive that definition as the one used by the claim? As a side note, I have no affiliation or ecen prior knowledge of the project/author prior to reading this post, I just get nerd sniped by overly broad claims about the halting problem.

lutusp 8d ago
> It blocks AI mistakes, it only accepts ones able to be proven. This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation. > It might also be prudent to ask the author if they really mean they interpretation you take How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful. > What's your definition of "non-trivial" here and how did you derive that definition as the one used by the claim? I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem .
- zamadatix 7d ago
  > This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation. I disagree, which is why I added all of the additional commentary you appear to have ignored to restate your original claim instead. I'm not sure why I should restate my response to these points when they're still available and awaiting response above. > How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful. When someone's words on a project as complicated as this seems to violate the basic foundations of computer science it's both your problem & disrespectful to claim you know for certain the problem is because it's a common beginners mistake. This may be something we cannot come to an agreement on morally, but I suppose it won't really matter for the rest of the mathematical conversation which continues below. > I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem . Wikipedia is a poor source to cite, but when I follow it I see no claim or definition by Turing for what non-trivial is. I see claim of what Rice meant by non-trivial in their eponymous theorem in 1951, but that's neither from 1936 nor a relevant definition for the current discussion so I must assume you mean somewhere else in Turing's actual paper I'd need to check. Which takes us to the actual 1936 paper rather than Wikipedia's summary https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf. I see 3 mentions of triviality, none of which appear to give a definition of what a non-trivial provably haltable example is: 1. Discussion of the remainder of the theorem itself being trivial [on page 31 of his paper, page 260 of the journal] 2. Since CC_0 is already been shown provable the conditional proof of the A(M)->CC_0 is trivial by the rules of implication [p32, 261 of the journal] 3. A trivial replacement of the variable naming scheme allows translation between the two notations without changing the calculus of them. [p34, 263 of the journal] None of these seem to define what a non-trivially provable program (Turing Machine/Algorithm) is in context of the halting problem, so I again ask can you tell me where and what actual definition in Turing's actual 1936 paper you are using to define what a non-trivial program is so that I may apply this definition to the current conversation? As another aside, one of my favorite "simplest" examples of a non-trivially provable program we know never halts despite the general case result of the halting problem: for every group of positive integers (a,b,c,n) with n > 2: if a^n + b^n = c^n: halt To prove this never halts you have to prove Fermat's last theorem. Which we have, and so we know this must never halt as you iterate infinitely over the positive integers, but it took one of the most complicated mathematical proofs known to show it. There are certainly definitions of non-trivial where this is still considered trivial, but I'm at a loss to what part of Turing's paper gives such a definition.

lutusp 8d ago

> It blocks AI mistakes, it only accepts ones able to be proven. This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation. > It might also be prudent to ask the author if they really mean they interpretation you take How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful. > What's your definition of "non-trivial" here and how did you derive that definition as the one used by the claim? I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem .

zamadatix 7d ago
> This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation. I disagree, which is why I added all of the additional commentary you appear to have ignored to restate your original claim instead. I'm not sure why I should restate my response to these points when they're still available and awaiting response above. > How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful. When someone's words on a project as complicated as this seems to violate the basic foundations of computer science it's both your problem & disrespectful to claim you know for certain the problem is because it's a common beginners mistake. This may be something we cannot come to an agreement on morally, but I suppose it won't really matter for the rest of the mathematical conversation which continues below. > I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem . Wikipedia is a poor source to cite, but when I follow it I see no claim or definition by Turing for what non-trivial is. I see claim of what Rice meant by non-trivial in their eponymous theorem in 1951, but that's neither from 1936 nor a relevant definition for the current discussion so I must assume you mean somewhere else in Turing's actual paper I'd need to check. Which takes us to the actual 1936 paper rather than Wikipedia's summary https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf. I see 3 mentions of triviality, none of which appear to give a definition of what a non-trivial provably haltable example is: 1. Discussion of the remainder of the theorem itself being trivial [on page 31 of his paper, page 260 of the journal] 2. Since CC_0 is already been shown provable the conditional proof of the A(M)->CC_0 is trivial by the rules of implication [p32, 261 of the journal] 3. A trivial replacement of the variable naming scheme allows translation between the two notations without changing the calculus of them. [p34, 263 of the journal] None of these seem to define what a non-trivially provable program (Turing Machine/Algorithm) is in context of the halting problem, so I again ask can you tell me where and what actual definition in Turing's actual 1936 paper you are using to define what a non-trivial program is so that I may apply this definition to the current conversation? As another aside, one of my favorite "simplest" examples of a non-trivially provable program we know never halts despite the general case result of the halting problem: for every group of positive integers (a,b,c,n) with n > 2: if a^n + b^n = c^n: halt To prove this never halts you have to prove Fermat's last theorem. Which we have, and so we know this must never halt as you iterate infinitely over the positive integers, but it took one of the most complicated mathematical proofs known to show it. There are certainly definitions of non-trivial where this is still considered trivial, but I'm at a loss to what part of Turing's paper gives such a definition.