On 7/5/2026 9:52 AM, Tristan Wibberley wrote:
On 04/07/2026 16:31, Tristan Wibberley wrote:
On 06/05/2026 20:37, Julio Di Egidio wrote:
On 02/05/2026 20:47, Scott Hoge wrote:
In Cantor's theorem, we do not actually construct a diagonal.
Rather, we presuppose that we can enumerate a set, and then,
/purely on the grounds of possibility/, conceive a diagonalized
non-element.
Nope, as explained and re-explained ad nauseam around here:
just the resident trolls won't get it.
Cantor's diagonal argument, the one with the binary sequences,
is indeed constructive: a definition of anti-diagonal of *any*
(infinite) list is provided, and the proof that the anti-diagonal
cannot be in the list is quite constructive.
"quite" but not "completely".
A constructive operation is defined, but a diagonal number is
constructed just when that constructive operation is applied to a
constructible list.
I should note for the less knowledgable readers of course it's less
often than that, it is only that often for systems such as the one Julio
and Phoenix are using which allows dequantification of universally
quantified statements into the system proper which then have derivable
statements containing actual constructions of the constructible objects
they apply to by virtue of their original quantification. Of course,
dequantification of fantastically quantified statements doesn't make a
statement about nonconstructible objects because there aren't any
outside of the fantastical quantification.
By which I don't mean to argue the countability of the set of reals as
defined in what we call Cantor's Proof of the Uncountability of the
Reals to include objects quantified over by fantatstical quantification
but not by universal quantification, but it does make some meaning
clearer.
While some of the sets might have objects in the system proper, some of
the members of some of the sets clearly do not.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
Olcott's Minimal Type Theory
G rao -4Prov_PA(riLGriY)
Directed Graph of evaluation sequence
00 rao 01 02
01 G
02 -4 03
03 Prov_PA 04
04 G||del_Number_of 01 // cycle indicates no well-founded justification
tree exists.
The absence of
(a) finite sequence of inference steps to an atomic base,
(b) canonical proof
(c) well-founded justification tree
makes the above to PTS invalid.
On 7/5/2026 2:56 PM, Ross Finlayson wrote:
On 07/05/2026 09:33 AM, olcott wrote:
On 7/5/2026 9:52 AM, Tristan Wibberley wrote:
On 04/07/2026 16:31, Tristan Wibberley wrote:
On 06/05/2026 20:37, Julio Di Egidio wrote:
On 02/05/2026 20:47, Scott Hoge wrote:
In Cantor's theorem, we do not actually construct a diagonal.
Rather, we presuppose that we can enumerate a set, and then,
/purely on the grounds of possibility/, conceive a diagonalized
non-element.
Nope, as explained and re-explained ad nauseam around here:
just the resident trolls won't get it.
Cantor's diagonal argument, the one with the binary sequences,
is indeed constructive: a definition of anti-diagonal of *any*
(infinite) list is provided, and the proof that the anti-diagonal
cannot be in the list is quite constructive.
"quite" but not "completely".
A constructive operation is defined, but a diagonal number is
constructed just when that constructive operation is applied to a
constructible list.
I should note for the less knowledgable readers of course it's less
often than that, it is only that often for systems such as the one
Julio
and Phoenix are using which allows dequantification of universally
quantified statements into the system proper which then have derivable >>>> statements containing actual constructions of the constructible objects >>>> they apply to by virtue of their original quantification. Of course,
dequantification of fantastically quantified statements doesn't make a >>>> statement about nonconstructible objects because there aren't any
outside of the fantastical quantification.
By which I don't mean to argue the countability of the set of reals as >>>> defined in what we call Cantor's Proof of the Uncountability of the
Reals to include objects quantified over by fantatstical quantification >>>> but not by universal quantification, but it does make some meaning
clearer.
While some of the sets might have objects in the system proper, some of >>>> the members of some of the sets clearly do not.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
Olcott's Minimal Type Theory
G rao -4Prov_PA(riLGriY)
Directed Graph of evaluation sequence
00 rao 01 02
01 G
02 -4 03
03 Prov_PA 04
04 G||del_Number_of 01 // cycle indicates no well-founded justification >>> tree exists.
The absence of
(a) finite sequence of inference steps to an atomic base,
(b) canonical proof
(c) well-founded justification tree
makes the above to PTS invalid.
Yeah, come up with something new, or stuff a sock in it.
The above proves that the notion of undecidable
is incorrect if you understood rather than ignored
what it says.
It also is the final resolution to the Liar Paradox
and you would know this if you understood it.
On 7/5/2026 4:30 PM, Ross Finlayson wrote:
On 07/05/2026 01:25 PM, olcott wrote:
On 7/5/2026 2:56 PM, Ross Finlayson wrote:
On 07/05/2026 09:33 AM, olcott wrote:
On 7/5/2026 9:52 AM, Tristan Wibberley wrote:
On 04/07/2026 16:31, Tristan Wibberley wrote:
On 06/05/2026 20:37, Julio Di Egidio wrote:
On 02/05/2026 20:47, Scott Hoge wrote:
In Cantor's theorem, we do not actually construct a diagonal. >>>>>>>>> Rather, we presuppose that we can enumerate a set, and then, >>>>>>>>> /purely on the grounds of possibility/, conceive a diagonalized >>>>>>>>> non-element.
Nope, as explained and re-explained ad nauseam around here:
just the resident trolls won't get it.
Cantor's diagonal argument, the one with the binary sequences, >>>>>>>> is indeed constructive: a definition of anti-diagonal of *any* >>>>>>>> (infinite) list is provided, and the proof that the anti-diagonal >>>>>>>> cannot be in the list is quite constructive.
"quite" but not "completely".
A constructive operation is defined, but a diagonal number is
constructed just when that constructive operation is applied to a >>>>>>> constructible list.
I should note for the less knowledgable readers of course it's less >>>>>> often than that, it is only that often for systems such as the one >>>>>> Julio
and Phoenix are using which allows dequantification of universally >>>>>> quantified statements into the system proper which then have
derivable
statements containing actual constructions of the constructible
objects
they apply to by virtue of their original quantification. Of course, >>>>>> dequantification of fantastically quantified statements doesn't
make a
statement about nonconstructible objects because there aren't any
outside of the fantastical quantification.
By which I don't mean to argue the countability of the set of
reals as
defined in what we call Cantor's Proof of the Uncountability of the >>>>>> Reals to include objects quantified over by fantatstical
quantification
but not by universal quantification, but it does make some meaning >>>>>> clearer.
While some of the sets might have objects in the system proper,
some of
the members of some of the sets clearly do not.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
Olcott's Minimal Type Theory
G rao -4Prov_PA(riLGriY)
Directed Graph of evaluation sequence
00 rao 01 02
01 G
02 -4 03
03 Prov_PA 04
04 G||del_Number_of 01 // cycle indicates no well-founded
justification
tree exists.
The absence of
(a) finite sequence of inference steps to an atomic base,
(b) canonical proof
(c) well-founded justification tree
makes the above to PTS invalid.
Yeah, come up with something new, or stuff a sock in it.
The above proves that the notion of undecidable
is incorrect if you understood rather than ignored
what it says.
It also is the final resolution to the Liar Paradox
and you would know this if you understood it.
Like I said,
"understanding" is for suckers,
"comprehension" is for knowledge.
Gemini agrees with me and I only gave it the Prolog. https://share.gemini.google/1dJnMwOZ2k5F
Your axiomatization otherwise is false.
It's like they say,
"It just don't mean a thing."
WM <- retro-finitist crankety-troll
JG <- retro-finitist crankety-troll
PO <- retro-finitist crankety-troll
"Polluter(s) of sci.math"
On 7/5/2026 5:15 PM, Ross Finlayson wrote:
On 07/05/2026 02:45 PM, olcott wrote:
On 7/5/2026 4:30 PM, Ross Finlayson wrote:
On 07/05/2026 01:25 PM, olcott wrote:
On 7/5/2026 2:56 PM, Ross Finlayson wrote:
On 07/05/2026 09:33 AM, olcott wrote:
On 7/5/2026 9:52 AM, Tristan Wibberley wrote:
On 04/07/2026 16:31, Tristan Wibberley wrote:
On 06/05/2026 20:37, Julio Di Egidio wrote:
On 02/05/2026 20:47, Scott Hoge wrote:
In Cantor's theorem, we do not actually construct a diagonal. >>>>>>>>>>> Rather, we presuppose that we can enumerate a set, and then, >>>>>>>>>>> /purely on the grounds of possibility/, conceive a diagonalized >>>>>>>>>>> non-element.
Nope, as explained and re-explained ad nauseam around here: >>>>>>>>>> just the resident trolls won't get it.
Cantor's diagonal argument, the one with the binary sequences, >>>>>>>>>> is indeed constructive: a definition of anti-diagonal of *any* >>>>>>>>>> (infinite) list is provided, and the proof that the anti-diagonal >>>>>>>>>> cannot be in the list is quite constructive.
"quite" but not "completely".
A constructive operation is defined, but a diagonal number is >>>>>>>>> constructed just when that constructive operation is applied to a >>>>>>>>> constructible list.
I should note for the less knowledgable readers of course it's less >>>>>>>> often than that, it is only that often for systems such as the one >>>>>>>> Julio
and Phoenix are using which allows dequantification of universally >>>>>>>> quantified statements into the system proper which then have
derivable
statements containing actual constructions of the constructible >>>>>>>> objects
they apply to by virtue of their original quantification. Of
course,
dequantification of fantastically quantified statements doesn't >>>>>>>> make a
statement about nonconstructible objects because there aren't any >>>>>>>> outside of the fantastical quantification.
By which I don't mean to argue the countability of the set of
reals as
defined in what we call Cantor's Proof of the Uncountability of the >>>>>>>> Reals to include objects quantified over by fantatstical
quantification
but not by universal quantification, but it does make some meaning >>>>>>>> clearer.
While some of the sets might have objects in the system proper, >>>>>>>> some of
the members of some of the sets clearly do not.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
Gemini agrees with not-you.
OK then the point that I was trying to make is
exactly what Gemini said right here:
https://share.gemini.google/1dJnMwOZ2k5F
| Sysop: | Amessyroom |
|---|---|
| Location: | Fayetteville, NC |
| Users: | 74 |
| Nodes: | 6 (0 / 6) |
| Uptime: | 50:19:52 |
| Calls: | 1,100 |
| Files: | 1,339 |
| Messages: | 275,859 |