On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:
Non-programmers and non-Prolog programmers only
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY.
I don't know about non-programmers but everyone who knows enough about
programming to be able to read the definition of the predicate
unify_with_occurs_check/2 can understand that its failure means that
the programmer does not like a cyclic structure at that point.
That is so stupidly wrong that it must be dishonest.
Prolog is what the standard says it is. You don't show any contradiction
with the Prolog standard but dishonesstly say "dishonest" anyway.
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:
Non-programmers and non-Prolog programmers only
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY.
I don't know about non-programmers but everyone who knows enough about >>>> programming to be able to read the definition of the predicate
unify_with_occurs_check/2 can understand that its failure means that
the programmer does not like a cyclic structure at that point.
That is so stupidly wrong that it must be dishonest.
Prolog is what the standard says it is. You don't show any contradiction
with the Prolog standard but dishonesstly say "dishonest" anyway.
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:
Non-programmers and non-Prolog programmers onlyI don't know about non-programmers but everyone who knows enough about >>>>> programming to be able to read the definition of the predicate
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY. >>>>>
unify_with_occurs_check/2 can understand that its failure means that >>>>> the programmer does not like a cyclic structure at that point.
That is so stupidly wrong that it must be dishonest.
Prolog is what the standard says it is. You don't show any contradiction >>> with the Prolog standard but dishonesstly say "dishonest" anyway.
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog semantics.
Only Prolog semantics is defined in the standard.
On 1/11/2026 4:26 AM, Mikko wrote:
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:
Non-programmers and non-Prolog programmers onlyI don't know about non-programmers but everyone who knows enough
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY. >>>>>>
about
programming to be able to read the definition of the predicate
unify_with_occurs_check/2 can understand that its failure means that >>>>>> the programmer does not like a cyclic structure at that point.
That is so stupidly wrong that it must be dishonest.
Prolog is what the standard says it is. You don't show any
contradiction
with the Prolog standard but dishonesstly say "dishonest" anyway.
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog semantics.
Only Prolog semantics is defined in the standard.
rCLProlog is an operational implementation of proof-theoretic semantics: truth is derivability, and only well-founded proofs count.rCY
rCLIn proof-theoretic semantics, as reflected in the well-founded
semantics of logic programming, the Liar is rejected as a non-well-
founded goal.rCY
In proof-theoretic semantics, the Liar Paradox is not a genuine contradiction but a non-well-founded construct, and thus not truth-apt.
Proof Theoretic Semantics is not the same as Truth Conditional Semantics.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
This is similar to semantically ungrounded (Kripke 1975) at the Tarski object language level thus cannot be resolved to a truth value. Outline
of a Theory of Truth --- Saul Kripke
On 1/11/26 9:25 AM, olcott wrote:
On 1/11/2026 4:26 AM, Mikko wrote:
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:
Non-programmers and non-Prolog programmers onlyI don't know about non-programmers but everyone who knows enough >>>>>>> about
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY. >>>>>>>
programming to be able to read the definition of the predicate
unify_with_occurs_check/2 can understand that its failure means that >>>>>>> the programmer does not like a cyclic structure at that point.
That is so stupidly wrong that it must be dishonest.
Prolog is what the standard says it is. You don't show any
contradiction
with the Prolog standard but dishonesstly say "dishonest" anyway.
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog semantics. >>> Only Prolog semantics is defined in the standard.
rCLProlog is an operational implementation of proof-theoretic semantics:
truth is derivability, and only well-founded proofs count.rCY
rCLIn proof-theoretic semantics, as reflected in the well-founded
semantics of logic programming, the Liar is rejected as a non-well-
founded goal.rCY
In proof-theoretic semantics, the Liar Paradox is not a genuine
contradiction but a non-well-founded construct, and thus not truth-apt.
Proof Theoretic Semantics is not the same as Truth Conditional Semantics.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
This is similar to semantically ungrounded (Kripke 1975) at the Tarski
object language level thus cannot be resolved to a truth value.
Outline of a Theory of Truth --- Saul Kripke
And the problem is that your "Proof Theoretic Semantics" isn't the logic domain of the problems you want to talk about.
On 1/11/26 9:25 AM, olcott wrote:
On 1/11/2026 4:26 AM, Mikko wrote:
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:
Non-programmers and non-Prolog programmers onlyI don't know about non-programmers but everyone who knows enough >>>>>>> about
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY. >>>>>>>
programming to be able to read the definition of the predicate
unify_with_occurs_check/2 can understand that its failure means that >>>>>>> the programmer does not like a cyclic structure at that point.
That is so stupidly wrong that it must be dishonest.
Prolog is what the standard says it is. You don't show any
contradiction
with the Prolog standard but dishonesstly say "dishonest" anyway.
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog semantics. >>> Only Prolog semantics is defined in the standard.
rCLProlog is an operational implementation of proof-theoretic semantics:
truth is derivability, and only well-founded proofs count.rCY
rCLIn proof-theoretic semantics, as reflected in the well-founded
semantics of logic programming, the Liar is rejected as a non-well-
founded goal.rCY
In proof-theoretic semantics, the Liar Paradox is not a genuine
contradiction but a non-well-founded construct, and thus not truth-apt.
Proof Theoretic Semantics is not the same as Truth Conditional Semantics.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
This is similar to semantically ungrounded (Kripke 1975) at the Tarski
object language level thus cannot be resolved to a truth value.
Outline of a Theory of Truth --- Saul Kripke
And the problem is that your "Proof Theoretic Semantics" isn't the logic domain of the problems you want to talk about.
On 1/11/2026 11:52 AM, Richard Damon wrote:
On 1/11/26 9:25 AM, olcott wrote:
On 1/11/2026 4:26 AM, Mikko wrote:
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:
Non-programmers and non-Prolog programmers onlyI don't know about non-programmers but everyone who knows enough >>>>>>>> about
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY. >>>>>>>>
programming to be able to read the definition of the predicate >>>>>>>> unify_with_occurs_check/2 can understand that its failure means >>>>>>>> that
the programmer does not like a cyclic structure at that point.
That is so stupidly wrong that it must be dishonest.
Prolog is what the standard says it is. You don't show any
contradiction
with the Prolog standard but dishonesstly say "dishonest" anyway.
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog
semantics.
Only Prolog semantics is defined in the standard.
rCLProlog is an operational implementation of proof-theoretic
semantics: truth is derivability, and only well-founded proofs count.rCY >>>
rCLIn proof-theoretic semantics, as reflected in the well-founded
semantics of logic programming, the Liar is rejected as a non-well-
founded goal.rCY
In proof-theoretic semantics, the Liar Paradox is not a genuine
contradiction but a non-well-founded construct, and thus not truth-apt.
Proof Theoretic Semantics is not the same as Truth Conditional
Semantics.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
This is similar to semantically ungrounded (Kripke 1975) at the
Tarski object language level thus cannot be resolved to a truth
value. Outline of a Theory of Truth --- Saul Kripke
And the problem is that your "Proof Theoretic Semantics" isn't the
logic domain of the problems you want to talk about.
It turns out that [Proof Theoretic Semantics] anchored in
-a A theory (over {E}) is defined as a conceptual class of
-a these elementary statements. Let {T} be such a theory.
-a Then the elementary statements which belong to {T} we
-a shall call the elementary theorems of {T}; we also say
-a that these elementary statements are true for {T}. Thus,
-a given {T}, an elementary theorem is an elementary
-a statement which is true. A theory is thus a way of
-a picking out from the statements of {E} a certain
-a subclass of true statementsrCa
Curry, Haskell 1977. Foundations of Mathematical
Logic. New York: Dover Publications, 45
Is the foundation of the system that I have been
talking about all of these years making
reCx ree T ((True(T, x) rei (T reo x))
and G||del Incompleteness impossible.
On 1/11/26 5:52 PM, olcott wrote:
On 1/11/2026 11:52 AM, Richard Damon wrote:
On 1/11/26 9:25 AM, olcott wrote:
On 1/11/2026 4:26 AM, Mikko wrote:
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:That is so stupidly wrong that it must be dishonest.
Non-programmers and non-Prolog programmers onlyI don't know about non-programmers but everyone who knows
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY. >>>>>>>>>
enough about
programming to be able to read the definition of the predicate >>>>>>>>> unify_with_occurs_check/2 can understand that its failure means >>>>>>>>> that
the programmer does not like a cyclic structure at that point. >>>>>>>
Prolog is what the standard says it is. You don't show any
contradiction
with the Prolog standard but dishonesstly say "dishonest" anyway. >>>>>>>
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog
semantics.
Only Prolog semantics is defined in the standard.
rCLProlog is an operational implementation of proof-theoretic
semantics: truth is derivability, and only well-founded proofs count.rCY >>>>
rCLIn proof-theoretic semantics, as reflected in the well-founded
semantics of logic programming, the Liar is rejected as a non-well-
founded goal.rCY
In proof-theoretic semantics, the Liar Paradox is not a genuine
contradiction but a non-well-founded construct, and thus not truth-apt. >>>>
Proof Theoretic Semantics is not the same as Truth Conditional
Semantics.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
This is similar to semantically ungrounded (Kripke 1975) at the
Tarski object language level thus cannot be resolved to a truth
value. Outline of a Theory of Truth --- Saul Kripke
And the problem is that your "Proof Theoretic Semantics" isn't the
logic domain of the problems you want to talk about.
It turns out that [Proof Theoretic Semantics] anchored in
-a-a A theory (over {E}) is defined as a conceptual class of
-a-a these elementary statements. Let {T} be such a theory.
-a-a Then the elementary statements which belong to {T} we
-a-a shall call the elementary theorems of {T}; we also say
-a-a that these elementary statements are true for {T}. Thus,
-a-a given {T}, an elementary theorem is an elementary
-a-a statement which is true. A theory is thus a way of
-a-a picking out from the statements of {E} a certain
-a-a subclass of true statementsrCa
Curry, Haskell 1977. Foundations of Mathematical
Logic. New York: Dover Publications, 45
Is the foundation of the system that I have been
talking about all of these years making
reCx ree T ((True(T, x) rei (T reo x))
and G||del Incompleteness impossible.
Nope. Read the last line, it say it allows picking out a certain
SUBCLASS of true statemensts, not that it picks out ALL true statements.
Proof SHOWS the statement to be true.
On 1/11/26 5:52 PM, olcott wrote:
On 1/11/2026 11:52 AM, Richard Damon wrote:
On 1/11/26 9:25 AM, olcott wrote:
On 1/11/2026 4:26 AM, Mikko wrote:
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:That is so stupidly wrong that it must be dishonest.
Non-programmers and non-Prolog programmers onlyI don't know about non-programmers but everyone who knows
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY. >>>>>>>>>
enough about
programming to be able to read the definition of the predicate >>>>>>>>> unify_with_occurs_check/2 can understand that its failure means >>>>>>>>> that
the programmer does not like a cyclic structure at that point. >>>>>>>
Prolog is what the standard says it is. You don't show any
contradiction
with the Prolog standard but dishonesstly say "dishonest" anyway. >>>>>>>
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog
semantics.
Only Prolog semantics is defined in the standard.
rCLProlog is an operational implementation of proof-theoretic
semantics: truth is derivability, and only well-founded proofs count.rCY >>>>
rCLIn proof-theoretic semantics, as reflected in the well-founded
semantics of logic programming, the Liar is rejected as a non-well-
founded goal.rCY
In proof-theoretic semantics, the Liar Paradox is not a genuine
contradiction but a non-well-founded construct, and thus not truth-apt. >>>>
Proof Theoretic Semantics is not the same as Truth Conditional
Semantics.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
This is similar to semantically ungrounded (Kripke 1975) at the
Tarski object language level thus cannot be resolved to a truth
value. Outline of a Theory of Truth --- Saul Kripke
And the problem is that your "Proof Theoretic Semantics" isn't the
logic domain of the problems you want to talk about.
It turns out that [Proof Theoretic Semantics] anchored in
-a-a A theory (over {E}) is defined as a conceptual class of
-a-a these elementary statements. Let {T} be such a theory.
-a-a Then the elementary statements which belong to {T} we
-a-a shall call the elementary theorems of {T}; we also say
-a-a that these elementary statements are true for {T}. Thus,
-a-a given {T}, an elementary theorem is an elementary
-a-a statement which is true. A theory is thus a way of
-a-a picking out from the statements of {E} a certain
-a-a subclass of true statementsrCa
Curry, Haskell 1977. Foundations of Mathematical
Logic. New York: Dover Publications, 45
Is the foundation of the system that I have been
talking about all of these years making
reCx ree T ((True(T, x) rei (T reo x))
and G||del Incompleteness impossible.
Nope. Read the last line, it say it allows picking out a certain
SUBCLASS of true statemensts, not that it picks out ALL true statements.
Proof SHOWS the statement to be true.
Not being able to prove a statement doesn't make it "not true", just not KNOWN true.
On 1/11/2026 9:37 PM, Richard Damon wrote:
On 1/11/26 5:52 PM, olcott wrote:
On 1/11/2026 11:52 AM, Richard Damon wrote:
On 1/11/26 9:25 AM, olcott wrote:
On 1/11/2026 4:26 AM, Mikko wrote:
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:That is so stupidly wrong that it must be dishonest.
Non-programmers and non-Prolog programmers only
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY.
I don't know about non-programmers but everyone who knows >>>>>>>>>> enough about
programming to be able to read the definition of the predicate >>>>>>>>>> unify_with_occurs_check/2 can understand that its failure >>>>>>>>>> means that
the programmer does not like a cyclic structure at that point. >>>>>>>>
Prolog is what the standard says it is. You don't show any
contradiction
with the Prolog standard but dishonesstly say "dishonest" anyway. >>>>>>>>
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog
semantics.
Only Prolog semantics is defined in the standard.
rCLProlog is an operational implementation of proof-theoretic
semantics: truth is derivability, and only well-founded proofs count.rCY >>>>>
rCLIn proof-theoretic semantics, as reflected in the well-founded
semantics of logic programming, the Liar is rejected as a non-well- >>>>> founded goal.rCY
In proof-theoretic semantics, the Liar Paradox is not a genuine
contradiction but a non-well-founded construct, and thus not truth- >>>>> apt.
Proof Theoretic Semantics is not the same as Truth Conditional
Semantics.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
This is similar to semantically ungrounded (Kripke 1975) at the
Tarski object language level thus cannot be resolved to a truth
value. Outline of a Theory of Truth --- Saul Kripke
And the problem is that your "Proof Theoretic Semantics" isn't the
logic domain of the problems you want to talk about.
It turns out that [Proof Theoretic Semantics] anchored in
-a-a A theory (over {E}) is defined as a conceptual class of
-a-a these elementary statements. Let {T} be such a theory.
-a-a Then the elementary statements which belong to {T} we
-a-a shall call the elementary theorems of {T}; we also say
-a-a that these elementary statements are true for {T}. Thus,
-a-a given {T}, an elementary theorem is an elementary
-a-a statement which is true. A theory is thus a way of
-a-a picking out from the statements of {E} a certain
-a-a subclass of true statementsrCa
Curry, Haskell 1977. Foundations of Mathematical
Logic. New York: Dover Publications, 45
Is the foundation of the system that I have been
talking about all of these years making
reCx ree T ((True(T, x) rei (T reo x))
and G||del Incompleteness impossible.
Nope. Read the last line, it say it allows picking out a certain
SUBCLASS of true statemensts, not that it picks out ALL true statements.
Proof SHOWS the statement to be true.
rCLThe system adopts Proof-Theoretic Semantics: meaning is determined by inferential role, and truth is internal to the theory. A theory T is
defined by a finite set of stipulated atomic statements together with
all expressions derivable from them under the inference rules. The statements belonging to T constitute its theorems, and these are exactly
the statements that are true-in-T.rCY reCx ree T ((True(T, x) rei (T reo x))
On 1/11/26 10:42 PM, olcott wrote:
On 1/11/2026 9:37 PM, Richard Damon wrote:
On 1/11/26 5:52 PM, olcott wrote:
On 1/11/2026 11:52 AM, Richard Damon wrote:
On 1/11/26 9:25 AM, olcott wrote:
On 1/11/2026 4:26 AM, Mikko wrote:
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:That is so stupidly wrong that it must be dishonest.
Non-programmers and non-Prolog programmers only
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY.
I don't know about non-programmers but everyone who knows >>>>>>>>>>> enough about
programming to be able to read the definition of the predicate >>>>>>>>>>> unify_with_occurs_check/2 can understand that its failure >>>>>>>>>>> means that
the programmer does not like a cyclic structure at that point. >>>>>>>>>
Prolog is what the standard says it is. You don't show any
contradiction
with the Prolog standard but dishonesstly say "dishonest" anyway. >>>>>>>>>
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog
semantics.
Only Prolog semantics is defined in the standard.
rCLProlog is an operational implementation of proof-theoretic
semantics: truth is derivability, and only well-founded proofs
count.rCY
rCLIn proof-theoretic semantics, as reflected in the well-founded >>>>>> semantics of logic programming, the Liar is rejected as a non-
well- founded goal.rCY
In proof-theoretic semantics, the Liar Paradox is not a genuine
contradiction but a non-well-founded construct, and thus not
truth- apt.
Proof Theoretic Semantics is not the same as Truth Conditional
Semantics.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
This is similar to semantically ungrounded (Kripke 1975) at the
Tarski object language level thus cannot be resolved to a truth
value. Outline of a Theory of Truth --- Saul Kripke
And the problem is that your "Proof Theoretic Semantics" isn't the
logic domain of the problems you want to talk about.
It turns out that [Proof Theoretic Semantics] anchored in
-a-a A theory (over {E}) is defined as a conceptual class of
-a-a these elementary statements. Let {T} be such a theory.
-a-a Then the elementary statements which belong to {T} we
-a-a shall call the elementary theorems of {T}; we also say
-a-a that these elementary statements are true for {T}. Thus,
-a-a given {T}, an elementary theorem is an elementary
-a-a statement which is true. A theory is thus a way of
-a-a picking out from the statements of {E} a certain
-a-a subclass of true statementsrCa
Curry, Haskell 1977. Foundations of Mathematical
Logic. New York: Dover Publications, 45
Is the foundation of the system that I have been
talking about all of these years making
reCx ree T ((True(T, x) rei (T reo x))
and G||del Incompleteness impossible.
Nope. Read the last line, it say it allows picking out a certain
SUBCLASS of true statemensts, not that it picks out ALL true statements. >>>
Proof SHOWS the statement to be true.
rCLThe system adopts Proof-Theoretic Semantics: meaning is determined by
inferential role, and truth is internal to the theory. A theory T is
defined by a finite set of stipulated atomic statements together with
all expressions derivable from them under the inference rules. The
statements belonging to T constitute its theorems, and these are
exactly the statements that are true-in-T.rCY reCx ree T ((True(T, x) rei (T reo
x))
I think the issue is that this "Proof-Theoretic Semantics" can't
actually handle systems like Peano Arithmatic.
In that case, it doesn't refute Godel's incompleteness Theorem, as that--
had as its precondition that ability to support the defintions of the Natural Numbers.
So, your problem is that, since you don't actually understand what any
of these fields are actually doing, you don't know which ones are
actualy applicable to the problem you want to deal with.
Since "Computation Theory" has at its foundation things that need to
have the properties of the Natural Numbers available, your systems that can't handle them are just not applicable.
On 1/11/26 9:25 AM, olcott wrote:
On 1/11/2026 4:26 AM, Mikko wrote:
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:
Non-programmers and non-Prolog programmers onlyI don't know about non-programmers but everyone who knows enough >>>>>>> about
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY. >>>>>>>
programming to be able to read the definition of the predicate
unify_with_occurs_check/2 can understand that its failure means that >>>>>>> the programmer does not like a cyclic structure at that point.
That is so stupidly wrong that it must be dishonest.
Prolog is what the standard says it is. You don't show any
contradiction
with the Prolog standard but dishonesstly say "dishonest" anyway.
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog semantics. >>> Only Prolog semantics is defined in the standard.
rCLProlog is an operational implementation of proof-theoretic semantics:
truth is derivability, and only well-founded proofs count.rCY
rCLIn proof-theoretic semantics, as reflected in the well-founded
semantics of logic programming, the Liar is rejected as a non-well-
founded goal.rCY
In proof-theoretic semantics, the Liar Paradox is not a genuine
contradiction but a non-well-founded construct, and thus not truth-apt.
Proof Theoretic Semantics is not the same as Truth Conditional Semantics.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
This is similar to semantically ungrounded (Kripke 1975) at the Tarski
object language level thus cannot be resolved to a truth value.
Outline of a Theory of Truth --- Saul Kripke
And the problem is that your "Proof Theoretic Semantics" isn't the logic domain of the problems you want to talk about.
On 1/11/26 9:25 AM, olcott wrote:
On 1/11/2026 4:26 AM, Mikko wrote:
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:
Non-programmers and non-Prolog programmers onlyI don't know about non-programmers but everyone who knows enough >>>>>>> about
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY. >>>>>>>
programming to be able to read the definition of the predicate
unify_with_occurs_check/2 can understand that its failure means that >>>>>>> the programmer does not like a cyclic structure at that point.
That is so stupidly wrong that it must be dishonest.
Prolog is what the standard says it is. You don't show any
contradiction
with the Prolog standard but dishonesstly say "dishonest" anyway.
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog semantics. >>> Only Prolog semantics is defined in the standard.
rCLProlog is an operational implementation of proof-theoretic semantics:
truth is derivability, and only well-founded proofs count.rCY
rCLIn proof-theoretic semantics, as reflected in the well-founded
semantics of logic programming, the Liar is rejected as a non-well-
founded goal.rCY
In proof-theoretic semantics, the Liar Paradox is not a genuine
contradiction but a non-well-founded construct, and thus not truth-apt.
Proof Theoretic Semantics is not the same as Truth Conditional Semantics.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
This is similar to semantically ungrounded (Kripke 1975) at the Tarski
object language level thus cannot be resolved to a truth value.
Outline of a Theory of Truth --- Saul Kripke
And the problem is that your "Proof Theoretic Semantics" isn't the logic domain of the problems you want to talk about.
On 1/11/2026 4:26 AM, Mikko wrote:
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:
Non-programmers and non-Prolog programmers onlyI don't know about non-programmers but everyone who knows enough
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY. >>>>>>
about
programming to be able to read the definition of the predicate
unify_with_occurs_check/2 can understand that its failure means that >>>>>> the programmer does not like a cyclic structure at that point.
That is so stupidly wrong that it must be dishonest.
Prolog is what the standard says it is. You don't show any
contradiction
with the Prolog standard but dishonesstly say "dishonest" anyway.
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog semantics.
Only Prolog semantics is defined in the standard.
rCLProlog is an operational implementation of proof-theoretic semantics: truth is derivability, and only well-founded proofs count.rCY
On 1/11/2026 10:00 PM, Richard Damon wrote:
On 1/11/26 10:42 PM, olcott wrote:
On 1/11/2026 9:37 PM, Richard Damon wrote:
On 1/11/26 5:52 PM, olcott wrote:
On 1/11/2026 11:52 AM, Richard Damon wrote:
On 1/11/26 9:25 AM, olcott wrote:
On 1/11/2026 4:26 AM, Mikko wrote:
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:That is so stupidly wrong that it must be dishonest.
Non-programmers and non-Prolog programmers only
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY.
I don't know about non-programmers but everyone who knows >>>>>>>>>>>> enough about
programming to be able to read the definition of the predicate >>>>>>>>>>>> unify_with_occurs_check/2 can understand that its failure >>>>>>>>>>>> means that
the programmer does not like a cyclic structure at that point. >>>>>>>>>>
Prolog is what the standard says it is. You don't show any >>>>>>>>>> contradiction
with the Prolog standard but dishonesstly say "dishonest" anyway. >>>>>>>>>>
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog >>>>>>>> semantics.
Only Prolog semantics is defined in the standard.
rCLProlog is an operational implementation of proof-theoretic
semantics: truth is derivability, and only well-founded proofs
count.rCY
rCLIn proof-theoretic semantics, as reflected in the well-founded >>>>>>> semantics of logic programming, the Liar is rejected as a non-
well- founded goal.rCY
In proof-theoretic semantics, the Liar Paradox is not a genuine >>>>>>> contradiction but a non-well-founded construct, and thus not
truth- apt.
Proof Theoretic Semantics is not the same as Truth Conditional
Semantics.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
This is similar to semantically ungrounded (Kripke 1975) at the >>>>>>> Tarski object language level thus cannot be resolved to a truth >>>>>>> value. Outline of a Theory of Truth --- Saul Kripke
And the problem is that your "Proof Theoretic Semantics" isn't the >>>>>> logic domain of the problems you want to talk about.
It turns out that [Proof Theoretic Semantics] anchored in
-a-a A theory (over {E}) is defined as a conceptual class of
-a-a these elementary statements. Let {T} be such a theory.
-a-a Then the elementary statements which belong to {T} we
-a-a shall call the elementary theorems of {T}; we also say
-a-a that these elementary statements are true for {T}. Thus,
-a-a given {T}, an elementary theorem is an elementary
-a-a statement which is true. A theory is thus a way of
-a-a picking out from the statements of {E} a certain
-a-a subclass of true statementsrCa
Curry, Haskell 1977. Foundations of Mathematical
Logic. New York: Dover Publications, 45
Is the foundation of the system that I have been
talking about all of these years making
reCx ree T ((True(T, x) rei (T reo x))
and G||del Incompleteness impossible.
Nope. Read the last line, it say it allows picking out a certain
SUBCLASS of true statemensts, not that it picks out ALL true
statements.
Proof SHOWS the statement to be true.
rCLThe system adopts Proof-Theoretic Semantics: meaning is determined
by inferential role, and truth is internal to the theory. A theory T
is defined by a finite set of stipulated atomic statements together
with all expressions derivable from them under the inference rules.
The statements belonging to T constitute its theorems, and these are
exactly the statements that are true-in-T.rCY reCx ree T ((True(T, x) rei (T
reo x))
I think the issue is that this "Proof-Theoretic Semantics" can't
actually handle systems like Peano Arithmatic.
It turns out that they can and much much more. So what
I have been saying all these years is about G||del is
essentially "Proof-Theoretic Semantics".
In that case, it doesn't refute Godel's incompleteness Theorem, as
that had as its precondition that ability to support the defintions of
the Natural Numbers.
So, your problem is that, since you don't actually understand what any
of these fields are actually doing, you don't know which ones are
actualy applicable to the problem you want to deal with.
Since "Computation Theory" has at its foundation things that need to
have the properties of the Natural Numbers available, your systems
that can't handle them are just not applicable.
On 1/11/26 11:33 PM, olcott wrote:
On 1/11/2026 10:00 PM, Richard Damon wrote:
On 1/11/26 10:42 PM, olcott wrote:
On 1/11/2026 9:37 PM, Richard Damon wrote:
On 1/11/26 5:52 PM, olcott wrote:
On 1/11/2026 11:52 AM, Richard Damon wrote:
On 1/11/26 9:25 AM, olcott wrote:
On 1/11/2026 4:26 AM, Mikko wrote:
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:That is so stupidly wrong that it must be dishonest.
Non-programmers and non-Prolog programmers only
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY.
I don't know about non-programmers but everyone who knows >>>>>>>>>>>>> enough about
programming to be able to read the definition of the predicate >>>>>>>>>>>>> unify_with_occurs_check/2 can understand that its failure >>>>>>>>>>>>> means that
the programmer does not like a cyclic structure at that point. >>>>>>>>>>>
Prolog is what the standard says it is. You don't show any >>>>>>>>>>> contradiction
with the Prolog standard but dishonesstly say "dishonest" >>>>>>>>>>> anyway.
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog >>>>>>>>> semantics.
Only Prolog semantics is defined in the standard.
rCLProlog is an operational implementation of proof-theoretic >>>>>>>> semantics: truth is derivability, and only well-founded proofs >>>>>>>> count.rCY
rCLIn proof-theoretic semantics, as reflected in the well-founded >>>>>>>> semantics of logic programming, the Liar is rejected as a non- >>>>>>>> well- founded goal.rCY
In proof-theoretic semantics, the Liar Paradox is not a genuine >>>>>>>> contradiction but a non-well-founded construct, and thus not
truth- apt.
Proof Theoretic Semantics is not the same as Truth Conditional >>>>>>>> Semantics.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
This is similar to semantically ungrounded (Kripke 1975) at the >>>>>>>> Tarski object language level thus cannot be resolved to a truth >>>>>>>> value. Outline of a Theory of Truth --- Saul Kripke
And the problem is that your "Proof Theoretic Semantics" isn't
the logic domain of the problems you want to talk about.
It turns out that [Proof Theoretic Semantics] anchored in
-a-a A theory (over {E}) is defined as a conceptual class of
-a-a these elementary statements. Let {T} be such a theory.
-a-a Then the elementary statements which belong to {T} we
-a-a shall call the elementary theorems of {T}; we also say
-a-a that these elementary statements are true for {T}. Thus,
-a-a given {T}, an elementary theorem is an elementary
-a-a statement which is true. A theory is thus a way of
-a-a picking out from the statements of {E} a certain
-a-a subclass of true statementsrCa
Curry, Haskell 1977. Foundations of Mathematical
Logic. New York: Dover Publications, 45
Is the foundation of the system that I have been
talking about all of these years making
reCx ree T ((True(T, x) rei (T reo x))
and G||del Incompleteness impossible.
Nope. Read the last line, it say it allows picking out a certain
SUBCLASS of true statemensts, not that it picks out ALL true
statements.
Proof SHOWS the statement to be true.
rCLThe system adopts Proof-Theoretic Semantics: meaning is determined >>>> by inferential role, and truth is internal to the theory. A theory T
is defined by a finite set of stipulated atomic statements together
with all expressions derivable from them under the inference rules.
The statements belonging to T constitute its theorems, and these are
exactly the statements that are true-in-T.rCY reCx ree T ((True(T, x) rei (T
reo x))
I think the issue is that this "Proof-Theoretic Semantics" can't
actually handle systems like Peano Arithmatic.
It turns out that they can and much much more. So what
I have been saying all these years is about G||del is
essentially "Proof-Theoretic Semantics".
Considering your history, you got anything that supports that claim?
In that case, it doesn't refute Godel's incompleteness Theorem, as
that had as its precondition that ability to support the defintions
of the Natural Numbers.
So, your problem is that, since you don't actually understand what
any of these fields are actually doing, you don't know which ones are
actualy applicable to the problem you want to deal with.
Since "Computation Theory" has at its foundation things that need to
have the properties of the Natural Numbers available, your systems
that can't handle them are just not applicable.
On 1/12/2026 5:56 AM, Richard Damon wrote:
On 1/11/26 11:33 PM, olcott wrote:
On 1/11/2026 10:00 PM, Richard Damon wrote:
On 1/11/26 10:42 PM, olcott wrote:
On 1/11/2026 9:37 PM, Richard Damon wrote:
On 1/11/26 5:52 PM, olcott wrote:
On 1/11/2026 11:52 AM, Richard Damon wrote:
On 1/11/26 9:25 AM, olcott wrote:
On 1/11/2026 4:26 AM, Mikko wrote:
On 10/01/2026 18:11, olcott wrote:
On 1/10/2026 3:02 AM, Mikko wrote:
On 09/01/2026 17:53, olcott wrote:
On 1/9/2026 4:03 AM, Mikko wrote:
On 09/01/2026 01:28, olcott wrote:
Non-programmers and non-Prolog programmers only
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY.
I don't know about non-programmers but everyone who knows >>>>>>>>>>>>>> enough about
programming to be able to read the definition of the >>>>>>>>>>>>>> predicate
unify_with_occurs_check/2 can understand that its failure >>>>>>>>>>>>>> means that
the programmer does not like a cyclic structure at that >>>>>>>>>>>>>> point.
That is so stupidly wrong that it must be dishonest.
Prolog is what the standard says it is. You don't show any >>>>>>>>>>>> contradiction
with the Prolog standard but dishonesstly say "dishonest" >>>>>>>>>>>> anyway.
I could not get a copy of the standard to prove
that I am correct its costs $600.
Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf
rCLIn proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.rCY
That is about the proof-theoretic semantics, not about Prolog >>>>>>>>>> semantics.
Only Prolog semantics is defined in the standard.
rCLProlog is an operational implementation of proof-theoretic >>>>>>>>> semantics: truth is derivability, and only well-founded proofs >>>>>>>>> count.rCY
rCLIn proof-theoretic semantics, as reflected in the well-founded >>>>>>>>> semantics of logic programming, the Liar is rejected as a non- >>>>>>>>> well- founded goal.rCY
In proof-theoretic semantics, the Liar Paradox is not a genuine >>>>>>>>> contradiction but a non-well-founded construct, and thus not >>>>>>>>> truth- apt.
Proof Theoretic Semantics is not the same as Truth Conditional >>>>>>>>> Semantics.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
This is similar to semantically ungrounded (Kripke 1975) at the >>>>>>>>> Tarski object language level thus cannot be resolved to a truth >>>>>>>>> value. Outline of a Theory of Truth --- Saul Kripke
And the problem is that your "Proof Theoretic Semantics" isn't >>>>>>>> the logic domain of the problems you want to talk about.
It turns out that [Proof Theoretic Semantics] anchored in
-a-a A theory (over {E}) is defined as a conceptual class of
-a-a these elementary statements. Let {T} be such a theory.
-a-a Then the elementary statements which belong to {T} we
-a-a shall call the elementary theorems of {T}; we also say
-a-a that these elementary statements are true for {T}. Thus,
-a-a given {T}, an elementary theorem is an elementary
-a-a statement which is true. A theory is thus a way of
-a-a picking out from the statements of {E} a certain
-a-a subclass of true statementsrCa
Curry, Haskell 1977. Foundations of Mathematical
Logic. New York: Dover Publications, 45
Is the foundation of the system that I have been
talking about all of these years making
reCx ree T ((True(T, x) rei (T reo x))
and G||del Incompleteness impossible.
Nope. Read the last line, it say it allows picking out a certain
SUBCLASS of true statemensts, not that it picks out ALL true
statements.
Proof SHOWS the statement to be true.
rCLThe system adopts Proof-Theoretic Semantics: meaning is determined >>>>> by inferential role, and truth is internal to the theory. A theory
T is defined by a finite set of stipulated atomic statements
together with all expressions derivable from them under the
inference rules. The statements belonging to T constitute its
theorems, and these are exactly the statements that are true-in-T.rCY >>>>> reCx ree T ((True(T, x) rei (T reo x))
I think the issue is that this "Proof-Theoretic Semantics" can't
actually handle systems like Peano Arithmatic.
It turns out that they can and much much more. So what
I have been saying all these years is about G||del is
essentially "Proof-Theoretic Semantics".
Considering your history, you got anything that supports that claim?
Why PA is fully expressible in this system
Peano Arithmetic (PA) fits perfectly into this framework because:
PA is a recursively axiomatized theory with a finite set of primitive symbols.
Its axioms and inference rules are finitary and syntactic, exactly the
kind of rules this system treats as meaning-giving.
Every PA proof is a finite, well-founded derivation, so PArCOs theorems
are automatically rCLtrue-in-PArCY in this sense.
PArCOs refutations (proofs of negations) are likewise finite, so PArCOs falsehoods are rCLfalse-in-PArCY.
PArCOs independent sentences (G||del, Rosser, ParisrCoHarrington, etc.) naturally fall into the non-well-founded category, since their
inferential roles cannot be grounded within PArCOs proof system.
Nothing in PA requires model-theoretic truth, infinite structures, or semantic notions beyond what this system provides. PArCOs entire content rCo its syntax, its proofs, its derivations, and its independence phenomena
rCo is fully captured by these three proof-theoretic statuses.
In short: PA is fully expressible because everything PA does is already proof-theoretic, and this systemrCOs semantics is defined entirely in proof-theoretic terms.
In that case, it doesn't refute Godel's incompleteness Theorem, as
that had as its precondition that ability to support the defintions
of the Natural Numbers.
So, your problem is that, since you don't actually understand what
any of these fields are actually doing, you don't know which ones
are actualy applicable to the problem you want to deal with.
Since "Computation Theory" has at its foundation things that need to
have the properties of the Natural Numbers available, your systems
that can't handle them are just not applicable.
| Sysop: | Amessyroom |
|---|---|
| Location: | Fayetteville, NC |
| Users: | 54 |
| Nodes: | 6 (1 / 5) |
| Uptime: | 24:28:31 |
| Calls: | 742 |
| Files: | 1,218 |
| D/L today: |
7 files (8,805K bytes) |
| Messages: | 187,121 |
| Posted today: | 1 |