The halting problem proof fails under operational semantics
From olcott@polcott333@gmail.com to comp.theory,sci.logic,sci.math,comp.ai.philosophy,comp.lang.prolog on Wed Jan 14 18:14:25 2026
From Newsgroup: comp.ai.philosophy
The halting problem proof fails not because finite computation
is insufficient, but because it asks finite computation
to decide a judgment that is not finitely grounded under
operational semantics.
By “operational semantics” I mean the standard proof-theoretic
account of program meaning in which execution judgments are
defined by inference rules and termination corresponds to the
existence of a finite derivation.
By proof-theoretic semantics I mean the standard approach in
which the meaning of a statement is given by its rules of
proof rather than by truth conditions in a model.
This is the same sense in which operational semantics gives
meaning to programs via execution rules rather than denotations.
By denotational semantics I mean the standard approach in which
every well-formed program or statement is assigned a mathematical
object such as a function or truth value---independently of how
it is computed or proved.
This contrasts with operational or proof-theoretic semantics,
where meaning is given by execution or proof rules rather than
by an abstract denotation.
I use ‘denotational semantics’ simply to refer to any semantics
that assigns abstract mathematical meanings to programs independently
of their operational behavior.
--
Copyright 2026 Olcott<br><br>
My 28 year goal has been to make <br>
"true on the basis of meaning expressed in language"<br>
reliably computable.<br><br>
This required establishing a new foundation<br>
--- Synchronet 3.21a-Linux NewsLink 1.2
Who's Online
Recent Visitors
Microbot
Tue Feb 3 08:27:31 2026
from
Moore, Ok
via
Telnet
Noozle
Tue Feb 3 07:13:28 2026
from
Noozle City
via
Telnet
Microbot
Mon Feb 2 10:07:38 2026
from
Moore, Ok
via
Telnet
Noozle
Mon Feb 2 08:57:17 2026
from
Noozle City
via
Telnet