The halting problem proof fails under operational semantics
From olcott@[email protected] 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
Wed Mar 11 00:59:44 2026
from
Moore, Ok
via
Telnet
Noozle
Tue Mar 10 16:57:26 2026
from
Noozle City
via
Telnet
Neko
Tue Mar 10 15:16:47 2026
from
San Francisco, Ca
via
Telnet
Microbot
Tue Mar 10 02:26:45 2026
from
Moore, Ok
via
Telnet