4 ms·

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

by lutusp 14d 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 ... This is not a topic open to debate, it is a statement of fact. I strongly recommend that you learn this topic, and the topics of mathematics and logic, where some statements can be proven true or false without ambiguity. The Turing Halting Problem applies to all Turing-complete environments. The program under discussion meets the criterion. AI meets the criterion. Lean meets the criterion. > There are certainly definitions of non-trivial ... This is a logical fallacy known as "Logic Chopping" : https://iep.utm.edu/fallacy/#Logic%Chopping https://iep.utm.edu/fallacy/#Logic%Chopping > where this is still considered trivial, but I'm at a loss to what part of Turing's paper gives such a definition. Yes, I can see that, but that's not what this discussion is about. Read this before posting again: https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem Dozens of online articles on this topic, make the same point in the same way. None of them digress into logical fallacies. > This may be something we cannot come to an agreement on morally ... "Morally", really? Another logical fallacy, another digression, and not the topic.

zamadatix 13d ago
If you wish to say you have a counterclaim to the idea mistakes can be blocked regardless if every program can be proven to halt which is based in mathematical reasoning you must be able to state or produce the claim in the actual mathematical reasoning itself (or at least a link to the specific math directly relevant to the claim), not an English text summary of an entire paper/problem on Wikipedia. Anything less is not mathematical reasoning. I'm unable to say more at this point as I can only assume you will continue to use that as a chance to quote and discuss everything but actual mathematics.
- lutusp 12d ago
  > If you wish to say you have a counterclaim to the idea mistakes can be blocked regardless if every program can be proven to halt which is based in mathematical reasoning you must be able to state or produce the claim in the actual mathematical reasoning itself ... This is not a philosophy discussion, and Alan Turing already plowed this ground. The original claim "Bend - a language that blocks AI mistakes via proof [...]" is unsupportable. > ... if every program can be proven to halt ... But that's not so. You have introduced a qualifier that is known to be false. > ... a chance to quote and discuss everything but actual mathematics. Yes, I agree -- you should stop doing that. I keep referring to the original technical reason the original claim is unsupportable, others keep raising objections without trying to think through their positions. It's not as though the Halting Problem is on the Millennium Prize Problem list, open to contradiction/reconsideration by some future challenge. It's a theorem, not a conjecture.
  - zamadatix 12d ago
    I've given notes of where in Turing's paper any type use triviality could be found, with direct page citations of the relevant original math, along with the mathematical reasons it doesn't have anything to do with the plain English statements you are making. This effort was a kindness done in good faith that I might find said mathematical definition of non-triviality for the halting problem somewhere in the paper, not something needed to show your claim devoid of a shown basis in mathematical reasoning so far. That much is apparent by the lack of a single mathematically defined claim specified by any of your messages. That said, if you'd like me to formally show what e.g. the triviality in the rules of implication Turing was talking about are in a purely mathematical form I'd be glad to state with no English commentary out of good faith as well. This would seem a waste of time unless that's the part of the paper you think the definition of non-triviality can be sourced, but at least I'd at last have a clear mathematical claim from you to discuss. It is now your opportunity to make a mathematical claim, of which proof by assertion this paper should apply because it proves something in general is not.
    - lutusp 12d ago
      > That much is apparent by the lack of a single mathematically defined claim specified by any of your messages. I posted the Turing Halting Problem Wikipedia page. It describes a theorem, not a conjecture that I need to prove, which shows the original poster's claim is contradicted by established facts. Let me put it this way. If I say, "There are an infinity of primes," will you reply, saying, "I disagree"? That position would be equally appropriate -- that is to say, not appropriate at all. Am I obliged to prove the infinity of primes by generating an infinity of candidate integers and prove that some of them are prime? No, and by the same token, I'm not obliged to reply to your naive demands and teach you why the Halting Problem falsifies the claim made by the original poster. That is not my responsibility, it is yours. In mathematics, some things are conjectures -- the Millennium Challenge problems, for example. Others are theorems, meaning established truths, beyond dispute. Turing's Halting problem is a theorem. Here is another authoritative reference to the fact I originally posted: "Did Turing prove the undecidability of the halting problem?" from the Oxford University Press -- https://academic.oup.com/logcom/article/36/1/exaf075/8417148 https://academic.oup.com/logcom/article/36/1/exaf075/8417148 . The question in the title is rhetorical, as you will discover if you read and understand the article I just linked. > It is now your opportunity to make a mathematical claim, of which proof by assertion this paper should apply because it proves something in general is not. How many more mathematical literature references will you require before you realize I have already met any burden of proof? I could post the entire technical proof here, but (a) the editors of this forum would kick me out, and (b) you would still refuse to accept the evidence. How do I know this? Because you keep refusing to learn what you need to know to engage in this conversation. There are an infinity of primes -- your turn.

by lutusp 14d ago

zamadatix 13d ago

If you wish to say you have a counterclaim to the idea mistakes can be blocked regardless if every program can be proven to halt which is based in mathematical reasoning you must be able to state or produce the claim in the actual mathematical reasoning itself (or at least a link to the specific math directly relevant to the claim), not an English text summary of an entire paper/problem on Wikipedia. Anything less is not mathematical reasoning. I'm unable to say more at this point as I can only assume you will continue to use that as a chance to quote and discuss everything but actual mathematics.

lutusp 12d ago
> If you wish to say you have a counterclaim to the idea mistakes can be blocked regardless if every program can be proven to halt which is based in mathematical reasoning you must be able to state or produce the claim in the actual mathematical reasoning itself ... This is not a philosophy discussion, and Alan Turing already plowed this ground. The original claim "Bend - a language that blocks AI mistakes via proof [...]" is unsupportable. > ... if every program can be proven to halt ... But that's not so. You have introduced a qualifier that is known to be false. > ... a chance to quote and discuss everything but actual mathematics. Yes, I agree -- you should stop doing that. I keep referring to the original technical reason the original claim is unsupportable, others keep raising objections without trying to think through their positions. It's not as though the Halting Problem is on the Millennium Prize Problem list, open to contradiction/reconsideration by some future challenge. It's a theorem, not a conjecture.
- zamadatix 12d ago
  I've given notes of where in Turing's paper any type use triviality could be found, with direct page citations of the relevant original math, along with the mathematical reasons it doesn't have anything to do with the plain English statements you are making. This effort was a kindness done in good faith that I might find said mathematical definition of non-triviality for the halting problem somewhere in the paper, not something needed to show your claim devoid of a shown basis in mathematical reasoning so far. That much is apparent by the lack of a single mathematically defined claim specified by any of your messages. That said, if you'd like me to formally show what e.g. the triviality in the rules of implication Turing was talking about are in a purely mathematical form I'd be glad to state with no English commentary out of good faith as well. This would seem a waste of time unless that's the part of the paper you think the definition of non-triviality can be sourced, but at least I'd at last have a clear mathematical claim from you to discuss. It is now your opportunity to make a mathematical claim, of which proof by assertion this paper should apply because it proves something in general is not.
  - lutusp 12d ago
    > That much is apparent by the lack of a single mathematically defined claim specified by any of your messages. I posted the Turing Halting Problem Wikipedia page. It describes a theorem, not a conjecture that I need to prove, which shows the original poster's claim is contradicted by established facts. Let me put it this way. If I say, "There are an infinity of primes," will you reply, saying, "I disagree"? That position would be equally appropriate -- that is to say, not appropriate at all. Am I obliged to prove the infinity of primes by generating an infinity of candidate integers and prove that some of them are prime? No, and by the same token, I'm not obliged to reply to your naive demands and teach you why the Halting Problem falsifies the claim made by the original poster. That is not my responsibility, it is yours. In mathematics, some things are conjectures -- the Millennium Challenge problems, for example. Others are theorems, meaning established truths, beyond dispute. Turing's Halting problem is a theorem. Here is another authoritative reference to the fact I originally posted: "Did Turing prove the undecidability of the halting problem?" from the Oxford University Press -- https://academic.oup.com/logcom/article/36/1/exaf075/8417148 https://academic.oup.com/logcom/article/36/1/exaf075/8417148 . The question in the title is rhetorical, as you will discover if you read and understand the article I just linked. > It is now your opportunity to make a mathematical claim, of which proof by assertion this paper should apply because it proves something in general is not. How many more mathematical literature references will you require before you realize I have already met any burden of proof? I could post the entire technical proof here, but (a) the editors of this forum would kick me out, and (b) you would still refuse to accept the evidence. How do I know this? Because you keep refusing to learn what you need to know to engage in this conversation. There are an infinity of primes -- your turn.