The only meaning a GUID has is that it is different from any other GUID.
On 11/29/2025 4:22 AM, Mikko wrote:
olcott kirjoitti 28.11.2025 klo 20.11:
On 11/28/2025 11:32 AM, Alan Mackenzie wrote:
[ Followup-To: set ]
In comp.theory olcott <polcott333@gmail.com> wrote:
[ .... ]
individual means one.
a group of individuals is not one individual
An ontology where the set of animals is an individual
animal is incoherent.
On 30/11/2025 09:37, Mikko wrote:
The only meaning a GUID has is that it is different from any other GUID.
Not strictly true, it encodes some knowledge about itself too--see GUID specification documents--some bits encode how it was generated such as
when (to whatever extent that itself means anything).
On 29/11/2025 18:00, olcott wrote:
On 11/29/2025 4:22 AM, Mikko wrote:
olcott kirjoitti 28.11.2025 klo 20.11:
On 11/28/2025 11:32 AM, Alan Mackenzie wrote:
[ Followup-To: set ]
In comp.theory olcott <polcott333@gmail.com> wrote:
[ .... ]
individual means one.
a group of individuals is not one individual
yes it is.
An ontology where the set of animals is an individual
animal is incoherent.
But one in which the set of animals is an individual set of things can
be okay. Are you sure you've been studying?
On 12/3/2025 7:57 PM, Tristan Wibberley wrote:
On 29/11/2025 18:00, olcott wrote:
On 11/29/2025 4:22 AM, Mikko wrote:
olcott kirjoitti 28.11.2025 klo 20.11:
On 11/28/2025 11:32 AM, Alan Mackenzie wrote:
[ Followup-To: set ]
In comp.theory olcott <polcott333@gmail.com> wrote:
[ .... ]
individual means one.
a group of individuals is not one individual
yes it is.
An ontology where the set of animals is an individual
animal is incoherent.
But one in which the set of animals is an individual set of things can
be okay. Are you sure you've been studying?
The seven virtues of simple type theory https://www.sciencedirect.com/science/article/pii/S157086830700081X
The purpose of Russell's Simple Type Theory was to
eliminate Russell's Paradox.
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.
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!
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!
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.
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"
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"
On 04/12/2025 08:58, 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.
I didn't read that as a use of prolog terminology. So I went and
understood why I didn't bring such to mind. It's because a "value" isn't "assigned" to A by that (see my paragraph below for the most peculiar
thing that I would concede if my life depended on it, but my life is
more likely to depend on not conceding it).
The only extent to which "?- A = B." for nonvar(B) has something like assignment of a value to A is that there's might be a program address (Dijkstra-oriented notion as one would perceive in a prolog debugger)
which differs from its predecessor by instantiation alone including in
ones consisting of just one unification. Whether that happens is
contingent because it's operational and there's no effect in the
language for that specific example. The statement doesn't have to end up
with more than one program address (being both the first and the last
address when permissible syntactic transformations are applied). I don't think it's reasonable to call that assignment of a value, not even for
lots of very ordinary statements because it's merely contingently
equivalent "in effect" to assignment in other languages and not part of
the /meaning/ of the statement specifically; nor is it part of the
meaning of =/2 generally.
On 04/12/2025 14:06, olcott wrote:
% 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"
No. I think I showed in one of my recent posts (using definition
extensions) that you need to formalise the mathematicians notion of
"proof /in/ [system]" vis-a-vis "let" and its stronger sibling
"suppose". That's a bigger job than you've done.
I need a new quotation convention for referring to things whose name has
an existing meaning in my U-language, I quoted "let" and "suppose" as if
I were using their names; I mean to use the things themselves, but they
have to be quoted in some way to distinguish the objects of mathematical language from the verbs of ordinary language without introducing such incidental new names as I would otherwise need.
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.
int main()
{
bool Sentence = !(Sentence); // Liar Paradox in C++
return 0;
}
Le 05/12/2025 à 18:00, olcott a écrit :
..
int main()
{
bool Sentence = !(Sentence); // Liar Paradox in C++
return 0;
}
You are diving into complete insanity, Olcott.
Maybe God will forgive your sins because you are insane. Who knows?
On 12/5/2025 4:17 PM, Python wrote:
Le 05/12/2025 à 18:00, olcott a écrit :
..
int main()
{
bool Sentence = !(Sentence); // Liar Paradox in C++
return 0;
}
You are diving into complete insanity, Olcott.
Maybe God will forgive your sins because you are insane. Who knows?
In other words you don't give a rat's ass for
truth at this crucial time when the lack of it
can have horrific consequences.
All that you have for rebuttal is ad homimen
person attacks. If that is accurately construed
as deceptions Revelations 21:8 may be bad for
you (unless you repent).
I care about truth because righteousness is
anchored in truth.
As far as righteousness goes I came up with
*Love one another with as much empathy as possible*
when a 2015 policy change at my church directly
caused the suicide of more than 30 young people.
Le 05/12/2025 à 23:24, olcott a écrit :
On 12/5/2025 4:17 PM, Python wrote:
Le 05/12/2025 à 18:00, olcott a écrit :
..
int main()
{
bool Sentence = !(Sentence); // Liar Paradox in C++
return 0;
}
You are diving into complete insanity, Olcott.
Maybe God will forgive your sins because you are insane. Who knows?
In other words you don't give a rat's ass for
truth at this crucial time when the lack of it
can have horrific consequences.
All that you have for rebuttal is ad homimen
person attacks. If that is accurately construed
as deceptions Revelations 21:8 may be bad for
you (unless you repent).
I care about truth because righteousness is
anchored in truth.
As far as righteousness goes I came up with
*Love one another with as much empathy as possible*
when a 2015 policy change at my church directly
caused the suicide of more than 30 young people.
There is no righteousness on your side, only hypocrisy and bigotry in disguise.
On 12/05/2025 02:45 PM, Python wrote:
Le 05/12/2025 à 23:24, olcott a écrit :
On 12/5/2025 4:17 PM, Python wrote:
Le 05/12/2025 à 18:00, olcott a écrit :
..
int main()
{
bool Sentence = !(Sentence); // Liar Paradox in C++
return 0;
}
You are diving into complete insanity, Olcott.
Maybe God will forgive your sins because you are insane. Who knows?
In other words you don't give a rat's ass for
truth at this crucial time when the lack of it
can have horrific consequences.
All that you have for rebuttal is ad homimen
person attacks. If that is accurately construed
as deceptions Revelations 21:8 may be bad for
you (unless you repent).
I care about truth because righteousness is
anchored in truth.
As far as righteousness goes I came up with
*Love one another with as much empathy as possible*
when a 2015 policy change at my church directly
caused the suicide of more than 30 young people.
There is no righteousness on your side, only hypocrisy and bigotry in
disguise.
It's invincible ignorance of the (sadly) usual enough
the inductive impasse, yet a wider, fuller dialectic
may make for analytical bridges first to establish
continuity then infinity and all quite naturally.
For paradox-free infinitary deductive reasoning, ....
Or, a retro-finitist howler crank troll, ...,
yet, one may aver they'd rather live in a world
of reasoned rationality a natural reality.
On 12/5/2025 4:49 AM, Tristan Wibberley wrote:
No. I think I showed in one of my recent posts (using definition
extensions) that you need to formalise the mathematicians notion of
"proof /in/ [system]" vis-a-vis "let" and its stronger sibling
"suppose". That's a bigger job than you've done.
If an expression of language cannot be proven at
all because it is semantically incoherent then it
seems quite stupid to say that it cannot be proved
in a specific formal system.
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?
On 05/12/2025 17:05, olcott wrote:
On 12/5/2025 4:49 AM, Tristan Wibberley wrote:
No. I think I showed in one of my recent posts (using definition
extensions) that you need to formalise the mathematicians notion of
"proof /in/ [system]" vis-a-vis "let" and its stronger sibling
"suppose". That's a bigger job than you've done.
If an expression of language cannot be proven at
all because it is semantically incoherent then it
seems quite stupid to say that it cannot be proved
in a specific formal system.
See if you find my message in your newsreader in which I describe some definition extensions and systems related by them. There is critical
matter of the precise meaning of "prove in a system" (mathematicians)
and "derive of a system" (logicians). And the matter of whether your "F" refers to the system of which your definition of G is an axiom, to its related basic system of which your G is not, or to something else.
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 2:24 AM, Tristan Wibberley wrote:
See if you find my message in your newsreader in which I describe some
definition extensions and systems related by them. There is critical
matter of the precise meaning of "prove in a system" (mathematicians)
and "derive of a system" (logicians). And the matter of whether your "F"
refers to the system of which your definition of G is an axiom, to its
related basic system of which your G is not, or to something else.
I just made the system have a large enough scope
such that unprovable in the system means not a member
of the body of general knowledge.
On 06/12/2025 12:08, olcott wrote:
On 12/6/2025 2:24 AM, Tristan Wibberley wrote:
See if you find my message in your newsreader in which I describe some
definition extensions and systems related by them. There is critical
matter of the precise meaning of "prove in a system" (mathematicians)
and "derive of a system" (logicians). And the matter of whether your "F" >>> refers to the system of which your definition of G is an axiom, to its
related basic system of which your G is not, or to something else.
I just made the system have a large enough scope
such that unprovable in the system means not a member
of the body of general knowledge.
I think you're talking about the logicians "derivable of a system" (ie,
"is among the theorems of a formal system").
I think you should read my more detailed message about definition
extension. I'm super sleepy so I can't make myself find the message id,
maybe later.
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?
I need a new quotation convention for referring to things whose name hasIn ASCII text you can use quotes, apostrophes, and grave accents. If you
an existing meaning in my U-language,
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?
On 04/12/2025 14:06, olcott wrote:
% 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"
No. I think I showed in one of my recent posts (using definition
extensions) that you need to formalise the mathematicians notion of
"proof /in/ [system]" vis-a-vis "let" and its stronger sibling
"suppose". That's a bigger job than you've done.
I need a new quotation convention for referring to things whose name has
an existing meaning in my U-language, I quoted "let" and "suppose" as if
I were using their names; I mean to use the things themselves, but they
have to be quoted in some way to distinguish the objects of mathematical language from the verbs of ordinary language without introducing such incidental new names as I would otherwise need.
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.
On 12/5/2025 4:49 AM, Tristan Wibberley wrote:
On 04/12/2025 14:06, olcott wrote:
% 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"
No. I think I showed in one of my recent posts (using definition
extensions) that you need to formalise the mathematicians notion of
"proof /in/ [system]" vis-a-vis "let" and its stronger sibling
"suppose". That's a bigger job than you've done.
I need a new quotation convention for referring to things whose name has
an existing meaning in my U-language, I quoted "let" and "suppose" as if
I were using their names; I mean to use the things themselves, but they
have to be quoted in some way to distinguish the objects of mathematical
language from the verbs of ordinary language without introducing such
incidental new names as I would otherwise need.
Semantics tautologies that define finite strings in
terms of other finite strings to give the LHS its
semantic meaning on the basis of the RHS.
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.
Le 10/12/2025 à 15:11, olcott a écrit :
..
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.
unify_with_occurs_check(G, not(provable(F, G))). returning false does
NOT prove that
G = not(provable(F, G)) “gets stuck in infinite recursion.”
All it proves is this:
With finite Prolog terms, you cannot unify a variable with a structure
that contains that same variable — the occurs-check rejects cyclic self- reference.
So the failure of unification means only:
Prolog refuses to build an illegal self-referential term,
not that the logical statement or predicate would “infinitely recurse.”
This is the usual Olcott confusion:--
he mistakes a language-specific operational failure (Prolog term construction) for a deep theorem about provability or self-reference.
Gödel diagonalization never uses this kind of naive unification, so the Prolog failure is irrelevant to logic.
olcott kirjoitti 8.12.2025 klo 21.12:
On 12/5/2025 4:49 AM, Tristan Wibberley wrote:
On 04/12/2025 14:06, olcott wrote:
% 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"
No. I think I showed in one of my recent posts (using definition
extensions) that you need to formalise the mathematicians notion of
"proof /in/ [system]" vis-a-vis "let" and its stronger sibling
"suppose". That's a bigger job than you've done.
I need a new quotation convention for referring to things whose name has >>> an existing meaning in my U-language, I quoted "let" and "suppose" as if >>> I were using their names; I mean to use the things themselves, but they
have to be quoted in some way to distinguish the objects of mathematical >>> language from the verbs of ordinary language without introducing such
incidental new names as I would otherwise need.
Semantics tautologies that define finite strings in
terms of other finite strings to give the LHS its
semantic meaning on the basis of the RHS.
You havn't given a single example of a smenatic tautology that can be interpreted as a definition nor a single example of defintion that is
a semantic tautology. Perhaps it is possible if you define "semantic taultology" so that it needn't be anything like a tautology.
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:10 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.12:
On 12/5/2025 4:49 AM, Tristan Wibberley wrote:
On 04/12/2025 14:06, olcott wrote:
% 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"
No. I think I showed in one of my recent posts (using definition
extensions) that you need to formalise the mathematicians notion of
"proof /in/ [system]" vis-a-vis "let" and its stronger sibling
"suppose". That's a bigger job than you've done.
I need a new quotation convention for referring to things whose name
has
an existing meaning in my U-language, I quoted "let" and "suppose"
as if
I were using their names; I mean to use the things themselves, but they >>>> have to be quoted in some way to distinguish the objects of
mathematical
language from the verbs of ordinary language without introducing such
incidental new names as I would otherwise need.
Semantics tautologies that define finite strings in
terms of other finite strings to give the LHS its
semantic meaning on the basis of the RHS.
You havn't given a single example of a smenatic tautology that can be
interpreted as a definition nor a single example of defintion that is
a semantic tautology. Perhaps it is possible if you define "semantic
taultology" so that it needn't be anything like a tautology.
From my signature line:
"true on the basis of meaning expressed in language"
Here is an example: "cats" <are> "animals"
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 18.29:
On 12/10/2025 4:10 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.12:
On 12/5/2025 4:49 AM, Tristan Wibberley wrote:
On 04/12/2025 14:06, olcott wrote:
% 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"
No. I think I showed in one of my recent posts (using definition
extensions) that you need to formalise the mathematicians notion of
"proof /in/ [system]" vis-a-vis "let" and its stronger sibling
"suppose". That's a bigger job than you've done.
I need a new quotation convention for referring to things whose
name has
an existing meaning in my U-language, I quoted "let" and "suppose"
as if
I were using their names; I mean to use the things themselves, but
they
have to be quoted in some way to distinguish the objects of
mathematical
language from the verbs of ordinary language without introducing such >>>>> incidental new names as I would otherwise need.
Semantics tautologies that define finite strings in
terms of other finite strings to give the LHS its
semantic meaning on the basis of the RHS.
You havn't given a single example of a smenatic tautology that can be
interpreted as a definition nor a single example of defintion that is
a semantic tautology. Perhaps it is possible if you define "semantic
taultology" so that it needn't be anything like a tautology.
From my signature line:
"true on the basis of meaning expressed in language"
Here is an example: "cats" <are> "animals"
Yes, that is an example of your inability mentioned above.
Your example not define anything and therefore is neither an exmaple
of a semantic tautology that can be interpreted as a defintion nor an
axample of a defintion that is a semantic tautology.
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:40 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 18.29:
On 12/10/2025 4:10 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.12:
On 12/5/2025 4:49 AM, Tristan Wibberley wrote:
On 04/12/2025 14:06, olcott wrote:
% 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"
No. I think I showed in one of my recent posts (using definition
extensions) that you need to formalise the mathematicians notion of >>>>>> "proof /in/ [system]" vis-a-vis "let" and its stronger sibling
"suppose". That's a bigger job than you've done.
I need a new quotation convention for referring to things whose
name has
an existing meaning in my U-language, I quoted "let" and "suppose" >>>>>> as if
I were using their names; I mean to use the things themselves, but >>>>>> they
have to be quoted in some way to distinguish the objects of
mathematical
language from the verbs of ordinary language without introducing such >>>>>> incidental new names as I would otherwise need.
Semantics tautologies that define finite strings in
terms of other finite strings to give the LHS its
semantic meaning on the basis of the RHS.
You havn't given a single example of a smenatic tautology that can be
interpreted as a definition nor a single example of defintion that is
a semantic tautology. Perhaps it is possible if you define "semantic
taultology" so that it needn't be anything like a tautology.
From my signature line:
"true on the basis of meaning expressed in language"
Here is an example: "cats" <are> "animals"
Yes, that is an example of your inability mentioned above.
Your example not define anything and therefore is neither an exmaple
of a semantic tautology that can be interpreted as a defintion nor an
axample of a defintion that is a semantic tautology.
Kurt Gödel in his 1944 Russell's mathematical logic gave the following definition of the "theory of simple types" in a footnote:
By the theory of simple types I mean the doctrine which says that the objects of thought (or, in another interpretation, the symbolic
expressions) are divided into types, namely: individuals, properties of individuals, relations between individuals, properties of such
relations, etc. (with a similar hierarchy for extensions), and that sentences of the form: " a has the property φ ", " b bears the relation
R to c ", etc. are meaningless, if a, b, c, R, φ are not of types
fitting together.
The finite string "cats" is stipulated to have
the type_of_relation <are> to the finite string
"animals".
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.15:
On 12/11/2025 2:40 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 18.29:
On 12/10/2025 4:10 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.12:
On 12/5/2025 4:49 AM, Tristan Wibberley wrote:
On 04/12/2025 14:06, olcott wrote:
% 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"
No. I think I showed in one of my recent posts (using definition >>>>>>> extensions) that you need to formalise the mathematicians notion of >>>>>>> "proof /in/ [system]" vis-a-vis "let" and its stronger sibling
"suppose". That's a bigger job than you've done.
I need a new quotation convention for referring to things whose >>>>>>> name has
an existing meaning in my U-language, I quoted "let" and
"suppose" as if
I were using their names; I mean to use the things themselves,
but they
have to be quoted in some way to distinguish the objects of
mathematical
language from the verbs of ordinary language without introducing >>>>>>> such
incidental new names as I would otherwise need.
Semantics tautologies that define finite strings in
terms of other finite strings to give the LHS its
semantic meaning on the basis of the RHS.
You havn't given a single example of a smenatic tautology that can be >>>>> interpreted as a definition nor a single example of defintion that is >>>>> a semantic tautology. Perhaps it is possible if you define "semantic >>>>> taultology" so that it needn't be anything like a tautology.
From my signature line:
"true on the basis of meaning expressed in language"
Here is an example: "cats" <are> "animals"
Yes, that is an example of your inability mentioned above.
Your example not define anything and therefore is neither an exmaple
of a semantic tautology that can be interpreted as a defintion nor an
axample of a defintion that is a semantic tautology.
Kurt Gödel in his 1944 Russell's mathematical logic gave the following
definition of the "theory of simple types" in a footnote:
By the theory of simple types I mean the doctrine which says that the
objects of thought (or, in another interpretation, the symbolic
expressions) are divided into types, namely: individuals, properties
of individuals, relations between individuals, properties of such
relations, etc. (with a similar hierarchy for extensions), and that
sentences of the form: " a has the property φ ", " b bears the
relation R to c ", etc. are meaningless, if a, b, c, R, φ are not of
types fitting together.
The finite string "cats" is stipulated to have
the type_of_relation <are> to the finite string
"animals".
Perhaps, but any definition of "cat" must exlude some animals as
non-cats. Yor above example of semantic tautology doesn't do that.
Note that the meaning of "cat" varies from 'Felis catus L.' to 'Felidae Fischer von Waldheim 1817' and even to non-animals.
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:46 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.15:
On 12/11/2025 2:40 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 18.29:
On 12/10/2025 4:10 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.12:
On 12/5/2025 4:49 AM, Tristan Wibberley wrote:
On 04/12/2025 14:06, olcott wrote:
% 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"
No. I think I showed in one of my recent posts (using definition >>>>>>>> extensions) that you need to formalise the mathematicians notion of >>>>>>>> "proof /in/ [system]" vis-a-vis "let" and its stronger sibling >>>>>>>> "suppose". That's a bigger job than you've done.
I need a new quotation convention for referring to things whose >>>>>>>> name has
an existing meaning in my U-language, I quoted "let" and
"suppose" as if
I were using their names; I mean to use the things themselves, >>>>>>>> but they
have to be quoted in some way to distinguish the objects of
mathematical
language from the verbs of ordinary language without introducing >>>>>>>> such
incidental new names as I would otherwise need.
Semantics tautologies that define finite strings in
terms of other finite strings to give the LHS its
semantic meaning on the basis of the RHS.
You havn't given a single example of a smenatic tautology that can be >>>>>> interpreted as a definition nor a single example of defintion that is >>>>>> a semantic tautology. Perhaps it is possible if you define "semantic >>>>>> taultology" so that it needn't be anything like a tautology.
From my signature line:
"true on the basis of meaning expressed in language"
Here is an example: "cats" <are> "animals"
Yes, that is an example of your inability mentioned above.
Your example not define anything and therefore is neither an exmaple
of a semantic tautology that can be interpreted as a defintion nor an
axample of a defintion that is a semantic tautology.
Kurt Gödel in his 1944 Russell's mathematical logic gave the
following definition of the "theory of simple types" in a footnote:
By the theory of simple types I mean the doctrine which says that the
objects of thought (or, in another interpretation, the symbolic
expressions) are divided into types, namely: individuals, properties
of individuals, relations between individuals, properties of such
relations, etc. (with a similar hierarchy for extensions), and that
sentences of the form: " a has the property φ ", " b bears the
relation R to c ", etc. are meaningless, if a, b, c, R, φ are not of
types fitting together.
The finite string "cats" is stipulated to have
the type_of_relation <are> to the finite string
"animals".
Perhaps, but any definition of "cat" must exlude some animals as
non-cats. Yor above example of semantic tautology doesn't do that.
Note that the meaning of "cat" varies from 'Felis catus L.' to 'Felidae
Fischer von Waldheim 1817' and even to non-animals.
https://en.wikipedia.org/wiki/Cat
It is a member of a set specification between GUIDs
in a (taxonomy) type hierarchy.
A cat (short for caterpillar brand) can also be Earth
moving equipment. https://www.caterpillar.com/
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.
On 12/12/2025 2:46 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.15:
On 12/11/2025 2:40 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 18.29:
On 12/10/2025 4:10 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.12:
On 12/5/2025 4:49 AM, Tristan Wibberley wrote:
On 04/12/2025 14:06, olcott wrote:
% 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"
No. I think I showed in one of my recent posts (using definition >>>>>>>> extensions) that you need to formalise the mathematicians notion of >>>>>>>> "proof /in/ [system]" vis-a-vis "let" and its stronger sibling >>>>>>>> "suppose". That's a bigger job than you've done.
I need a new quotation convention for referring to things whose >>>>>>>> name has
an existing meaning in my U-language, I quoted "let" and
"suppose" as if
I were using their names; I mean to use the things themselves, >>>>>>>> but they
have to be quoted in some way to distinguish the objects of
mathematical
language from the verbs of ordinary language without introducing >>>>>>>> such
incidental new names as I would otherwise need.
Semantics tautologies that define finite strings in
terms of other finite strings to give the LHS its
semantic meaning on the basis of the RHS.
You havn't given a single example of a smenatic tautology that can be >>>>>> interpreted as a definition nor a single example of defintion that is >>>>>> a semantic tautology. Perhaps it is possible if you define "semantic >>>>>> taultology" so that it needn't be anything like a tautology.
From my signature line:
"true on the basis of meaning expressed in language"
Here is an example: "cats" <are> "animals"
Yes, that is an example of your inability mentioned above.
Your example not define anything and therefore is neither an exmaple
of a semantic tautology that can be interpreted as a defintion nor an
axample of a defintion that is a semantic tautology.
Kurt Gödel in his 1944 Russell's mathematical logic gave the
following definition of the "theory of simple types" in a footnote:
By the theory of simple types I mean the doctrine which says that the
objects of thought (or, in another interpretation, the symbolic
expressions) are divided into types, namely: individuals, properties
of individuals, relations between individuals, properties of such
relations, etc. (with a similar hierarchy for extensions), and that
sentences of the form: " a has the property φ ", " b bears the
relation R to c ", etc. are meaningless, if a, b, c, R, φ are not of
types fitting together.
The finite string "cats" is stipulated to have
the type_of_relation <are> to the finite string
"animals".
Perhaps, but any definition of "cat" must exlude some animals as
non-cats. Yor above example of semantic tautology doesn't do that.
Note that the meaning of "cat" varies from 'Felis catus L.' to 'Felidae
Fischer von Waldheim 1817' and even to non-animals.
https://en.wikipedia.org/wiki/Cat
It is a member of a set specification between GUIDs
in a (taxonomy) type hierarchy.
A cat (short for caterpillar brand) can also be Earth
moving equipment. https://www.caterpillar.com/
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.
olcott kirjoitti 12.12.2025 klo 16.16:
On 12/12/2025 2:46 AM, Mikko wrote:
olcott kirjoitti 11.12.2025 klo 16.15:
On 12/11/2025 2:40 AM, Mikko wrote:
olcott kirjoitti 10.12.2025 klo 18.29:
On 12/10/2025 4:10 AM, Mikko wrote:
olcott kirjoitti 8.12.2025 klo 21.12:
On 12/5/2025 4:49 AM, Tristan Wibberley wrote:
On 04/12/2025 14:06, olcott wrote:
% 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"
No. I think I showed in one of my recent posts (using definition >>>>>>>>> extensions) that you need to formalise the mathematicians
notion of
"proof /in/ [system]" vis-a-vis "let" and its stronger sibling >>>>>>>>> "suppose". That's a bigger job than you've done.
I need a new quotation convention for referring to things whose >>>>>>>>> name has
an existing meaning in my U-language, I quoted "let" and
"suppose" as if
I were using their names; I mean to use the things themselves, >>>>>>>>> but they
have to be quoted in some way to distinguish the objects of >>>>>>>>> mathematical
language from the verbs of ordinary language without
introducing such
incidental new names as I would otherwise need.
Semantics tautologies that define finite strings in
terms of other finite strings to give the LHS its
semantic meaning on the basis of the RHS.
You havn't given a single example of a smenatic tautology that
can be
interpreted as a definition nor a single example of defintion
that is
a semantic tautology. Perhaps it is possible if you define "semantic >>>>>>> taultology" so that it needn't be anything like a tautology.
From my signature line:
"true on the basis of meaning expressed in language"
Here is an example: "cats" <are> "animals"
Yes, that is an example of your inability mentioned above.
Your example not define anything and therefore is neither an exmaple >>>>> of a semantic tautology that can be interpreted as a defintion nor an >>>>> axample of a defintion that is a semantic tautology.
Kurt Gödel in his 1944 Russell's mathematical logic gave the
following definition of the "theory of simple types" in a footnote:
By the theory of simple types I mean the doctrine which says that
the objects of thought (or, in another interpretation, the symbolic
expressions) are divided into types, namely: individuals, properties
of individuals, relations between individuals, properties of such
relations, etc. (with a similar hierarchy for extensions), and that
sentences of the form: " a has the property φ ", " b bears the
relation R to c ", etc. are meaningless, if a, b, c, R, φ are not of >>>> types fitting together.
The finite string "cats" is stipulated to have
the type_of_relation <are> to the finite string
"animals".
Perhaps, but any definition of "cat" must exlude some animals as
non-cats. Yor above example of semantic tautology doesn't do that.
Note that the meaning of "cat" varies from 'Felis catus L.' to 'Felidae
Fischer von Waldheim 1817' and even to non-animals.
https://en.wikipedia.org/wiki/Cat
It is a member of a set specification between GUIDs
in a (taxonomy) type hierarchy.
That needs many GUIDs in or
A cat (short for caterpillar brand) can also be Earth
moving equipment. https://www.caterpillar.com/
I estimate 200 petabytes of GUIDs and connections
between them to encode the complete body of general
knowledge.
200 petabytes for body of general knowledge
stored as relations between GUIDs
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.
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,089 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 155:34:49 |
| Calls: | 13,921 |
| Calls today: | 2 |
| Files: | 187,021 |
| D/L today: |
3,962 files (1,001M bytes) |
| Messages: | 2,457,202 |