Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > sci.math > #627366

Re: Self-evidently I am not my grandpa

Show all headers | View raw

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.

Moebius schrieb:
> "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?
> 
> 

Back to sci.math | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

Self-evidently I am not my grandpa Mild Shock <janburse@fastmail.fm> - 2024-04-27 14:44 +1000
  Re: Self-evidently I am not my grandpa Mild Shock <janburse@fastmail.fm> - 2024-05-02 10:35 +1000
    Re: Self-evidently I am not my grandpa Moebius <invalid@example.invalid> - 2024-05-02 02:49 +0200
    Re: Self-evidently I am not my grandpa Moebius <invalid@example.invalid> - 2024-05-02 02:50 +0200
      Re: Self-evidently I am not my grandpa Mild Shock <janburse@fastmail.fm> - 2024-05-02 10:59 +1000
        Re: Self-evidently I am not my grandpa Moebius <invalid@example.invalid> - 2024-05-02 03:44 +0200
          Re: Self-evidently I am not my grandpa Mild Shock <janburse@fastmail.fm> - 2024-05-03 11:46 +1000
            Re: Self-evidently I am not my grandpa Moebius <invalid@example.invalid> - 2024-05-03 10:07 +0200

csiph-web