1. Forum
  2. Newsgroups
  3. comp.theory

  • Re: When halt provers are allowed to reject bad inputs the remainingdomain is decidable

    From Mikko@[email protected] to sci.logic,comp.theory on Sun Feb 8 11:06:04 2026
    From Newsgroup: comp.theory

    On 07/02/2026 15:08, olcott wrote:
    On 2/7/2026 4:15 AM, Mikko wrote:
    On 06/02/2026 17:32, olcott wrote:
    On 2/6/2026 3:15 AM, Mikko wrote:
    On 05/02/2026 13:28, olcott wrote:

    On 2/5/2026 4:45 AM, Mikko wrote:
    On 04/02/2026 18:47, olcott wrote:

    A halt prover attempts to prove halting

    To prove that a computation halts is simple. Just show the execution >>>>>> trace from the start to the halting. The hard problem is to prove
    that an execution does not halt.

    and when it detects that the proof of its input does not form

    *a well-founded justification tree within Proof*
    *theoretic semantics*

    Then it is correct to reject this input as bad data.

    No, that does not follow. That only means that it is correct to
    reject
    the proof. The conclusion of the proof may still be correct.
    The way that proofs work in proof theoretic
    semantics is that they reject inputs not having
    well-founded justification trees as bad data.

    An example of a valid input is "42". That input has no justification,
    well-founded or otherwise. But there is no proof that would reject
    "42" as bad data.

    It is an element of the set of natural numbers.

    True, but non necessarily relevant to tthe proof. But the current
    question is whether the proof rejects the input "42" as bad data.

    Is the integer 42 a machine description that halts?
    Reject.

    The question is already answered above: "42" is an input not having
    a well-founded justification tree, or at least none that I know.
    --
    Mikko
    --- Synchronet 3.21b-Linux NewsLink 1.2