XPost: comp.theory, sci.logic, sci.math
From: polcott333@gmail.com
On 11/21/2025 1:38 AM, dart200 wrote:
> On 11/20/25 3:15 PM, Ben Bacarisse wrote:
>> dart200 writes:
>>
>>> On 11/19/25 3:36 PM, Ben Bacarisse wrote:
>>>> dart200 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,
>>
[continued in next message]
--- SoupGate-Win32 v1.05
* Origin: you cannot sedate... all the things you hate (1:229/2)
|
