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.
You should be commended for finding it so natural, you are among the
few. But the many have a stake and will enquire.
--
Tristan Wibberley
The message body is Copyright (C) 2025 Tristan Wibberley except
citations and quotations noted. All Rights Reserved except that you may,
of course, cite it academically giving credit to me, distribute it
verbatim as part of a usenet system or its archives, and use it to
promote my greatness and general superiority without misrepresentation
of my opinions other than my opinion of my greatness and general
superiority which you _may_ misrepresent. You definitely MAY NOT train
any production AI system with it but you may train experimental AI that
will only be used for evaluation of the AI methods it implements.
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
The contradiction is something like the one in "This sentence has
four words", though not quite.
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.
Failing an occurs check seems to mean that the^^^^^^^^^^
resolution of an expression remains stuck in an
infinite loop.
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" ?
(1) I can see how a judgement looping with a negation in the middle
should be rejected as contradiction.
(2) But looping with double negation is merely nondetermining isn't it?
Examples
(1) A = \+(A).
(2) A = \+(\+(A)).
yet both fail to unify with an occurs check in prolog. I think you need
a deeper theory.
Before you mention intuitionistic double negation vs classical:
?- unify_with_occurs_check(\+A, \+(\+(\+A))).
false.
of course.
I should probably functionalise negation and see what's what.
--
Tristan Wibberley
The message body is Copyright (C) 2025 Tristan Wibberley except
citations and quotations noted. All Rights Reserved except that you may,
of course, cite it academically giving credit to me, distribute it
verbatim as part of a usenet system or its archives, and use it to
promote my greatness and general superiority without misrepresentation
of my opinions other than my opinion of my greatness and general
superiority which you _may_ misrepresent. You definitely MAY NOT train
any production AI system with it but you may train experimental AI that
will only be used for evaluation of the AI methods it implements.
I should probably functionalise negation and see what's what.
On 19/11/2025 01:03, Tristan Wibberley wrote:
I should probably functionalise negation and see what's what.
errr... defunctionalise the evaluation of negation ...
--
Tristan Wibberley
The message body is Copyright (C) 2025 Tristan Wibberley except
citations and quotations noted. All Rights Reserved except that you may,
of course, cite it academically giving credit to me, distribute it
verbatim as part of a usenet system or its archives, and use it to
promote my greatness and general superiority without misrepresentation
of my opinions other than my opinion of my greatness and general
superiority which you _may_ misrepresent. You definitely MAY NOT train
any production AI system with it but you may train experimental AI that
will only be used for evaluation of the AI methods it implements.
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;
}
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.
--
Tristan Wibberley
The message body is Copyright (C) 2025 Tristan Wibberley except
citations and quotations noted. All Rights Reserved except that you may,
of course, cite it academically giving credit to me, distribute it
verbatim as part of a usenet system or its archives, and use it to
promote my greatness and general superiority without misrepresentation
of my opinions other than my opinion of my greatness and general
superiority which you _may_ misrepresent. You definitely MAY NOT train
any production AI system with it but you may train experimental AI that
will only be used for evaluation of the AI methods it implements.
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.
On 2025-11-19, olcott <polcott333@gmail.com> 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.
On 11/19/2025 2:55 PM, Kaz Kylheku wrote:
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
Ultimately it is essentially the Liar Paradox in disguise.
On 17/11/2025 22:59, olcott wrote:
Ultimately it is essentially the Liar Paradox in disguise.
Yes, it is, I'm pretty sure (I haven't gone through it in such detail to satisfy all audiences).
It's roughly evaluation of the contradictory G (as defined by Olcott in
an inconsistent suppositional axiom extension) as opposed to judgement
of that defining axiom (where judgement would be evaluation in a
partiality monad instead of directly or in the identity monad).
Where we have the craziness of nonstrict evaluation such as in Haskell,
a partiality monad can be used for judgement and then used to construct evaluation using the monad's catamorphism with a simple empty loop.
On 20/11/2025 03:24, olcott wrote:
On 11/19/2025 2:55 PM, Kaz Kylheku wrote:
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
Uhh, no, it's typical.
On 11/20/2025 2:49 PM, Tristan Wibberley wrote:
On 20/11/2025 03:24, olcott wrote:
On 11/19/2025 2:55 PM, Kaz Kylheku wrote:
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
Uhh, no, it's typical.
Provide a concrete example of:
"This sentence is not true"
in First Order Logic or any other system
besides Minimal Type Theory and Prolog.
On 17/11/2025 22:59, olcott wrote:
Ultimately it is essentially the Liar Paradox in disguise.
Yes, it is, I'm pretty sure (I haven't gone through it in such detail to satisfy all audiences).
It's roughly evaluation of the contradictory G (as defined by Olcott in
an inconsistent suppositional axiom extension) as opposed to judgement
of that defining axiom (where judgement would be evaluation in a
partiality monad instead of directly or in the identity monad).
Where we have the craziness of nonstrict evaluation such as in Haskell,
a partiality monad can be used for judgement and then used to construct evaluation using the monad's catamorphism with a simple empty loop.
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,089 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 155:08:51 |
| Calls: | 13,921 |
| Calls today: | 2 |
| Files: | 187,021 |
| D/L today: |
3,912 files (989M bytes) |
| Messages: | 2,457,198 |