Path: ...!weretis.net!feeder9.news.weretis.net!news.misty.com!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Re: Self-evidently I am not my grandpa
Date: Mon, 29 Apr 2024 22:16:31 +1000
Message-ID: <v0o332$5krh$1@solani.org>
References: <v0hvp5$25uj$1@solani.org> <v0nmc7$1kvn0$1@dont-email.me>
 <v0o032$5j35$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 29 Apr 2024 12:16:34 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="185201"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.18.2
Cancel-Lock: sha1:BTKp2YtETfhjgToV10obHZL7hXU=
In-Reply-To: <v0o032$5j35$1@solani.org>
X-User-ID: eJwFwQkBwDAIA0BL/LRyUkb8S9hdemlNR2VFMmkjG72M28YAoEO0fxrr8Voxry7sQGaxaaQjU/gdwUm8H3MKFpk=
Bytes: 3773
Lines: 86

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   |
>> -----------------------------
>>
>