Self-evidently I am not my grandpa

[Mild Shock]

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"

[Mild Shock]

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!

Post by Mild Shock

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.
Lets say you build a Prolog family database and
make definitions for father, grand-father etc..
"Im my own grandpa"

[Moebius]

Post by Mild Shock
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
McCunes Mace4 Model Finder
https://swish.swi-prolog.org/p/mace4.swinb
Have Fun!

 > 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.
Lets say you build a Prolog family database and
make definitions for father, grand-father etc..
"Im my own grandpa"

"Problem 1: I am my own grandpa?

Is this possible from terminological definition:
grand_father(X,Y) :- father(X,Z), father(Z,Y)."

Of course. Where's the problem?

If X = Y = I
and Z = Nop

and in the datebase:
father(I, Nobody)
father(Nobody, I)

then clearly

grand_father(I,I)

holds. No?

[Moebius]

Post by Mild Shock
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
McCunes Mace4 Model Finder
https://swish.swi-prolog.org/p/mace4.swinb
Have Fun!

Post by Mild Shock

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.
Lets say you build a Prolog family database and
make definitions for father, grand-father etc..
"Im my own grandpa"

"Problem 1: I am my own grandpa?

Is this possible from terminological definition:
grand_father(X,Y) :- father(X,Z), father(Z,Y)."

Of course. Where's the problem?

If X = Y = I
and Z = Nobody

and in the datebase:
father(I, Nobody)
father(Nobody, I)

then clearly

grand_father(I,I)

holds. No?

[Mild Shock]

Yeah you find such a solution also among
the answers that the model finder generates:

% ?- counter(1).
% father(0,0)-1
% grand_father(0,0)-1
% 1true
% father(0,0)-1 father(0,1)-0 father(1,0)-0 father(1,1)-0
% grand_father(0,0)-1 grand_father(0,1)-0
grand_father(1,0)-0 grand_father(1,1)-0
% 2true
% father(0,0)-1 father(0,1)-1 father(1,0)-0 father(1,1)-0
% grand_father(0,0)-1 grand_father(0,1)-1
grand_father(1,0)-0 grand_father(1,1)-0
% 3true
% father(0,0)-1 father(0,1)-0 father(1,0)-1 father(1,1)-0
grand_father(0,0)-1 grand_father(0,1)-0
grand_father(1,0)-1 grand_father(1,1)-0
% 4true
https://swish.swi-prolog.org/p/mace4.swinb

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

Problem 1 is defined as:

/* I am my own grandpa? */
problem(1, (
@[X]: @[Y]:(#[Z]:(father(X,Z) & father(Z,Y)) <=> grand_father(X,Y)) =>
~ #[X]:grand_father(X,X))).

I have also toyed around with Problem 2:

/* Is every monoid commutative? */
problem(2, (
(@[X]:(0*X = X) &
@[X]:(X*0 = X) &
@[X]: @[Y]: @[Z]:((X*Y)*Z = X*(Y*Z))) => (a*b = b*a))).

But Problem 3 is quite hard, takes 12 minutes:

/* Is every group commutative? */
problem(3, (
(@[X]:(0*X = X) &
@[X]:(i(X)*X = 0) &
@[X]: @[Y]: @[Z]:((X*Y)*Z = X*(Y*Z))) => (a*b = b*a))).

McCune claims it takes < 1 second with his mace4.

Don't know yet how to speed up Problem 3.

Post by Moebius
"Problem 1: I am my own grandpa?
grand_father(X,Y) :- father(X,Z), father(Z,Y)."
Of course. Where's the problem?
If X = Y = I
and Z = Nobody
father(I, Nobody)
father(Nobody, I)
then clearly
grand_father(I,I)
holds. No?

[Moebius]

Am 02.05.2024 um 02:59 schrieb Mild Shock:

Ok, I have to admit that I unconsciously assumed that the database does
not allow for father(a,a) entries. Hence I missed the solutions with
domain size = 1, sorry.

Of course if this restriction does not exist, there's a solution with
database entry father(I,I) too. :-)

In general we get a solution (for all n e IN) with database entries
father(I, X_1)
father(X_1, X_2)
:
father(X_n, I)
and I, X_1, ... X_n pairwise distinct.

In this cases: grand_father(I,I) [with domain size = n+1].

Post by Mild Shock
Yeah you find such a solution also among
% ?- counter(1).
% father(0,0)-1
% grand_father(0,0)-1
% 1true
% father(0,0)-1 father(0,1)-0 father(1,0)-0 father(1,1)-0
% grand_father(0,0)-1 grand_father(0,1)-0
grand_father(1,0)-0 grand_father(1,1)-0
% 2true
% father(0,0)-1 father(0,1)-1 father(1,0)-0 father(1,1)-0
% grand_father(0,0)-1 grand_father(0,1)-1
grand_father(1,0)-0 grand_father(1,1)-0
% 3true
% father(0,0)-1 father(0,1)-0 father(1,0)-1 father(1,1)-0
grand_father(0,0)-1 grand_father(0,1)-0
grand_father(1,0)-1 grand_father(1,1)-0
% 4true
https://swish.swi-prolog.org/p/mace4.swinb
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 fourth 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.
/* I am my own grandpa? */
problem(1, (
  ~ #[X]:grand_father(X,X))).
/* Is every monoid commutative? */
problem(2, (
/* Is every group commutative? */
problem(3, (
McCune claims it takes < 1 second with his mace4.
Don't know yet how to speed up Problem 3.

Post by Moebius
"Problem 1: I am my own grandpa?
grand_father(X,Y) :- father(X,Z), father(Z,Y)."
Of course. Where's the problem?
If X = Y = I
and Z = Nobody
father(I, Nobody)
father(Nobody, I)
then clearly
grand_father(I,I)
holds. No?

[Mild Shock]

If the X_i are distinct from each other and distinct from I.

Post by Moebius
father(I, X_1)
father(X_1, X_2)
father(X_n, I)

Its quite difficult to satisfy for n>1:

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

Maybe you have ancestor/2 in mind? How would you define it?

Post by Moebius
Ok, I have to admit that I unconsciously assumed that the database does
not allow for father(a,a) entries. Hence I missed the solutions with
domain size = 1, sorry.
Of course if this restriction does not exist, there's a solution with
database entry father(I,I) too. :-)
In general we get a solution (for all n e IN) with database entries
  father(I, X_1)
  father(X_1, X_2)
  father(X_n, I)
and I, X_1, ... X_n pairwise distinct.
In this cases: grand_father(I,I) [with domain size = n+1].

Post by Mild Shock
Yeah you find such a solution also among
% ?- counter(1).
% father(0,0)-1
% grand_father(0,0)-1
% 1true
% father(0,0)-1 father(0,1)-0 father(1,0)-0 father(1,1)-0
% grand_father(0,0)-1 grand_father(0,1)-0
grand_father(1,0)-0 grand_father(1,1)-0
% 2true
% father(0,0)-1 father(0,1)-1 father(1,0)-0 father(1,1)-0
% grand_father(0,0)-1 grand_father(0,1)-1
grand_father(1,0)-0 grand_father(1,1)-0
% 3true
% father(0,0)-1 father(0,1)-0 father(1,0)-1 father(1,1)-0
grand_father(0,0)-1 grand_father(0,1)-0
grand_father(1,0)-1 grand_father(1,1)-0
% 4true
https://swish.swi-prolog.org/p/mace4.swinb
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 fourth 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.
/* I am my own grandpa? */
problem(1, (
   ~ #[X]:grand_father(X,X))).
/* Is every monoid commutative? */
problem(2, (
/* Is every group commutative? */
problem(3, (
McCune claims it takes < 1 second with his mace4.
Don't know yet how to speed up Problem 3.

Post by Moebius
"Problem 1: I am my own grandpa?
grand_father(X,Y) :- father(X,Z), father(Z,Y)."
Of course. Where's the problem?
If X = Y = I
and Z = Nobody
father(I, Nobody)
father(Nobody, I)
then clearly
grand_father(I,I)
holds. No?

[Moebius]

Post by Mild Shock
If the X_i are distinct from each other and distinct from I.

    father(I, X_1)
    father(X_1, X_2)
    father(X_n, I)

grand_father(X,Y) :- father(X,Z), father(Z,Y).
Maybe you have ancestor/2 in mind? [...]

Indeed. A thinko, sorry.

Post by Mild Shock

Ok, I have to admit that I unconsciously assumed that the database
does not allow for father(a,a) entries. Hence I missed the solutions
with domain size = 1, sorry.
Of course if this restriction does not exist, there's a solution with
database entry father(I,I) too. :-)
In general we get a solution (for all n e IN) with database entries
   father(I, X_1)
   father(X_1, X_2)
   father(X_n, I)
and I, X_1, ... X_n pairwise distinct.
In this cases: grand_father(I,I) [with domain size = n+1].

Post by Mild Shock
Yeah you find such a solution also among
% ?- counter(1).
% father(0,0)-1
% grand_father(0,0)-1
% 1true
% father(0,0)-1 father(0,1)-0 father(1,0)-0 father(1,1)-0
% grand_father(0,0)-1 grand_father(0,1)-0
grand_father(1,0)-0 grand_father(1,1)-0
% 2true
% father(0,0)-1 father(0,1)-1 father(1,0)-0 father(1,1)-0
% grand_father(0,0)-1 grand_father(0,1)-1
grand_father(1,0)-0 grand_father(1,1)-0
% 3true
% father(0,0)-1 father(0,1)-0 father(1,0)-1 father(1,1)-0
grand_father(0,0)-1 grand_father(0,1)-0
grand_father(1,0)-1 grand_father(1,1)-0
% 4true
https://swish.swi-prolog.org/p/mace4.swinb
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 fourth 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.
/* I am my own grandpa? */
problem(1, (
grand_father(X,Y)) =>
   ~ #[X]:grand_father(X,X))).
/* Is every monoid commutative? */
problem(2, (
/* Is every group commutative? */
problem(3, (
McCune claims it takes < 1 second with his mace4.
Don't know yet how to speed up Problem 3.

Post by Moebius
"Problem 1: I am my own grandpa?
grand_father(X,Y) :- father(X,Z), father(Z,Y)."
Of course. Where's the problem?
If X = Y = I
and Z = Nobody
father(I, Nobody)
father(Nobody, I)
then clearly
grand_father(I,I)
holds. No?