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"

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

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

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

On 29/04/2024 23:25, Mild Shock wrote:
>
> Well I forgot to say, that only first order
> logic with equality, FOL=, is available.

It's not clear to me whether you are asking about FOL=, or Prolog. (You
do know that they are not the same, right?)

> How would you define ancestor?

The usual way.

This is beginning to smell a lot like homework.

Maybe you should take this to comp.lang.prolog (where they also resist
doing people's homework for them, but maybe someone's sense of smell is
less acute then mine).

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

On 4/29/2024 5:25 AM, Mild Shock wrote:
>
> Well I forgot to say, that only first order
> logic with equality, FOL=, is available.
You also forgot that you posed this as a Prolog, not an FOL, problem.
> 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.--
Jeff Barnett

Its only work if you don't like it, otherwise
its pure logic programming joy. I didn't have
time to try an ancestor formalization yet.

Yes the requirememt is FOL, from the SWI-Prolog
thread one can extract that I am using the
Vidal-Rosset Variant of the Otten Prover Syntax:

:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
:- op( 500, fy, !). % universal quantifier: ![X]:
:- op( 500, fy, ?). % existential quantifier: ?[X]:
:- op( 500,xfy, :).

Thats the Operator definitions in Prolog
to feed the Otten Prover with FOL formulas.
I use the same Operators to feed my model

finder with FOL formulas. Now I have rewritten
the model finder to give a better output:

?- counter(1).
father(0,0)-1
grand_father(0,0)-1
true ;
[...]
father(0,0)-0
father(0,1)-1
father(1,0)-1
father(1,1)-0
grand_father(0,0)-1
grand_father(0,1)-0
grand_father(1,0)-0
grand_father(1,1)-1
true

This is the cosmetic makeover of the model finder:

% problem(+Integer, -Formula)
problem(1, (
![X]:![Y]:(?[Z]:(father(X,Z) & father(Z,Y)) <=> grand_father(X,Y)) =>
~ ?[X]:grand_father(X,X))).

% counter(+Integer)
counter(K) :-
problem(K, F),
between(1, 3, N),
expand(F, N, G),
quine(G, M, V),
V = 0,
keysort(M, L),
(member(X, L), write(X), nl, fail; true).

Plus expand/3 and quine/3 are found here:
https://swi-prolog.discourse.group/t/7398

Barb Knox schrieb:
> This is beginning to smell a lot like homework.

Jeff/Barb you might be highly confused! This is Prolog:

grand_father(X,Y) :- father(X,Z), father(Z,Y).

But this is FOL:

∀X∀Y(∃Z(father(X,Z) & father(Z,Y)) <=> grand_father(X,Y)).

The manual method to go from Prolog to FOL is
the so called Clark Completion. It was recently
made popular again by SWI-Prolog's s(CASP),

but the method exists already quite long:

Logic Programming Theory Lecture 8: Clark Completion
https://www.inf.ed.ac.uk/teaching/courses/lp/2012/slides/lpTheory8.pdf

But I am using it manually as well here. You see
the FOL formula I used as input to the model finder
in the problem/2 fact:

% problem(+Integer, -Formula)
problem(1, (
![X]:![Y]:(?[Z]:(father(X,Z) & father(Z,Y)) <=> grand_father(X,Y)) =>
~ ?[X]:grand_father(X,X))).

Jeff Barnett schrieb:
> You also forgot that you posed this as a Prolog, not an FOL, problem.

Hi,

A full version that has operator definitions
that also work for Scryer Prolog and that uses a
Quine algorithm that even supports function

symbols like in Mace4 by McCune, is found
here on SWI-Prolog SWISH:

McCunes Mace4 Model Finder
https://swish.swi-prolog.org/p/mace4.swinb

Have Fun!

Mild Shock schrieb:
> Its only work if you don't like it, otherwise
> its pure logic programming joy. I didn't have
> time to try an ancestor formalization yet.
>
> Yes the requirememt is FOL, from the SWI-Prolog
> thread one can extract that I am using the
> Vidal-Rosset Variant of the Otten Prover Syntax:
>
> :- op( 500, fy, ~).     % negation
> :- op(1000, xfy, &).    % conjunction
> :- op(1100, xfy, '|').  % disjunction
> :- op(1110, xfy, =>).   % conditional
> :- op(1120, xfy, <=>).  % biconditional
> :- op( 500, fy, !).     % universal quantifier:  ![X]:
> :- op( 500, fy, ?).     % existential quantifier:  ?[X]:
> :- op( 500,xfy, :).
>
> Thats the Operator definitions in Prolog
> to feed the Otten Prover with FOL formulas.
> I use the same Operators to feed my model
>
> finder with FOL formulas. Now I have rewritten
> the model finder to give a better output:
>
> ?- counter(1).
> father(0,0)-1
> grand_father(0,0)-1
> true ;
> [...]
> father(0,0)-0
> father(0,1)-1
> father(1,0)-1
> father(1,1)-0
> grand_father(0,0)-1
> grand_father(0,1)-0
> grand_father(1,0)-0
> grand_father(1,1)-1
> true
>
> This is the cosmetic makeover of the model finder:
>
> % problem(+Integer, -Formula)
> problem(1, (
>   ![X]:![Y]:(?[Z]:(father(X,Z) & father(Z,Y)) <=> grand_father(X,Y)) =>
>   ~ ?[X]:grand_father(X,X))).
>
> % counter(+Integer)
> counter(K) :-
>    problem(K, F),
>    between(1, 3, N),
>    expand(F, N, G),
>    quine(G, M, V),
>    V = 0,
>    keysort(M, L),
>    (member(X, L), write(X), nl, fail; true).
>
> Plus expand/3 and quine/3 are found here:
> https://swi-prolog.discourse.group/t/7398
>
> Barb Knox schrieb:
> > This is beginning to smell a lot like homework.