olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = not(provable(
F, G))" can be proven for some F and some G. The answer is that it can
for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G = not(provable
(F, G))" can be proven for some F and some G that do not contain cycles.
The answer is that in the proof system of Prolog it cannot be.
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings ofFor sufficiently informal definitions of "value".
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does not. >>>>
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = not(provable(
F, G))" can be proven for some F and some G. The answer is that it can
for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G = not(provable
(F, G))" can be proven for some F and some G that do not contain cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings ofFor sufficiently informal definitions of "value".
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does not. >>>>>
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = not(provable( >>> F, G))" can be proven for some F and some G. The answer is that it can
for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G = not(provable >>> (F, G))" can be proven for some F and some G that do not contain cycles. >>> The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
When "G = not(provable(F, G))." is used as a Prolog goal the
applied semantics is what Prolog lauguage definition specifies.
Does "semantically sound" mean something in that context?
At least your Prolog interpretation finds it meaningful. It determines
that the excution of that goal succeeds and assigns a value G but not
to F.
On 12/6/2025 3:30 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does >>>>>>>> not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that it can >>>> for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G =
not(provable
(F, G))" can be proven for some F and some G that do not contain
cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
When "G = not(provable(F, G))." is used as a Prolog goal the
applied semantics is what Prolog lauguage definition specifies.
Does "semantically sound" mean something in that context?
At least your Prolog interpretation finds it meaningful. It determines
that the excution of that goal succeeds and assigns a value G but not
to F.
Is this sentence true or false:
"This sentence is not true"
It is not semantically sound.
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings ofFor sufficiently informal definitions of "value".
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does not. >>>>
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = not(provable(
F, G))" can be proven for some F and some G. The answer is that it can
for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G = not(provable
(F, G))" can be proven for some F and some G that do not contain cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings ofFor sufficiently informal definitions of "value".
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does not. >>>>>
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = not(provable( >>> F, G))" can be proven for some F and some G. The answer is that it can
for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G = not(provable >>> (F, G))" can be proven for some F and some G that do not contain cycles. >>> The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
olcott kirjoitti 6.12.2025 klo 14.50:
On 12/6/2025 3:30 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does >>>>>>>>> not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that it can >>>>> for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G =
not(provable
(F, G))" can be proven for some F and some G that do not contain
cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
When "G = not(provable(F, G))." is used as a Prolog goal the
applied semantics is what Prolog lauguage definition specifies.
Does "semantically sound" mean something in that context?
At least your Prolog interpretation finds it meaningful. It determines
that the excution of that goal succeeds and assigns a value G but not
to F.
Is this sentence true or false:
"This sentence is not true"
It is not semantically sound.
Formal systems we usually use have no expression for "this".
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does >>>>>>>> not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that it can >>>> for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G =
not(provable
(F, G))" can be proven for some F and some G that do not contain
cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter does >>>>>>>>> not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that it can >>>>> for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G =
not(provable
(F, G))" can be proven for some F and some G that do not contain
cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G))
to a truth value true. When doing so it evaluated each side of =
to a value that is not a truth value.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)...
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate unify_with_occurs_check/2 is used explicitly instead of the normal unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable. END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg: Springer-Verlag.
On 10/12/2025 14:10, olcott wrote:
BEGIN:(Clocksin & Mellish 2003:254)...
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
You're a veritable treasure-trove.
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:% This sentence cannot be proven in F
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter >>>>>>>>>> does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means. >>>>>>
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that it >>>>>> can
for every F and for (at least) one G, which is not(provable(G)).
The second query can be regarded as a question whether "G =
not(provable
(F, G))" can be proven for some F and some G that do not contain
cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G))
to a truth value true. When doing so it evaluated each side of =
to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate unify_with_occurs_check/2 is used explicitly instead of the normal unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable. END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg: Springer-Verlag.
olcott kirjoitti 10.12.2025 klo 16.10:
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:% This sentence cannot be proven in F
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))).
are different. The former assigns a value to G, the latter >>>>>>>>>>> does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means. >>>>>>>
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that >>>>>>> it can
for every F and for (at least) one G, which is not(provable(G)). >>>>>>>
The second query can be regarded as a question whether "G =
not(provable
(F, G))" can be proven for some F and some G that do not contain >>>>>>> cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G))
to a truth value true. When doing so it evaluated each side of =
to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
Thank you for the confirmation of my explanation of your error.
As I say non-terminating, thus never resolves to a truth value.Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
olcott kirjoitti 10.12.2025 klo 16.10:
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
As I say non-terminating, thus never resolves to a truth value.
olcott kirjoitti 10.12.2025 klo 16.10:
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
On 11/12/2025 14:17, olcott wrote:
As I say non-terminating, thus never resolves to a truth value.
$ export S='G=foo(G).'; gprolog <<<"$S"; swipl <<<"$S"
GNU Prolog 1.4.5 (64 bits)
Compiled Feb 23 2020, 20:14:50 with gcc
By Daniel Diaz
Copyright (C) 1999-2020 Daniel Diaz
| ?-
cannot display cyclic term for G
yes
| ?-
Welcome to SWI-Prolog (threaded, 64 bits, version 8.4.2)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.
For online help and background, visit https://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).
G = foo(G).
% halt
On 12/11/2025 5:28 PM, Tristan Wibberley wrote:
olcott kirjoitti 10.12.2025 klo 16.10:
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
On 11/12/2025 14:17, olcott wrote:
As I say non-terminating, thus never resolves to a truth value.
$ export S='G=foo(G).'; gprolog <<<"$S"; swipl <<<"$S"
GNU Prolog 1.4.5 (64 bits)
Compiled Feb 23 2020, 20:14:50 with gcc
By Daniel Diaz
Copyright (C) 1999-2020 Daniel Diaz
| ?-
cannot display cyclic term for G
yes
| ?-
Welcome to SWI-Prolog (threaded, 64 bits, version 8.4.2)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.
For online help and background, visit https://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).
G = foo(G).
% halt
Run SWI-Prolog
paste "G = not(provable(F, G))."
at the ?- prompt ending up this:
?- G = not(provable(F, G)).
Then you hit return and get this:
G = not(provable(F, G)).
Then you past this: "unify_with_occurs_check(G, not(provable(F, G)))."
at the next ?- prompt and get this
?- unify_with_occurs_check(G, not(provable(F, G))).
You hit return and get this:
false
*It all ends up looking like this*
*It all ends up looking like this*
*It all ends up looking like this*
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
On 12/11/2025 2:42 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 16.10:
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:% This sentence cannot be proven in F
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>> are different. The former assigns a value to G, the latter >>>>>>>>>>>> does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable means. >>>>>>>>
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that >>>>>>>> it can
for every F and for (at least) one G, which is not(provable(G)). >>>>>>>>
The second query can be regarded as a question whether "G =
not(provable
(F, G))" can be proven for some F and some G that do not contain >>>>>>>> cycles.
The answer is that in the proof system of Prolog it cannot be.
No that it flatly incorrect. The second question is this:
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G))
to a truth value true. When doing so it evaluated each side of =
to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
Thank you for the confirmation of my explanation of your error.
As I say non-terminating, thus never resolves to a truth value.Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
olcott kirjoitti 11.12.2025 klo 16.17:
On 12/11/2025 2:42 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 16.10:As I say non-terminating, thus never resolves to a truth value.
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:No that it flatly incorrect. The second question is this:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>> are different. The former assigns a value to G, the latter >>>>>>>>>>>>> does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable >>>>>>>>>>> means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G =
not(provable(
F, G))" can be proven for some F and some G. The answer is that >>>>>>>>> it can
for every F and for (at least) one G, which is not(provable(G)). >>>>>>>>>
The second query can be regarded as a question whether "G = >>>>>>>>> not(provable
(F, G))" can be proven for some F and some G that do not
contain cycles.
The answer is that in the proof system of Prolog it cannot be. >>>>>>>>
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G))
to a truth value true. When doing so it evaluated each side of =
to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
Thank you for the confirmation of my explanation of your error.
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
As according to Prolog rules foo(Y) isn't a truth value for any Y
the above is obviously just an attempt to deive with a distraction.
On 12/12/2025 2:50 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.17:
On 12/11/2025 2:42 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 16.10:As I say non-terminating, thus never resolves to a truth value.
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:No that it flatly incorrect. The second question is this:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>> are different. The former assigns a value to G, the latter >>>>>>>>>>>>>> does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable >>>>>>>>>>>> means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = >>>>>>>>>> not(provable(
F, G))" can be proven for some F and some G. The answer is >>>>>>>>>> that it can
for every F and for (at least) one G, which is not(provable(G)). >>>>>>>>>>
The second query can be regarded as a question whether "G = >>>>>>>>>> not(provable
(F, G))" can be proven for some F and some G that do not
contain cycles.
The answer is that in the proof system of Prolog it cannot be. >>>>>>>>>
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G))
to a truth value true. When doing so it evaluated each side of =
to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
Thank you for the confirmation of my explanation of your error.
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
As according to Prolog rules foo(Y) isn't a truth value for any Y
the above is obviously just an attempt to deive with a distraction.
That was a quote from the most definitive source
for the Prolog Language.
Prolog only has Facts and Rules thus the only
derivation is to a truth value.
On 12/12/2025 2:50 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.17:
On 12/11/2025 2:42 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 16.10:As I say non-terminating, thus never resolves to a truth value.
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:No that it flatly incorrect. The second question is this:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>> are different. The former assigns a value to G, the latter >>>>>>>>>>>>>> does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable >>>>>>>>>>>> means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = >>>>>>>>>> not(provable(
F, G))" can be proven for some F and some G. The answer is >>>>>>>>>> that it can
for every F and for (at least) one G, which is not(provable(G)). >>>>>>>>>>
The second query can be regarded as a question whether "G = >>>>>>>>>> not(provable
(F, G))" can be proven for some F and some G that do not
contain cycles.
The answer is that in the proof system of Prolog it cannot be. >>>>>>>>>
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G))
to a truth value true. When doing so it evaluated each side of =
to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated
subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that
wherever an occurs check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
Thank you for the confirmation of my explanation of your error.
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
As according to Prolog rules foo(Y) isn't a truth value for any Y
the above is obviously just an attempt to deive with a distraction.
That was a quote from the most definitive source
for the Prolog Language.
Prolog only has Facts and Rules thus the only
derivation is to a truth value.
olcott kirjoitti 12.12.2025 klo 16.19:
On 12/12/2025 2:50 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.17:
On 12/11/2025 2:42 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 16.10:As I say non-terminating, thus never resolves to a truth value.
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:No that it flatly incorrect. The second question is this:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>> are different. The former assigns a value to G, the >>>>>>>>>>>>>>> latter does not.
For sufficiently informal definitions of "value".
And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable >>>>>>>>>>>>> means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = >>>>>>>>>>> not(provable(
F, G))" can be proven for some F and some G. The answer is >>>>>>>>>>> that it can
for every F and for (at least) one G, which is not(provable(G)). >>>>>>>>>>>
The second query can be regarded as a question whether "G = >>>>>>>>>>> not(provable
(F, G))" can be proven for some F and some G that do not >>>>>>>>>>> contain cycles.
The answer is that in the proof system of Prolog it cannot be. >>>>>>>>>>
Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G)) >>>>>>> to a truth value true. When doing so it evaluated each side of = >>>>>>> to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an uninstantiated >>>>>> subterm of itself, which means that programs which cause this to
happen will not be portable. A portable program should ensure that >>>>>> wherever an occurs check might be applicable the built-in predicate >>>>>> unify_with_occurs_check/2 is used explicitly instead of the normal >>>>>> unification operation of the Prolog implementation. As its name
suggests, this predicate acts like =/2 except that it fails if an
occurs check detects an illegal attempt to instantiate a variable. >>>>>> END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
Thank you for the confirmation of my explanation of your error.
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
As according to Prolog rules foo(Y) isn't a truth value for any Y
the above is obviously just an attempt to deive with a distraction.
That was a quote from the most definitive source
for the Prolog Language.
As I already said, that source agrees with what I said above.
Prolog only has Facts and Rules thus the only
derivation is to a truth value.
Not true. Prolog also has term expressions that can be used in facts
and rules. In particular, in the goal G = not(provable(F, G)) the
symbol G is a term expression and provable(F, G) is another term
expression. A goal is evaluated to a truth value but if that truth
value is true the values of variables (if there are any) are also
evalueted to values that are not truth values. In the example
?- G = not(provable(F, G)).
the answer
G = not(provable(F, G)).
mans that the Prolog implementation evaluated the query to true and
the variable G to the expression not(provable(F, G)). The quoted
text says that another Prolog implementation may interprethe the
same query differently.
The quoted text does not stay unify_with_occurs_check/2 would reject
anything as "semntically unsound". First of all, it nas no consequences unless it is used. Secondly, if the result of unification would be
that at a cycle be created then it simpy evaluates to false just
like unify_with_occurs_check(1, 2) evaluates to false.
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
On 12/13/2025 4:19 AM, Mikko wrote:
olcott kirjoitti 12.12.2025 klo 16.19:
On 12/12/2025 2:50 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.17:
On 12/11/2025 2:42 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 16.10:As I say non-terminating, thus never resolves to a truth value.
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:No that it flatly incorrect. The second question is this: >>>>>>>>>>> Is "G = not(provable(F, G))." semantically sound?
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>>> are different. The former assigns a value to G, the >>>>>>>>>>>>>>>> latter does not.
For sufficiently informal definitions of "value". >>>>>>>>>>>>>>> And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog variable >>>>>>>>>>>>>> means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = >>>>>>>>>>>> not(provable(
F, G))" can be proven for some F and some G. The answer is >>>>>>>>>>>> that it can
for every F and for (at least) one G, which is
not(provable(G)).
The second query can be regarded as a question whether "G = >>>>>>>>>>>> not(provable
(F, G))" can be proven for some F and some G that do not >>>>>>>>>>>> contain cycles.
The answer is that in the proof system of Prolog it cannot be. >>>>>>>>>>>
Where is the definition of Prolog semantics is that said?
Any expression of Prolog that cannot be evaluated to
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G)) >>>>>>>> to a truth value true. When doing so it evaluated each side of = >>>>>>>> to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come
to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably.
Since it would only affect very few programs, most implementors
have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an
uninstantiated subterm of itself, which means that programs which >>>>>>> cause this to
happen will not be portable. A portable program should ensure
that wherever an occurs check might be applicable the built-in
predicate
unify_with_occurs_check/2 is used explicitly instead of the normal >>>>>>> unification operation of the Prolog implementation. As its name >>>>>>> suggests, this predicate acts like =/2 except that it fails if an >>>>>>> occurs check detects an illegal attempt to instantiate a variable. >>>>>>> END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
Thank you for the confirmation of my explanation of your error.
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
As according to Prolog rules foo(Y) isn't a truth value for any Y
the above is obviously just an attempt to deive with a distraction.
That was a quote from the most definitive source
for the Prolog Language.
As I already said, that source agrees with what I said above.
Prolog only has Facts and Rules thus the only
derivation is to a truth value.
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails. https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2
But Prolog also can't handle full first order logic, so isn't a valid
model of such a logic system.
Of course, it seems it handles a superset of the logic you can handle,
so you think it is great, but that just shows your own problem.
On 13/12/2025 16:43, olcott wrote:
On 12/13/2025 4:19 AM, Mikko wrote:
olcott kirjoitti 12.12.2025 klo 16.19:
On 12/12/2025 2:50 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.17:
On 12/11/2025 2:42 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 16.10:As I say non-terminating, thus never resolves to a truth value.
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:Any expression of Prolog that cannot be evaluated to
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:No that it flatly incorrect. The second question is this: >>>>>>>>>>>> Is "G = not(provable(F, G))." semantically sound?
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32: >>>>>>>>>>>>>>>> On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>>>> are different. The former assigns a value to G, the >>>>>>>>>>>>>>>>> latter does not.
For sufficiently informal definitions of "value". >>>>>>>>>>>>>>>> And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog >>>>>>>>>>>>>>> variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>> false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = >>>>>>>>>>>>> not(provable(
F, G))" can be proven for some F and some G. The answer is >>>>>>>>>>>>> that it can
for every F and for (at least) one G, which is
not(provable(G)).
The second query can be regarded as a question whether "G = >>>>>>>>>>>>> not(provable
(F, G))" can be proven for some F and some G that do not >>>>>>>>>>>>> contain cycles.
The answer is that in the proof system of Prolog it cannot be. >>>>>>>>>>>>
Where is the definition of Prolog semantics is that said? >>>>>>>>>>
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G)) >>>>>>>>> to a truth value true. When doing so it evaluated each side of = >>>>>>>>> to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems
will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something
like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come >>>>>>>> to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably. >>>>>>>> Since it would only affect very few programs, most implementors >>>>>>>> have simply left it out 1.
1 The Prolog standard states that the result is undefined if
a Prolog system attempts to match a term against an
uninstantiated subterm of itself, which means that programs
which cause this to
happen will not be portable. A portable program should ensure >>>>>>>> that wherever an occurs check might be applicable the built-in >>>>>>>> predicate
unify_with_occurs_check/2 is used explicitly instead of the normal >>>>>>>> unification operation of the Prolog implementation. As its name >>>>>>>> suggests, this predicate acts like =/2 except that it fails if an >>>>>>>> occurs check detects an illegal attempt to instantiate a variable. >>>>>>>> END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
Springer-Verlag.
Thank you for the confirmation of my explanation of your error.
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
As according to Prolog rules foo(Y) isn't a truth value for any Y
the above is obviously just an attempt to deive with a distraction.
That was a quote from the most definitive source
for the Prolog Language.
As I already said, that source agrees with what I said above.
Prolog only has Facts and Rules thus the only
derivation is to a truth value.
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-understanding.
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
Also every other decision problem instance
with pathological self reference is isomorphic
to the Liar Paradox.
On 12/14/25 6:14 PM, olcott wrote:
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?
predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-understanding. >>>
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
Also every other decision problem instance
with pathological self reference is isomorphic
to the Liar Paradox.
But no one (except maybe you) didn't understand that the liar paradox
wasn't a truth bearer.
On 12/14/2025 6:13 PM, Richard Damon wrote:
On 12/14/25 6:14 PM, olcott wrote:
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?
predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-
understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
Also every other decision problem instance
with pathological self reference is isomorphic
to the Liar Paradox.
But no one (except maybe you) didn't understand that the liar paradox
wasn't a truth bearer.
It sure would seem that way wouldn't it?
It turns out that the Liar Paradox as not
a truth bearer has never been accepted.
It remains one of the great unresolved
paradoxes of the world.
On 12/14/25 7:46 PM, olcott wrote:
On 12/14/2025 6:13 PM, Richard Damon wrote:
On 12/14/25 6:14 PM, olcott wrote:
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?
predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-
understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
Also every other decision problem instance
with pathological self reference is isomorphic
to the Liar Paradox.
But no one (except maybe you) didn't understand that the liar paradox
wasn't a truth bearer.
It sure would seem that way wouldn't it?
Yep
It turns out that the Liar Paradox as not
a truth bearer has never been accepted.
Sure it has. It is you who just don't understand what people are
talking about.
It remains one of the great unresolved
paradoxes of the world.
Nope. Care to docuement that claim?
It seems you are just that stupid that you can't understand what you--
read, but then, that is what happens when you don't understand that you
need to use the right defintions of the words, and can't just make up
what you think they mean.
On 12/14/2025 6:53 PM, Richard Damon wrote:
On 12/14/25 7:46 PM, olcott wrote:
On 12/14/2025 6:13 PM, Richard Damon wrote:
On 12/14/25 6:14 PM, olcott wrote:
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?
predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-
understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
Also every other decision problem instance
with pathological self reference is isomorphic
to the Liar Paradox.
But no one (except maybe you) didn't understand that the liar
paradox wasn't a truth bearer.
It sure would seem that way wouldn't it?
Yep
It turns out that the Liar Paradox as not
a truth bearer has never been accepted.
Sure it has. It is you who just don't understand what people are
talking about.
It remains one of the great unresolved
paradoxes of the world.
Nope. Care to docuement that claim?
I know exactly how ridiculous it sounds.
None-the-less that the Liar Paradox has
no accepted resolutions remains a verified fact.
This guy is one of the greatest experts in
the field of Truthmaker Maximalism
I do not mean to commit myself to the claim that
denying that the Liar expresses a proposition is the
best solution to the Liar paradox, nor do I want
to commit Truthmaker Maximalism to that claim.
Published in Analysis 2006
Truthmaker Maximalism defended
GONZALO RODRIGUEZ-PEREYRA
https://philarchive.org/archive/RODTMD
I have owned LiarParadox.org for many years
as the repository for my word. It used
to be a WordPress size before it was hacked.
On 12/14/25 8:08 PM, olcott wrote:
On 12/14/2025 6:53 PM, Richard Damon wrote:
On 12/14/25 7:46 PM, olcott wrote:
On 12/14/2025 6:13 PM, Richard Damon wrote:
On 12/14/25 6:14 PM, olcott wrote:
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?
predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-
understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
Also every other decision problem instance
with pathological self reference is isomorphic
to the Liar Paradox.
But no one (except maybe you) didn't understand that the liar
paradox wasn't a truth bearer.
It sure would seem that way wouldn't it?
Yep
It turns out that the Liar Paradox as not
a truth bearer has never been accepted.
Sure it has. It is you who just don't understand what people are
talking about.
It remains one of the great unresolved
paradoxes of the world.
Nope. Care to docuement that claim?
I know exactly how ridiculous it sounds.
None-the-less that the Liar Paradox has
no accepted resolutions remains a verified fact.
Can you show where someone didn't consider it a non-truth-bearing
statement?
This guy is one of the greatest experts in
the field of Truthmaker Maximalism
I do not mean to commit myself to the claim that
denying that the Liar expresses a proposition is the
best solution to the Liar paradox, nor do I want
to commit Truthmaker Maximalism to that claim.
So, you don't understand the difference between it being a proposition
or not, and having a truth value?
Just shows your stupidity.
--Published in Analysis 2006
Truthmaker Maximalism defended
GONZALO RODRIGUEZ-PEREYRA
https://philarchive.org/archive/RODTMD
I have owned LiarParadox.org for many years
as the repository for my word. It used
to be a WordPress size before it was hacked.
So, you couldn't fix the hacked site?
On 12/14/25 8:08 PM, olcott wrote:
On 12/14/2025 6:53 PM, Richard Damon wrote:
On 12/14/25 7:46 PM, olcott wrote:
On 12/14/2025 6:13 PM, Richard Damon wrote:
On 12/14/25 6:14 PM, olcott wrote:
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?
predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-
understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
Also every other decision problem instance
with pathological self reference is isomorphic
to the Liar Paradox.
But no one (except maybe you) didn't understand that the liar
paradox wasn't a truth bearer.
It sure would seem that way wouldn't it?
Yep
It turns out that the Liar Paradox as not
a truth bearer has never been accepted.
Sure it has. It is you who just don't understand what people are
talking about.
It remains one of the great unresolved
paradoxes of the world.
Nope. Care to docuement that claim?
I know exactly how ridiculous it sounds.
None-the-less that the Liar Paradox has
no accepted resolutions remains a verified fact.
Can you show where someone didn't consider it a non-truth-bearing
statement?
On 12/14/2025 7:46 PM, Richard Damon wrote:
On 12/14/25 8:08 PM, olcott wrote:
On 12/14/2025 6:53 PM, Richard Damon wrote:
On 12/14/25 7:46 PM, olcott wrote:
On 12/14/2025 6:13 PM, Richard Damon wrote:
On 12/14/25 6:14 PM, olcott wrote:
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?
predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-
understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
Also every other decision problem instance
with pathological self reference is isomorphic
to the Liar Paradox.
But no one (except maybe you) didn't understand that the liar
paradox wasn't a truth bearer.
It sure would seem that way wouldn't it?
Yep
It turns out that the Liar Paradox as not
a truth bearer has never been accepted.
Sure it has. It is you who just don't understand what people are
talking about.
It remains one of the great unresolved
paradoxes of the world.
Nope. Care to docuement that claim?
I know exactly how ridiculous it sounds.
None-the-less that the Liar Paradox has
no accepted resolutions remains a verified fact.
Can you show where someone didn't consider it a non-truth-bearing
statement?
There are all kinds of screwy views including
that it is both true and false. There are no
accepted final resolutions.
On 12/14/2025 7:46 PM, Richard Damon wrote:
On 12/14/25 8:08 PM, olcott wrote:
On 12/14/2025 6:53 PM, Richard Damon wrote:
On 12/14/25 7:46 PM, olcott wrote:
On 12/14/2025 6:13 PM, Richard Damon wrote:
On 12/14/25 6:14 PM, olcott wrote:
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?
predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-
understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
Also every other decision problem instance
with pathological self reference is isomorphic
to the Liar Paradox.
But no one (except maybe you) didn't understand that the liar
paradox wasn't a truth bearer.
It sure would seem that way wouldn't it?
Yep
It turns out that the Liar Paradox as not
a truth bearer has never been accepted.
Sure it has. It is you who just don't understand what people are
talking about.
It remains one of the great unresolved
paradoxes of the world.
Nope. Care to docuement that claim?
I know exactly how ridiculous it sounds.
None-the-less that the Liar Paradox has
no accepted resolutions remains a verified fact.
Can you show where someone didn't consider it a non-truth-bearing
statement?
There isn't an accepted final resolution to the Liar Paradox—it remains one of the most debated open problems in logic and philosophy!
The Liar Paradox (sentences like "This sentence is false") has generated numerous proposed solutions, but none has achieved consensus. Here are
the main approaches:
1. Tarski's Hierarchy of Languages
Truth predicates apply only to sentences in lower-level languages. The
liar sentence is blocked because it tries to apply a truth predicate to itself within the same language level. This "solves" it but many find it restrictive for natural language.
2. Paraconsistent Logic
Accept that some contradictions can exist without everything becoming provable. The liar sentence can be both true and false without the
logical system exploding.
3. Dialetheism (Graham Priest)
Accept that the liar sentence is actually both true and false—a "true contradiction" or dialetheia. Challenges the law of non-contradiction.
4. Semantic Approaches
Various theories argue the liar sentence is meaningless, lacks a truth value, or is semantically defective in some way.
5. Contextualism
The truth value shifts depending on context or level of evaluation.
6. Revision Theories
Truth values can be revised over time through iterative processes.
Each approach has its defenders and critics, and philosophers continue
to debate which (if any) is correct. The paradox remains philosophically live—it's not "solved" in the way mathematical problems get solved with accepted proofs.
On 12/14/25 9:09 PM, olcott wrote:
On 12/14/2025 7:46 PM, Richard Damon wrote:
On 12/14/25 8:08 PM, olcott wrote:
On 12/14/2025 6:53 PM, Richard Damon wrote:
On 12/14/25 7:46 PM, olcott wrote:
On 12/14/2025 6:13 PM, Richard Damon wrote:
On 12/14/25 6:14 PM, olcott wrote:
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?
predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-
understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
Also every other decision problem instance
with pathological self reference is isomorphic
to the Liar Paradox.
But no one (except maybe you) didn't understand that the liar
paradox wasn't a truth bearer.
It sure would seem that way wouldn't it?
Yep
It turns out that the Liar Paradox as not
a truth bearer has never been accepted.
Sure it has. It is you who just don't understand what people are
talking about.
It remains one of the great unresolved
paradoxes of the world.
Nope. Care to docuement that claim?
I know exactly how ridiculous it sounds.
None-the-less that the Liar Paradox has
no accepted resolutions remains a verified fact.
Can you show where someone didn't consider it a non-truth-bearing
statement?
There isn't an accepted final resolution to the Liar Paradox—it
remains one of the most debated open problems in logic and philosophy!
Nope, it is well resolved in formal logic, it just doesn't have a truth value.
The Liar Paradox (sentences like "This sentence is false") has
generated numerous proposed solutions, but none has achieved
consensus. Here are the main approaches:
1. Tarski's Hierarchy of Languages
Truth predicates apply only to sentences in lower-level languages. The
liar sentence is blocked because it tries to apply a truth predicate
to itself within the same language level. This "solves" it but many
find it restrictive for natural language.
And what is wrong with that rule? Note, this rule also resolves to there
is no truth predicate that can be defined in its own language.
And none of the following seem to be defined in normal FORMAL LOGIC
systems.
2. Paraconsistent Logic
Accept that some contradictions can exist without everything becoming
provable. The liar sentence can be both true and false without the
logical system exploding.
3. Dialetheism (Graham Priest)
Accept that the liar sentence is actually both true and false—a "true
contradiction" or dialetheia. Challenges the law of non-contradiction.
4. Semantic Approaches
Various theories argue the liar sentence is meaningless, lacks a truth
value, or is semantically defective in some way.
5. Contextualism
The truth value shifts depending on context or level of evaluation.
6. Revision Theories
Truth values can be revised over time through iterative processes.
Each approach has its defenders and critics, and philosophers continue
to debate which (if any) is correct. The paradox remains
philosophically live—it's not "solved" in the way mathematical
problems get solved with accepted proofs.
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
On 12/13/2025 4:19 AM, Mikko wrote:
olcott kirjoitti 12.12.2025 klo 16.19:
On 12/12/2025 2:50 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.17:That was a quote from the most definitive source
On 12/11/2025 2:42 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 16.10:As I say non-terminating, thus never resolves to a truth value.
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:Any expression of Prolog that cannot be evaluated to
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32: >>>>>>>>>>>>>>>>> On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>>>>> are different. The former assigns a value to G, the >>>>>>>>>>>>>>>>>> latter does not.
For sufficiently informal definitions of "value". >>>>>>>>>>>>>>>>> And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog >>>>>>>>>>>>>>>> variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>> false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = >>>>>>>>>>>>>> not(provable(
F, G))" can be proven for some F and some G. The answer is >>>>>>>>>>>>>> that it can
for every F and for (at least) one G, which is
not(provable(G)).
The second query can be regarded as a question whether "G >>>>>>>>>>>>>> = not(provable
(F, G))" can be proven for some F and some G that do not >>>>>>>>>>>>>> contain cycles.
The answer is that in the proof system of Prolog it cannot >>>>>>>>>>>>>> be.
No that it flatly incorrect. The second question is this: >>>>>>>>>>>>> Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said? >>>>>>>>>>>
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G)) >>>>>>>>>> to a truth value true. When doing so it evaluated each side of = >>>>>>>>>> to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems >>>>>>>>> will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something >>>>>>>>> like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come >>>>>>>>> to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably. >>>>>>>>> Since it would only affect very few programs, most implementors >>>>>>>>> have simply left it out 1.
1 The Prolog standard states that the result is undefined if >>>>>>>>> a Prolog system attempts to match a term against an
uninstantiated subterm of itself, which means that programs >>>>>>>>> which cause this to
happen will not be portable. A portable program should ensure >>>>>>>>> that wherever an occurs check might be applicable the built-in >>>>>>>>> predicate
unify_with_occurs_check/2 is used explicitly instead of the normal >>>>>>>>> unification operation of the Prolog implementation. As its name >>>>>>>>> suggests, this predicate acts like =/2 except that it fails if an >>>>>>>>> occurs check detects an illegal attempt to instantiate a variable. >>>>>>>>> END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog >>>>>>>>> Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg: >>>>>>>>> Springer-Verlag.
Thank you for the confirmation of my explanation of your error. >>>>>>>
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
As according to Prolog rules foo(Y) isn't a truth value for any Y
the above is obviously just an attempt to deive with a distraction. >>>>>
for the Prolog Language.
As I already said, that source agrees with what I said above.
Prolog only has Facts and Rules thus the only
derivation is to a truth value.
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
On 12/14/2025 8:27 PM, Richard Damon wrote:
On 12/14/25 9:09 PM, olcott wrote:
On 12/14/2025 7:46 PM, Richard Damon wrote:
On 12/14/25 8:08 PM, olcott wrote:
On 12/14/2025 6:53 PM, Richard Damon wrote:
On 12/14/25 7:46 PM, olcott wrote:
On 12/14/2025 6:13 PM, Richard Damon wrote:
On 12/14/25 6:14 PM, olcott wrote:
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?
predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non- >>>>>>>>>> understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
Also every other decision problem instance
with pathological self reference is isomorphic
to the Liar Paradox.
But no one (except maybe you) didn't understand that the liar >>>>>>>> paradox wasn't a truth bearer.
It sure would seem that way wouldn't it?
Yep
It turns out that the Liar Paradox as not
a truth bearer has never been accepted.
Sure it has. It is you who just don't understand what people are >>>>>> talking about.
It remains one of the great unresolved
paradoxes of the world.
Nope. Care to docuement that claim?
I know exactly how ridiculous it sounds.
None-the-less that the Liar Paradox has
no accepted resolutions remains a verified fact.
Can you show where someone didn't consider it a non-truth-bearing
statement?
There isn't an accepted final resolution to the Liar Paradox—it
remains one of the most debated open problems in logic and philosophy!
Nope, it is well resolved in formal logic, it just doesn't have a
truth value.
The Liar Paradox (sentences like "This sentence is false") has
generated numerous proposed solutions, but none has achieved
consensus. Here are the main approaches:
1. Tarski's Hierarchy of Languages
Truth predicates apply only to sentences in lower-level languages.
The liar sentence is blocked because it tries to apply a truth
predicate to itself within the same language level. This "solves" it
but many find it restrictive for natural language.
And what is wrong with that rule? Note, this rule also resolves to
there is no truth predicate that can be defined in its own language.
And none of the following seem to be defined in normal FORMAL LOGIC
systems.
None of them (above or below) has ever been
accepted as the final resolution.
2. Paraconsistent Logic
Accept that some contradictions can exist without everything becoming
provable. The liar sentence can be both true and false without the
logical system exploding.
3. Dialetheism (Graham Priest)
Accept that the liar sentence is actually both true and false—a "true >>> contradiction" or dialetheia. Challenges the law of non-contradiction.
4. Semantic Approaches
Various theories argue the liar sentence is meaningless, lacks a
truth value, or is semantically defective in some way.
5. Contextualism
The truth value shifts depending on context or level of evaluation.
6. Revision Theories
Truth values can be revised over time through iterative processes.
Each approach has its defenders and critics, and philosophers
continue to debate which (if any) is correct. The paradox remains
philosophically live—it's not "solved" in the way mathematical
problems get solved with accepted proofs.
On 15/12/2025 01:14, olcott wrote:
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
On 12/13/2025 4:19 AM, Mikko wrote:
olcott kirjoitti 12.12.2025 klo 16.19:
On 12/12/2025 2:50 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.17:That was a quote from the most definitive source
On 12/11/2025 2:42 AM, Mikko wrote:As according to Prolog rules foo(Y) isn't a truth value for any Y >>>>>>> the above is obviously just an attempt to deive with a distraction. >>>>>>
olcott kirjoitti 10.12.2025 klo 16.10:
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:Any expression of Prolog that cannot be evaluated to
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32: >>>>>>>>>>>>>>>>>> On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>>>>>> are different. The former assigns a value to G, the >>>>>>>>>>>>>>>>>>> latter does not.
For sufficiently informal definitions of "value". >>>>>>>>>>>>>>>>>> And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog >>>>>>>>>>>>>>>>> variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>>> false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G >>>>>>>>>>>>>>> = not(provable(
F, G))" can be proven for some F and some G. The answer >>>>>>>>>>>>>>> is that it can
for every F and for (at least) one G, which is
not(provable(G)).
The second query can be regarded as a question whether "G >>>>>>>>>>>>>>> = not(provable
(F, G))" can be proven for some F and some G that do not >>>>>>>>>>>>>>> contain cycles.
The answer is that in the proof system of Prolog it >>>>>>>>>>>>>>> cannot be.
No that it flatly incorrect. The second question is this: >>>>>>>>>>>>>> Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said? >>>>>>>>>>>>
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies >>>>>>>>>>>> that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, >>>>>>>>>>> G))
to a truth value true. When doing so it evaluated each side of = >>>>>>>>>>> to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs >>>>>>>>>> from the unification used in Resolution. Most Prolog systems >>>>>>>>>> will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result, >>>>>>>>>> Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure. >>>>>>>>>>
Note that, whereas they may allow you to construct something >>>>>>>>>> like this, most Prolog systems will not be able to write it >>>>>>>>>> out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come >>>>>>>>>> to exist. Thus Prolog systems that allow a term to match an >>>>>>>>>> uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we >>>>>>>>>> would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check, >>>>>>>>>> an occurs check, would be straightforward to implement, but >>>>>>>>>> would slow down the execution of Prolog programs considerably. >>>>>>>>>> Since it would only affect very few programs, most implementors >>>>>>>>>> have simply left it out 1.
1 The Prolog standard states that the result is undefined if >>>>>>>>>> a Prolog system attempts to match a term against an
uninstantiated subterm of itself, which means that programs >>>>>>>>>> which cause this to
happen will not be portable. A portable program should ensure >>>>>>>>>> that wherever an occurs check might be applicable the built-in >>>>>>>>>> predicate
unify_with_occurs_check/2 is used explicitly instead of the >>>>>>>>>> normal
unification operation of the Prolog implementation. As its >>>>>>>>>> name suggests, this predicate acts like =/2 except that it >>>>>>>>>> fails if an
occurs check detects an illegal attempt to instantiate a
variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog >>>>>>>>>> Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg: >>>>>>>>>> Springer-Verlag.
Thank you for the confirmation of my explanation of your error. >>>>>>>>
Y will stand for foo(Y), which is foo(foo(Y)) (because of >>>>>>>> >> what Y stands for), which is foo(foo(foo(Y))), and so on. >>>>>>>> As I say non-terminating, thus never resolves to a truth value. >>>>>>>
for the Prolog Language.
As I already said, that source agrees with what I said above.
Prolog only has Facts and Rules thus the only
derivation is to a truth value.
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?
predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
In other words you admit you were lying about me.
On 12/15/2025 3:04 AM, Mikko wrote:
On 15/12/2025 01:14, olcott wrote:
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
On 12/13/2025 4:19 AM, Mikko wrote:
olcott kirjoitti 12.12.2025 klo 16.19:
On 12/12/2025 2:50 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.17:That was a quote from the most definitive source
On 12/11/2025 2:42 AM, Mikko wrote:As according to Prolog rules foo(Y) isn't a truth value for any Y >>>>>>>> the above is obviously just an attempt to deive with a distraction. >>>>>>>
olcott kirjoitti 10.12.2025 klo 16.10:
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:Any expression of Prolog that cannot be evaluated to >>>>>>>>>>>>> a truth value because it specifies non-terminating
On 12/5/2025 3:38 AM, Mikko wrote:Where is the definition of Prolog semantics is that said? >>>>>>>>>>>>>
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32: >>>>>>>>>>>>>>>>>>> On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>>>>>>> are different. The former assigns a value to G, the >>>>>>>>>>>>>>>>>>>> latter does not.
For sufficiently informal definitions of "value". >>>>>>>>>>>>>>>>>>> And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog >>>>>>>>>>>>>>>>>> variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>>>> false.
I would say that the above Prolog is the 100% >>>>>>>>>>>>>>>>> complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G >>>>>>>>>>>>>>>> = not(provable(
F, G))" can be proven for some F and some G. The answer >>>>>>>>>>>>>>>> is that it can
for every F and for (at least) one G, which is >>>>>>>>>>>>>>>> not(provable(G)).
The second query can be regarded as a question whether >>>>>>>>>>>>>>>> "G = not(provable
(F, G))" can be proven for some F and some G that do not >>>>>>>>>>>>>>>> contain cycles.
The answer is that in the proof system of Prolog it >>>>>>>>>>>>>>>> cannot be.
No that it flatly incorrect. The second question is this: >>>>>>>>>>>>>>> Is "G = not(provable(F, G))." semantically sound? >>>>>>>>>>>>>>
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies >>>>>>>>>>>>> that cannot be evaluated to a truth value because it >>>>>>>>>>>>> specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G =
not(provablel(F, G))
to a truth value true. When doing so it evaluated each side >>>>>>>>>>>> of =
to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs >>>>>>>>>>> from the unification used in Resolution. Most Prolog systems >>>>>>>>>>> will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y) >>>>>>>>>>> is matched against Y, which appears within it. As a result, >>>>>>>>>>> Y will stand for foo(Y), which is foo(foo(Y)) (because of >>>>>>>>>>> what Y stands for), which is foo(foo(foo(Y))), and so on. >>>>>>>>>>> So Y ends up standing for some kind of infinite structure. >>>>>>>>>>>
Note that, whereas they may allow you to construct something >>>>>>>>>>> like this, most Prolog systems will not be able to write it >>>>>>>>>>> out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come >>>>>>>>>>> to exist. Thus Prolog systems that allow a term to match an >>>>>>>>>>> uninstantiated subterm of itself do not act correctly as >>>>>>>>>>> Resolution theorem provers. In order to make them do so, we >>>>>>>>>>> would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check, >>>>>>>>>>> an occurs check, would be straightforward to implement, but >>>>>>>>>>> would slow down the execution of Prolog programs considerably. >>>>>>>>>>> Since it would only affect very few programs, most implementors >>>>>>>>>>> have simply left it out 1.
1 The Prolog standard states that the result is undefined if >>>>>>>>>>> a Prolog system attempts to match a term against an
uninstantiated subterm of itself, which means that programs >>>>>>>>>>> which cause this to
happen will not be portable. A portable program should ensure >>>>>>>>>>> that wherever an occurs check might be applicable the built- >>>>>>>>>>> in predicate
unify_with_occurs_check/2 is used explicitly instead of the >>>>>>>>>>> normal
unification operation of the Prolog implementation. As its >>>>>>>>>>> name suggests, this predicate acts like =/2 except that it >>>>>>>>>>> fails if an
occurs check detects an illegal attempt to instantiate a >>>>>>>>>>> variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog >>>>>>>>>>> Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg: >>>>>>>>>>> Springer-Verlag.
Thank you for the confirmation of my explanation of your error. >>>>>>>>>
Y will stand for foo(Y), which is foo(foo(Y)) (because of >>>>>>>>> >> what Y stands for), which is foo(foo(foo(Y))), and so on. >>>>>>>>> As I say non-terminating, thus never resolves to a truth value. >>>>>>>>
for the Prolog Language.
As I already said, that source agrees with what I said above.
Prolog only has Facts and Rules thus the only
derivation is to a truth value.
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?
predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-
understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
In other words you admit you were lying about me.
I have no idea what you are referring to.
On 12/14/2025 4:05 AM, Mikko wrote:
On 13/12/2025 16:43, olcott wrote:
On 12/13/2025 4:19 AM, Mikko wrote:
olcott kirjoitti 12.12.2025 klo 16.19:
On 12/12/2025 2:50 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.17:That was a quote from the most definitive source
On 12/11/2025 2:42 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 16.10:As I say non-terminating, thus never resolves to a truth value.
On 12/10/2025 4:04 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.09:
On 12/8/2025 3:13 AM, Mikko wrote:
olcott kirjoitti 5.12.2025 klo 19.43:Any expression of Prolog that cannot be evaluated to
On 12/5/2025 3:38 AM, Mikko wrote:
olcott kirjoitti 4.12.2025 klo 16.06:
On 12/4/2025 2:58 AM, Mikko wrote:
Tristan Wibberley kirjoitti 4.12.2025 klo 4.32: >>>>>>>>>>>>>>>>> On 30/11/2025 09:58, Mikko wrote:
Note that the meanings of
?- G = not(provable(F, G)).
and
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>>>>> are different. The former assigns a value to G, the >>>>>>>>>>>>>>>>>> latter does not.
For sufficiently informal definitions of "value". >>>>>>>>>>>>>>>>> And for sufficiently wrong ones too!
It is sufficiently clear what "value" of a Prolog >>>>>>>>>>>>>>>> variable means.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>> false.
I would say that the above Prolog is the 100%
complete formal specification of:
"This sentence cannot be proven in F"
The first query can be regarded as a question whether "G = >>>>>>>>>>>>>> not(provable(
F, G))" can be proven for some F and some G. The answer is >>>>>>>>>>>>>> that it can
for every F and for (at least) one G, which is
not(provable(G)).
The second query can be regarded as a question whether "G >>>>>>>>>>>>>> = not(provable
(F, G))" can be proven for some F and some G that do not >>>>>>>>>>>>>> contain cycles.
The answer is that in the proof system of Prolog it cannot >>>>>>>>>>>>>> be.
No that it flatly incorrect. The second question is this: >>>>>>>>>>>>> Is "G = not(provable(F, G))." semantically sound?
Where is the definition of Prolog semantics is that said? >>>>>>>>>>>
a truth value because it specifies non-terminating
infinite recursion is "semantically unsound" by the
definition of those terms even if Prolog only specifies
that cannot be evaluated to a truth value because it
specifies non-terminating infinite recursion.
Your Prolog implementation has evaluated G = not(provablel(F, G)) >>>>>>>>>> to a truth value true. When doing so it evaluated each side of = >>>>>>>>>> to a value that is not a truth value.
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
Proves that
G = not(provable(F, G)).
would remain stuck in infinite recursion.
unify_with_occurs_check() examines the directed
graph of the evaluation sequence of an expression.
When it detects a cycle that indicates that an
expression would remain stuck in recursive
evaluation never to be resolved to a truth value.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs
from the unification used in Resolution. Most Prolog systems >>>>>>>>> will allow you to satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an
uninstantiated subterm of itself. In this example, foo(Y)
is matched against Y, which appears within it. As a result,
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something >>>>>>>>> like this, most Prolog systems will not be able to write it
out at the end. According to the formal definition of
Unification, this kind of “infinite term” should never come >>>>>>>>> to exist. Thus Prolog systems that allow a term to match an
uninstantiated subterm of itself do not act correctly as
Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be
instantiated to something containing itself. Such a check,
an occurs check, would be straightforward to implement, but
would slow down the execution of Prolog programs considerably. >>>>>>>>> Since it would only affect very few programs, most implementors >>>>>>>>> have simply left it out 1.
1 The Prolog standard states that the result is undefined if >>>>>>>>> a Prolog system attempts to match a term against an
uninstantiated subterm of itself, which means that programs >>>>>>>>> which cause this to
happen will not be portable. A portable program should ensure >>>>>>>>> that wherever an occurs check might be applicable the built-in >>>>>>>>> predicate
unify_with_occurs_check/2 is used explicitly instead of the normal >>>>>>>>> unification operation of the Prolog implementation. As its name >>>>>>>>> suggests, this predicate acts like =/2 except that it fails if an >>>>>>>>> occurs check detects an illegal attempt to instantiate a variable. >>>>>>>>> END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog >>>>>>>>> Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg: >>>>>>>>> Springer-Verlag.
Thank you for the confirmation of my explanation of your error. >>>>>>>
Y will stand for foo(Y), which is foo(foo(Y)) (because of
what Y stands for), which is foo(foo(foo(Y))), and so on.
As according to Prolog rules foo(Y) isn't a truth value for any Y
the above is obviously just an attempt to deive with a distraction. >>>>>
for the Prolog Language.
As I already said, that source agrees with what I said above.
Prolog only has Facts and Rules thus the only
derivation is to a truth value.
You just don't seem to understand:
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first statement creates a cyclic term, also called
a rational tree. The second executes logically sound
unification and thus fails.
https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2
Saying the same as I said does not support a claim of non-understanding.
It finally resolves the Liar Paradox
as not a truth bearer or proposition.
Also every other decision problem instance
with pathological self reference is isomorphic
to the Liar Paradox.
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,090 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 61:34:30 |
| Calls: | 13,949 |
| Calls today: | 2 |
| Files: | 187,035 |
| D/L today: |
3,081 files (873M bytes) |
| Messages: | 2,461,355 |