Non-programmers and non-Prolog programmers only
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY.
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.
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.
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
Non-programmers and non-Prolog programmers only
understand OccursrCacheck failure as rCLProlog doesnrCOt like itrCY.
When you write LP = not(true(LP)) you are defining LP
in terms of itself with no base case. If you try to
expand the structure, you get: not(true(not(true(not(true(not(true(rCa))))))))
The expansion never bottoms out. It is an infinite
regress. Most Prolog systems will show a cyclic term
if you run:?- LP = not(true(LP)).
But this is only a compact representation. It is not
a wellrCafounded term in the ISO sense.
If you enforce the ISO occurs check:
?- unify_with_occurs_check(LP, not(true(LP))).
you get: false.
OccursrCacheck failure has a precise meaning:
the unification would create a nonrCawellrCafounded term
whose structure expands forever. ISO Prolog requires
all terms to be finite and wellrCafounded, so the
unification must fail.
For nonrCaProlog programmers: occursrCacheck failure means
the system was about to build a data structure that
expands forever. No finite machine can represent that
safely. If Prolog actually tried to expand it, it would
recurse until it ran out of memory. So Prolog correctly
rejects it.
Conclusion: LP = not(true(LP)) is formally illrCafounded
in PrologrCOs term model. Its structural expansion is
infinite, it violates the wellrCafoundedness requirement for
terms, and unify_with_occurs_check/2 correctly detects
this. Because the term cannot be wellrCafounded, it cannot
be assigned a truth value in any wellrCafounded interpretation.
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.
How The Well-Founded Semantics for General Logic Programs
of (Van Gelder, Ross & Schlipf, 1991)
Journal of the Association for Computing Machinery,
volume 38, number 3, pp. 620{650 (1991). https://users.soe.ucsc.edu/%7Eavg/Papers/wf.pdf
handle the Liar Paradox when we construe
non-well-founded / undefined as not a truth-bearer?
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
WFS assigns undefined to self-referential paradoxes
without external support.
When we interpret undefined as lack of truth-bearer
status the Liar sentence fails to be about anything
that can bear truth values
The paradox dissolves - there's no contradiction
because there's no genuine proposition
This is actually similar to how some philosophers
(like the "gap theorists") handle the Liar: sentences
that fail to achieve determinate truth conditions
simply aren't truth-bearers. WFS's undefined value
provides a formal mechanism for identifying exactly
these cases.
A Subtle Point The occurs-check failure in Prolog is
slightly different from WFS's undefined assignment -
it's a structural constraint on term formation. But
both point to the same insight: circular, unsupported
self-reference doesn't create genuine semantic content.
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.
On 1/12/26 4:41 PM, olcott wrote:
How The Well-Founded Semantics for General Logic Programs
of (Van Gelder, Ross & Schlipf, 1991)
Journal of the Association for Computing Machinery,
volume 38, number 3, pp. 620{650 (1991).
https://users.soe.ucsc.edu/%7Eavg/Papers/wf.pdf
handle the Liar Paradox when we construe
non-well-founded / undefined as not a truth-bearer?
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
WFS assigns undefined to self-referential paradoxes
without external support.
When we interpret undefined as lack of truth-bearer
status the Liar sentence fails to be about anything
that can bear truth values
The paradox dissolves - there's no contradiction
because there's no genuine proposition
This is actually similar to how some philosophers
(like the "gap theorists") handle the Liar: sentences
that fail to achieve determinate truth conditions
simply aren't truth-bearers. WFS's undefined value
provides a formal mechanism for identifying exactly
these cases.
A Subtle Point The occurs-check failure in Prolog is
slightly different from WFS's undefined assignment -
it's a structural constraint on term formation. But
both point to the same insight: circular, unsupported
self-reference doesn't create genuine semantic content.
I thought you said that no one in the past handled the liar paradox?
I guess you are just admitting you are just a liar.
Note, since Prolog's logic is not sufficient to handle PA,
your argument--
here doesn't affect the logic system that you are trying to argue about,
and you are just showing that you don't understand that difference.
Many system can handle some self-references, which Prolog, and yours,
can't.
On 1/12/2026 9:16 PM, Richard Damon wrote:
On 1/12/26 4:41 PM, olcott wrote:
How The Well-Founded Semantics for General Logic Programs
of (Van Gelder, Ross & Schlipf, 1991)
Journal of the Association for Computing Machinery,
volume 38, number 3, pp. 620{650 (1991).
https://users.soe.ucsc.edu/%7Eavg/Papers/wf.pdf
handle the Liar Paradox when we construe
non-well-founded / undefined as not a truth-bearer?
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
WFS assigns undefined to self-referential paradoxes
without external support.
When we interpret undefined as lack of truth-bearer
status the Liar sentence fails to be about anything
that can bear truth values
The paradox dissolves - there's no contradiction
because there's no genuine proposition
This is actually similar to how some philosophers
(like the "gap theorists") handle the Liar: sentences
that fail to achieve determinate truth conditions
simply aren't truth-bearers. WFS's undefined value
provides a formal mechanism for identifying exactly
these cases.
A Subtle Point The occurs-check failure in Prolog is
slightly different from WFS's undefined assignment -
it's a structural constraint on term formation. But
both point to the same insight: circular, unsupported
self-reference doesn't create genuine semantic content.
I thought you said that no one in the past handled the liar paradox?
That is no one in the past handling the Liar Paradox.
That all happened today.
I guess you are just admitting you are just a liar.
Note, since Prolog's logic is not sufficient to handle PA,
I never said it was. A formal system anchored in
Proof Theoretic Semantics is powerful enough.
your argument here doesn't affect the logic system that you are trying
to argue about, and you are just showing that you don't understand
that difference.
Many system can handle some self-references, which Prolog, and yours,
can't.
On 1/12/26 11:46 PM, olcott wrote:
On 1/12/2026 9:16 PM, Richard Damon wrote:
On 1/12/26 4:41 PM, olcott wrote:
How The Well-Founded Semantics for General Logic Programs
of (Van Gelder, Ross & Schlipf, 1991)
Journal of the Association for Computing Machinery,
volume 38, number 3, pp. 620{650 (1991).
https://users.soe.ucsc.edu/%7Eavg/Papers/wf.pdf
handle the Liar Paradox when we construe
non-well-founded / undefined as not a truth-bearer?
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
WFS assigns undefined to self-referential paradoxes
without external support.
When we interpret undefined as lack of truth-bearer
status the Liar sentence fails to be about anything
that can bear truth values
The paradox dissolves - there's no contradiction
because there's no genuine proposition
This is actually similar to how some philosophers
(like the "gap theorists") handle the Liar: sentences
that fail to achieve determinate truth conditions
simply aren't truth-bearers. WFS's undefined value
provides a formal mechanism for identifying exactly
these cases.
A Subtle Point The occurs-check failure in Prolog is
slightly different from WFS's undefined assignment -
it's a structural constraint on term formation. But
both point to the same insight: circular, unsupported
self-reference doesn't create genuine semantic content.
I thought you said that no one in the past handled the liar paradox?
That is no one in the past handling the Liar Paradox.
That all happened today.
So, today is 1991?
I guess you are just admitting you are just a liar.
Note, since Prolog's logic is not sufficient to handle PA,
I never said it was. A formal system anchored in
Proof Theoretic Semantics is powerful enough.
Nope. It can't handle PA.
your argument here doesn't affect the logic system that you are
trying to argue about, and you are just showing that you don't
understand that difference.
Many system can handle some self-references, which Prolog, and yours,
can't.
| Sysop: | Amessyroom |
|---|---|
| Location: | Fayetteville, NC |
| Users: | 54 |
| Nodes: | 6 (0 / 6) |
| Uptime: | 19:05:47 |
| Calls: | 742 |
| Files: | 1,218 |
| D/L today: |
5 files (8,203K bytes) |
| Messages: | 184,913 |
| Posted today: | 1 |