From Newsgroup: sci.math

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.21b-Linux NewsLink 1.2