## The Forum for Discussion about The Third Manifesto and Related Matters

Forum breadcrumbs - You are here:
Please or Register to create posts and topics.

# Extracting a domain from a relation

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

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

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

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

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))
)
).
```