# Extracting a domain from a relation

Quote from Vadim on January 11, 2020, 3:17 amI'm trying to prove the following relational lattice identity:

`(y` ^ x') v (y' ^ x `) = (y' v x') ^ (y` v x `).`

Assuming that

`x`

and`y`

are two binary relations, and introducing the three unary domain relations`P1`

,`P2`

,`P3`

, I have translated it into the Prover9 dialect of the predicate calculus syntax the following way:formulas(assumptions).

`( exists p x(p,q)) <-> P3(q).`

( exists s x(p2,s)

| exists r y(r,p2) ) <-> P2(p2).

( exists r y(q,r)) <-> P1(q).

end_of_list.

formulas(goals).

`exists p1 exists p3 (`

`(P3(p3) & exists p1 exists p2 y(p1,p2))`

`& -x(p2,p3)`

`|`

`-y(p1,p2) &`

`(P1(p1) & exists p2 exists p3 x(p2,p3))`

`)`

`<->`

`exists p1 exists p3`

`(-x(p2,p3)`

`|`

`-y(p1,p2))`

`&`

`exists p1 exists p3 (`

`P3(p3) & (exists p1 exists p2 y(p1,p2))`

`| P1(p1) & (exists p2 exists p3 x(p2,p3))`

`)`

`.`

In the formulas part I'm trying to assert that

`P1`

and`P2`

are the domains of the relation`y`

, while`P2`

and`P3`

are domains of the relation x. However, Mace4 exhibits the following counterexample:

`P1(0).`

`- P1(1).`

`- P1(2).`

`P2(0).`

`- P2(1).`

`- P2(2).`

`- P3(0).`

`- P3(1).`

`- P3(2).`

`- x(0,0).`

`x(0,1).`

`- x(0,2).`

`- x(1,0).`

`- x(1,1).`

`- x(1,2).`

`- x(2,0).`

`- x(2,1).`

`- x(2,2).`

`y(0,0).`

`- y(0,1).`

`- y(0,2).`

`- y(1,0).`

`- y(1,1).`

`- y(1,2).`

`- y(2,0).`

`- y(2,1).`

`- y(2,2).`

It insists on

`P3`

being empty, but this is wrong because`x`

is not empty (i.e.`x(0,1)=true`

). Certainly, it would invalidate the first formula/assumption that`P3`

is domain of`x`

?Edit: have solved the domain emptiness puzzle with the following formulas/assumptions:

`all q (P3(q) | all p -x(p,q)).`

`all q (P1(q) | all p -y(q,p)).`

`all q (P2(q) | all p (-y(p,q)&-x(q,p)) ).`

Still, there seems to be a counterexample...

I'm trying to prove the following relational lattice identity:

`(y` ^ x') v (y' ^ x `) = (y' v x') ^ (y` v x `).`

Assuming that `x`

and `y`

are two binary relations, and introducing the three unary domain relations `P1`

, `P2`

, `P3`

, I have translated it into the Prover9 dialect of the predicate calculus syntax the following way:

formulas(assumptions).

`( exists p x(p,q)) <-> P3(q).`

( exists s x(p2,s)

| exists r y(r,p2) ) <-> P2(p2).

( exists r y(q,r)) <-> P1(q).

end_of_list.

formulas(goals).

`exists p1 exists p3 (`

`(P3(p3) & exists p1 exists p2 y(p1,p2)) `

`& -x(p2,p3)`

`| `

`-y(p1,p2) & `

`(P1(p1) & exists p2 exists p3 x(p2,p3)) `

`) `

`<->`

`exists p1 exists p3`

`(-x(p2,p3)`

`| `

`-y(p1,p2))`

`&`

`exists p1 exists p3 (`

`P3(p3) & (exists p1 exists p2 y(p1,p2)) `

`| P1(p1) & (exists p2 exists p3 x(p2,p3)) `

`)`

`.`

In the formulas part I'm trying to assert that `P1`

and `P2`

are the domains of the relation `y`

, while `P2`

and `P3`

are domains of the relation x. However, Mace4 exhibits the following counterexample:

`P1(0).`

`- P1(1).`

`- P1(2).`

`P2(0).`

`- P2(1).`

`- P2(2).`

`- P3(0).`

`- P3(1).`

`- P3(2).`

`- x(0,0).`

`x(0,1).`

`- x(0,2).`

`- x(1,0).`

`- x(1,1).`

`- x(1,2).`

`- x(2,0).`

`- x(2,1).`

`- x(2,2).`

`y(0,0).`

`- y(0,1).`

`- y(0,2).`

`- y(1,0).`

`- y(1,1).`

`- y(1,2).`

`- y(2,0).`

`- y(2,1).`

`- y(2,2).`

It insists on `P3`

being empty, but this is wrong because `x`

is not empty (i.e. `x(0,1)=true`

). Certainly, it would invalidate the first formula/assumption that `P3`

is domain of `x`

?

Edit: have solved the domain emptiness puzzle with the following formulas/assumptions:

`all q (P3(q) | all p -x(p,q)).`

`all q (P1(q) | all p -y(q,p)).`

`all q (P2(q) | all p (-y(p,q)&-x(q,p)) ).`

Still, there seems to be a counterexample...

Quote from AntC on January 11, 2020, 6:20 amAs the only person round here likely to understand Prover9 format, I suppose I'd better chirp up. I've never before seen formulas trying to express domains, so the best I can do is act the cardboard programmer.This comment (lower down) "In the formulas part I'm trying to assert that`P1`

and`P2`

are the domains of the relation`y`

, while`P2`

and`P3`

are domains of the relation x." seems inconsistent with the ' formulas(assumptions)' disjunction`<-> P2(p2).`

One of the disjuncts uses`x(p2,s)`

, the other`y(r,p2)`

. So that seems to assert`P2`

is in the domain of both`x`

(its first domain) and`y`

(its second domain).Edit:ahh, my mistake (I'll leave this here for ref). You put`y`

first in your narrative, but second in the code. I read them the wrong way round.Quote from Vadim on January 11, 2020, 3:17 amI'm trying to prove the following relational lattice identity:

`(y` ^ x') v (y' ^ x `) = (y' v x') ^ (y` v x `).`

Assuming that

`x`

and`y`

are two binary relations, and introducing the three unary domain relations`P1`

,`P2`

,`P3`

, I have translated it into the Prover9 dialect of the predicate calculus syntax the following way:formulas(assumptions).

`( exists p x(p,q)) <-> P3(q).`

( exists s x(p2,s)

| exists r y(r,p2) ) <-> P2(p2).

( exists r y(q,r)) <-> P1(q).

end_of_list.

formulas(goals).

`exists p1 exists p3 (`

`(P3(p3) & exists p1 exists p2 y(p1,p2))`

`& -x(p2,p3)`

`|`

`-y(p1,p2) &`

`(P1(p1) & exists p2 exists p3 x(p2,p3))`

`)`

`<->`

`exists p1 exists p3`

`(-x(p2,p3)`

`|`

`-y(p1,p2))`

`&`

`exists p1 exists p3 (`

`P3(p3) & (exists p1 exists p2 y(p1,p2))`

`| P1(p1) & (exists p2 exists p3 x(p2,p3))`

`)`

`.`

In the formulas part I'm trying to assert that

`P1`

and`P2`

are the domains of the relation`y`

, while`P2`

and`P3`

are domains of the relation x. However, Mace4 exhibits the following counterexample:

`P1(0).`

`- P1(1).`

`- P1(2).`

`P2(0).`

`- P2(1).`

`- P2(2).`

`- P3(0).`

`- P3(1).`

`- P3(2).`

`- x(0,0).`

`x(0,1).`

`- x(0,2).`

`- x(1,0).`

`- x(1,1).`

`- x(1,2).`

`- x(2,0).`

`- x(2,1).`

`- x(2,2).`

`y(0,0).`

`- y(0,1).`

`- y(0,2).`

`- y(1,0).`

`- y(1,1).`

`- y(1,2).`

`- y(2,0).`

`- y(2,1).`

`- y(2,2).`

It insists on

`P3`

being empty, but this is wrong because`x`

is not empty (i.e.`x(0,1)=true`

). Certainly, it would invalidate the first formula/assumption that`P3`

is domain of`x`

?Edit: have solved the domain emptiness puzzle with the following formulas/assumptions:

`all q (P3(q) | all p -x(p,q)).`

`all q (P1(q) | all p -y(q,p)).`

`all q (P2(q) | all p (-y(p,q)&-x(q,p)) ).`

Still, there seems to be a counterexample...

`P1`

and `P2`

are the domains of the relation `y`

, while `P2`

and `P3`

are domains of the relation x." seems inconsistent with the ' formulas(assumptions)' disjunction `<-> P2(p2).`

One of the disjuncts uses `x(p2,s)`

, the other `y(r,p2)`

. So that seems to assert `P2`

is in the domain of both `x`

(its first domain) and `y`

(its second domain).**Edit:**ahh, my mistake (I'll leave this here for ref). You put

`y`

first in your narrative, but second in the code. I read them the wrong way round.Quote from Vadim on January 11, 2020, 3:17 amI'm trying to prove the following relational lattice identity:

`(y` ^ x') v (y' ^ x `) = (y' v x') ^ (y` v x `).`

`x`

and`y`

are two binary relations, and introducing the three unary domain relations`P1`

,`P2`

,`P3`

, I have translated it into the Prover9 dialect of the predicate calculus syntax the following way:formulas(assumptions).

( exists s x(p2,s)

| exists r y(r,p2) ) <-> P2(p2).

( exists r y(q,r)) <-> P1(q).

end_of_list.

formulas(goals).

`exists p1 exists p3 (`

`(P3(p3) & exists p1 exists p2 y(p1,p2))`

`& -x(p2,p3)`

`|`

`-y(p1,p2) &`

`(P1(p1) & exists p2 exists p3 x(p2,p3))`

`)`

`<->`

`exists p1 exists p3`

`(-x(p2,p3)`

`|`

`-y(p1,p2))`

`&`

`exists p1 exists p3 (`

`P3(p3) & (exists p1 exists p2 y(p1,p2))`

`| P1(p1) & (exists p2 exists p3 x(p2,p3))`

`)`

`.`

`P1`

and`P2`

are the domains of the relation`y`

, while`P2`

and`P3`

are domains of the relation x. However, Mace4 exhibits the following counterexample:

`P1(0).`

`- P1(1).`

`- P1(2).`

`P2(0).`

`- P2(1).`

`- P2(2).`

`- P3(0).`

`- P3(1).`

`- P3(2).`

`- x(0,0).`

`x(0,1).`

`- x(0,2).`

`- x(1,0).`

`- x(1,1).`

`- x(1,2).`

`- x(2,0).`

`- x(2,1).`

`- x(2,2).`

`y(0,0).`

`- y(0,1).`

`- y(0,2).`

`- y(1,0).`

`- y(1,1).`

`- y(1,2).`

`- y(2,0).`

`- y(2,1).`

`- y(2,2).`

`P3`

being empty, but this is wrong because`x`

is not empty (i.e.`x(0,1)=true`

). Certainly, it would invalidate the first formula/assumption that`P3`

is domain of`x`

?Edit: have solved the domain emptiness puzzle with the following formulas/assumptions:

`all q (P3(q) | all p -x(p,q)).`

`all q (P1(q) | all p -y(q,p)).`

`all q (P2(q) | all p (-y(p,q)&-x(q,p)) ).`

Still, there seems to be a counterexample...

Quote from AntC on January 11, 2020, 10:18 amThis code looks odd, particularly the scoping of the

`exists`

-bound`pn`

variables:

`exists p1 exists p3 (`

`(P3(p3) & exists p1 exists p2 y(p1,p2))`

`& -x(p2,p3)`

% this`p2`

is free in the whole formula

`|`

`-y(p1,p2) &`

% this`p2`

is the same free

`(P1(p1) & exists p2 exists p3 x(p2,p3))`

`)`

`<->`

`exists p1 exists p3`

`(-x(p2,p3)`

%`p2`

free

`|`

`-y(p1,p2))`

%`p2`

free

`&`

`exists p1 exists p3 (`

`P3(p3) & (exists p1 exists p2 y(p1,p2))`

`| P1(p1) & (exists p2 exists p3 x(p2,p3))`

`)`

`.`

So the formula has a

`p2`

free (i.e. implicit (for)`all`

), but some appearances of`p2`

are`exists`

-bound. The free occurrences of`p2`

are negations in branches of disjunctions. The formula has`p1, p3`

`exists`

-bound at outer scope, but some appearances of`p1, p3`

are`exists`

-bound at narrow scope.The negations, disjunctions, local bindings,

`exists`

are all things that make the formula difficult to read. It seems over-complicated for what you're aiming to do. (Also it'll give Prover9 inference severe indigestion, as Tadeusz points out.)

This code looks odd, particularly the scoping of the `exists`

-bound `pn`

variables:

`exists p1 exists p3 (`

`(P3(p3) & exists p1 exists p2 y(p1,p2))`

`& -x(p2,p3)`

% this `p2`

is free in the whole formula

`|`

`-y(p1,p2) &`

% this `p2`

is the same free

`(P1(p1) & exists p2 exists p3 x(p2,p3))`

`)`

`<->`

`exists p1 exists p3`

`(-x(p2,p3)`

% `p2`

free

`|`

`-y(p1,p2))`

% `p2`

free

`&`

`exists p1 exists p3 (`

`P3(p3) & (exists p1 exists p2 y(p1,p2))`

`| P1(p1) & (exists p2 exists p3 x(p2,p3))`

`)`

`.`

So the formula has a `p2`

free (i.e. implicit (for)`all`

), but some appearances of `p2`

are `exists`

-bound. The free occurrences of `p2`

are negations in branches of disjunctions. The formula has `p1, p3`

`exists`

-bound at outer scope, but some appearances of `p1, p3`

are `exists`

-bound at narrow scope.

The negations, disjunctions, local bindings, `exists`

are all things that make the formula difficult to read. It seems over-complicated for what you're aiming to do. (Also it'll give Prover9 inference severe indigestion, as Tadeusz points out.)

Quote from Vadim on January 11, 2020, 5:53 pmThank you Anthony. Forum ate my indentations:-) Simplified domain definition, and it is proven:

formulas(assumptions). all q D(q). formulas(goals). %(y` ^ x') v (y' ^ x `) = (y' v x') ^ (y` v x `). ( exists p3 ( (D(p3) & exists s exists t y(s,t)) & -x(p2,p3) ) | exists p1 ( (D(p1) & exists s exists t x(s,t)) & -y(p1,p2) ) ) <-> ( ( exists t2 -x(p2,t2) | exists s2 -y(s2,p2) ) & ( exists u (D(u) & exists q exists r y(q,r)) | exists w (D(w) & exists q exists r x(q,r)) ) ).

Thank you Anthony. Forum ate my indentations:-) Simplified domain definition, and it is proven:

formulas(assumptions). all q D(q). formulas(goals). %(y` ^ x') v (y' ^ x `) = (y' v x') ^ (y` v x `). ( exists p3 ( (D(p3) & exists s exists t y(s,t)) & -x(p2,p3) ) | exists p1 ( (D(p1) & exists s exists t x(s,t)) & -y(p1,p2) ) ) <-> ( ( exists t2 -x(p2,t2) | exists s2 -y(s2,p2) ) & ( exists u (D(u) & exists q exists r y(q,r)) | exists w (D(w) & exists q exists r x(q,r)) ) ).