XPost: comp.theory, comp.ai.philosophy, sci.math
From: polcott333@gmail.com
On 11/19/2025 2:55 PM, Kaz Kylheku wrote:
> On 2025-11-19, olcott wrote:
>> On 11/19/2025 12:51 PM, Tristan Wibberley wrote:
>>> On 19/11/2025 01:36, olcott wrote:
>>>> On 11/18/2025 7:03 PM, Tristan Wibberley wrote:
>>>>> On 17/11/2025 22:59, olcott wrote:
>>>>>> On 11/17/2025 4:45 PM, Tristan Wibberley wrote:
>>>>>>> On 17/11/2025 22:15, Alan Mackenzie wrote:
>>>>>>>
>>>>>>>> There is no proper academic conversation to be had over 2 + 2 = 4.
>>>>>>>> It is
>>>>>>>> firm, unassailable knowledge, unchallengeable. The Halting Theorem
>>>>>>>> is of
>>>>>>>> the same status, proven using the same methodology from the same
>>>>>>>> fundamentals.
>>>>>>>
>>>>>>>
>>>>>>> It's a completely different league from 2 + 2 = 4.
>>>>>>> It's closer to x = 1/2 + x/2 but it's still conceptually /much/ harder
>>>>>>> than that.
>>>>>>> It's more like the problem of whether a fixed point exists or not, but
>>>>>>> it's for the fixed point of a limit of a particular, conceptually
>>>>>>> weird,
>>>>>>> sequence of functions.
>>>>>>>
>>>>>>> It really is quite peculiar.
>>>>>>>
>>>>>>
>>>>>> Ultimately it is essentially the Liar Paradox in disguise.
>>>>>>
>>>>>> The Liar Paradox formalized in the Prolog Programming language
>>>>>>
>>>>>> This sentence is not true.
>>>>>> It is not true about what?
>>>>>> It is not true about being not true.
>>>>>> It is not true about being not true about what?
>>>>>> It is not true about being not true about being not true.
>>>>>> Oh I see you are stuck in a loop!
>>>>>>
>>>>>> This is formalized in the Prolog programming language below.
>>>>>>
>>>>>> ?- LP = not(true(LP)).
>>>>>> LP = not(true(LP)).
>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>> false.
>>>>>
>>>>> true/0
>>>>> use \+/1 rather than not/1
>>>>>
>>>>>
>>>>>> Failing an occurs check seems to mean that the
>>>>>> resolution of an expression remains stuck in an
>>>>> ^^^^^^^^^^
>>>>>> infinite loop.
>>>>>
>>>>> You mean "judgement" ?
>>>>
>>>> I mean like this thingy:
>>>>
>>>> void Infinite_Loop()
>>>> {
>>>> HERE: goto HERE;
>>>> return;
>>>> }
>>>
>>> Ah the terminological problem of what to call something like a
>>> "normalisation" process when it might be that no normal form exists.
>>>
>>> In the pure functional world your C characterisation is typically called
>>> "a computation" but I'm not sure where the boundary lies or whether you
>>> really mean "judgement" or "evaluation". In the C world "evaluation" of
>>> "Infinite_Loop()" is a real thing that exists, even if the expression
>>> has no value or any normal form in any conventionally reasonable
>>> formalisation and the mapping of your original terms to Infinite_Loop is
>>> just one choice for how to judge.
>>>
>>
>> When you fully understand every nuance of my terms
>> then you understand that when the directed graph
>> of the evaluation sequence of a formal expression
>> contains a cycle that this proves that this expression
>> is semantically unsound because the evaluation of
>> this expression does have an actual infinite loop
>> just like this one.
>
> Your three pages full of nothng, titled Minimal Type Theory,
> don't contain anything original.
>
It directly encodes self-reference that no other
formal system has ever done and has a provability
operator directly in the language.
G := (F ⊬ G) // G "is defined as" unprovable in F
LP := ~True(LP) // LP "is defined as" not true
--
Copyright 2025 Olcott
My 28 year goal has been to make
"true on the basis of meaning" computable.
--- SoupGate-Win32 v1.05
* Origin: you cannot sedate... all the things you hate (1:229/2)
|
