Forums before death by AOL, social media and spammers... "We can't have nice things"
|    sci.logic    |    Logic -- math, philosophy & computationa    |    262,912 messages    |
[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]
|    Message 262,830 of 262,912    |
|    olcott to Mikko    |
|    Re: When halt provers are allowed to rej    |
|    06 Feb 26 09:32:37    |
      From: polcott333@gmail.com              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.              --       Copyright 2026 Olcott |
[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]
(c) 1994, bbs@darkrealms.ca