From Newsgroup: comp.ai.philosophy

On 11/21/2025 1:38 AM, dart200 wrote:

On 11/20/25 3:15 PM, Ben Bacarisse wrote:

dart200 <user7160@newsgrouper.org.invalid> writes:

On 11/19/25 3:36 PM, Ben Bacarisse wrote:

dart200 <user7160@newsgrouper.org.invalid> writes:

On 11/17/25 9:29 AM, Alan Mackenzie wrote:

The Halting Theorem is wholly a theorem of mathematics,
and only secondarily about computer science.

the original proof as written by turing uses notions justified in
turing
machines to then support godel's result, not the other way around

No.  Turing was working on the Entscheidungsproblem.  A different
problem altogether.

it is fundamentally based in computer science using turing machines as >>>>> "axioms", which are in turn justified by our ability to mechanically >>>>> undertake the operations, not set theory

No.  Turing machines are not "axioms" in any sense of the word; they >>>> are
entirely mathematical entities built from the axioms of set theory.
Turing was writing for an audience that would know that a "tape" was
just a convenient term for a function from Z to Gamma (the tape
alphabet), that the "head" is just an integer and "writing to the tape" >>>> just results in a new function from Z to Gamma.  The "machine
configuration" is just a tuple as is the TM itself.  I.e. a TM is
just a
set (though you need to know how tuples and function are just sets in
order to believe this).

literally his words:

we may compare a man in the process of computing a real number to a
machine which is only capable of a finite number of conditions q1, q2,
... qi; which will be called "m-configurations". The machine is supplied >>> with a "tape " (the analogue of paper) running through it, and
divided into
sections (called "squares") each capable of bearing a "symbol". At any
moment there is just one square, say the r-th, bearing the symbol
T(r)vwhich
is "in the machine". We may call this square the "scanned square ". The
symbol on the scanned square may be called the " scanned symbol". The
"scanned symbol" is the only one of which the machine is, so to speak,
"directly aware" [Tur36]

Yes, I've read the paper several times.  Turing was a mathematician,

several times end to end??? i'm smelling some bs my dude, sorry bout
that, but i'm going to have quote turing a bunch to show how ur quite mistaken about the paper.

i haven't read the paper thoroughly end to end. i've only read certain sections thoroughly and skimmed it end to end. most of my focus has into specifically §8, and have read that *very* thoroughly. i then skimmed
the rest of the paper concentration specifically on how the results of
of §8 are used to justify conclusions in the following sections. i've mostly ignored before §8 since he was mostly just constructing turing machines, but have a rough idea what's going on.

working under Alonzo Church on formal systems.  He is describing a
mathematical object now called a Turing Machine.

idk maybe you can describe turing machines in set theory, but it's
weird to
claim turing just assumed they would make the connection instead of
being
specific about it.

He was a mathematician working at a time when a computer was a person
who did arithmetic and sometimes symbol manipulation -- i.e. maths.  He
knew (and he knew that all his reader knew) that he was describing
mathematical results about mathematical objects.

What do you think he was talking about if not mathematical theorems
about mathematical objects?

The Entscheidungsproblem is an entirely mathematical question about
formal systems.  Cranks focus on Turing's work because the metaphors of >>>> tapes and so on are easy to get one's head around (no pun intended!).
This is also why Turing gets so much credit, but Church, technically,
got there first with his proof using the lambda calculus.  No crank
ever
disputes this proof because they can't waffle about it (or, in most
cases, even understand it).

no one focuses the semantic paradox actually described by turing either,

There is no paradox.

i'm gunna say this a million times, eh???

*the halting paradox is a paradox like how the liar's paradox is a paradox*

When an input D to a decider H is encoded to do the
opposite of whatever H returns this H/D pair is
isomorphic to the Liar Paradox.

?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.

The above definitively proves that the Liar
Paradox is semantically unsound because its
resolution has an infinite resolution loop.

Because the halting problem is isomorphic to
the Liar Paradox the Halting Problem is refuted
by proxy.

So more than a mere paradox both the Halting
Problem and the Liar Paradox are rejected as
errors of reasoning.

When we start with a complete set of atomic
facts of the world expressed in language and
the only inference step allowed is semantic
logical entailment then no paradox can be
derived and True(Language L, Expression E)
can always be computed.

The language to encode all of this is an
extended form of Montague Grammar uniting
syntax and semantics as one. This discards
the whole notice of model theory.

It makes a syntactic proof the same thing as
semantic logical entailment. The Atomic facts
of the world are stored in a knowledge ontology
inheritance hierarchy.

they work the same way: if you try to "decide" the math object into a
set classifying it's semantics, then the object will take that classification and defy the classification, making it impossible to
decide upon.

they all focus on the halting problem which wasn't what turing
specifically
worked on.

Since Turing was interested in the mathematics (the
Entscheidungsproblem) and not the practicality of what we now call
"computing" he rattles off what we now call the halting theorem and a
couple of other (to him) trivial results without giving them either a
name or much weight, except in that the advance his main goal.

yes, he was using them as building blocks in his proof

turing uses a "satisfactory" problem to support godel's incompleteness
not the halting problem,

No.  I'm not sure what you mean by "a 'satisfactory' problem" because

/A number which is a description number of a circle-free machine will be called a satisfactory number. In §8 it is shown that there can be no general process for determining whether a given number is satisfactory
or not/ [Tur36 p241]

after turing spends §1-§7 defining turing machine, §8 is where he proves the "halting theorem" as you say. in that proof he's really proving
there's no way to prove a number "satisfactory" or more technically "circle-free"

big miss there buddy, the "satisfactory" paradox (inability to build a general decider for "satisfactory" numbers) he describes §8 (on p247) in
is literally keystone contradiction he bases the rest of his undecidable proof

Turing uses the term "satisfactory" only in relation to numbers.
However, he is not supporting Godel's incompleteness theorem, he is

he is 100% supporting godel's result

/If the negation of what Godel has shown had been proved, i.e. if, for
each U, either U or —U is provable, then we should have an immediate solution of the Entscheidungsproblem. For we can invent a machine H
which will prove consecutively all provable formulae. Sooner or later H
will reach either U or —U. If it reaches U, then we know that U is provable. If it reaches —U, then, since K is consistent (Hilbert and Ackermann, p. 65), we know that U is not provable/ [Tur36 p259]

what he's doing is saying that if godel had proven otherwise (to incompleteness) then there'd be some machine which would prove all
provable formulae

because of this there must be some method to ensure such isn't construct-able, and ultimately §11 is tying such a machine to the previously disproveb notion (of §8) that a decider D that could
determine whether a given number is satisfactory:

/We are now in a position to show that the Entscheidungsproblem cannot
be solved. Let us suppose the contrary. Then there is a general
(mechanical) process for determining whether Un(𝓜 ) is provable. By Lemmas 1 and 2, this implies that there is a process for determining
whether 𝓜 ever prints 0, and this is impossible, by §8. Hence the Entscheidungsproblem cannot be solved/ [Tur26 p262]

yes he is ultimately also disproving the entscheidungsproblem, but he's motivated in doing so specifically because it aligns with godel's
previous result, and his paper ultimately strengthens godel's result,
even if the specific method *is* quite different

using what we now call the halting theorem to derive results about
computation numbers.  In section 11 he says "It should perhaps be
remarked what I shall prove is quite different from the well-known
results of Gödel".

the halting problem variant was
first described by kleene and/or davis

The term was indeed coined later, but the result is right there in the

not just coined later, but also described later. turing specifically
tied his support of incompleteness to the "satisfactory number" paradox,
not halting paradox

paper along with two proofs.  He was inventing the whole subject on the
fly so it not surprising that we now use other terms, but a theorem by
another name shall smell as sweet.

--
Copyright 2025 Olcott

My 28 year goal has been to make
"true on the basis of meaning" computable.
--- Synchronet 3.21a-Linux NewsLink 1.2