Re: Self-evidently I am not my grandpa

As expected, if I only use this Prolog:
grand_father(X,Y) :- father(X,Z), father(Z,Y).
Applying Clark Completion gets me this closed formula:
∀X∀Y(∃Z(father(X,Z) & father(Z,Y)) <=> grand_father(X,Y)).
Asking for counter models to ~ "Im my own grandpa" entailment:
% ?- problem(1, F), counter(F, M).
% M = [father(0, 0)-1, grand_father(0, 0)-1]
% Etc..
% M = [father(1, 1)-0, father(1, 0)-1, father(0, 1)-1,
%   grand_father(1, 1)-1, father(0, 0)-0, grand_father(1, 0)-0,
%   grand_father(0, 1)-0, grand_father(0, 0)-1]
% Etc..
The first solution, is from a domain with size N=1,
and it basically says a counter model is when
there is an individual 0, which is its own father.
The second solution, is from a domain with size N=2,
and it basically says a counter model is when
there are two individuals 0 and 1, which are each others father.
Etc..
Source code:
% problem(+Integer, -Formula)
problem(1, (
   ![X]:![Y]:(?[Z]:(father(X,Z) & father(Z,Y)) <=> grand_father(X,Y)) =>
   ~ ?[X]:grand_father(X,X))).
% counter(+Formula, -Model)
counter(F, M) :-
    between(1, 3, N),
    expand(F, N, G),
    quine(G, M, V),
    V = 0.
Plus expand/3 and quine/3 are found here:
https://swi-prolog.discourse.group/t/7398
Mild Shock schrieb:

 Well I forgot to say, that only first order
logic with equality, FOL=, is available.
 How would you define ancestor?
 Barb Knox schrieb:

On 27/04/2024 16:43, Mild Shock wrote:

Lets take this "truth":
>

Quine explains, “No bachelor is married,” where

the meaning of the word ‘bachelor’ is synonymous
with the meaning of the word ‘unmarried.’ However,
we can make this kind of analytic claim into a
logical truth (as defined above) by replacing
‘bachelor’ with its synonym, that is, ‘unmarried man,’
to get “No unmarried man is married,” which is an
instance of No not-X is X.
>
Then examine this "truth":
>
Lets say you build a Prolog family database and
make definitions for father, grand-father etc..
Will this Prolog family database exclude:
>
"Im my own grandpa"

>
If you want it to.  The additional rule needed is that X can not be an ancestor of X.
>
-- ---------------------------
|  BBB                b    \   Barbara at LivingHistory stop co stop uk
|  B  B   aa     rrr  b     |
|  BBB   a  a   r     bbb   |  Quidquid latine dictum sit,
|  B  B  a  a   r     b  b  |  altum videtur.
|  BBB    aa a  r     bbb   |
-----------------------------
>