How to write in second-order logic that a relation is divisible by another?

177 Views Asked by At

Suppose we have the relation of being 100 meters apart, R. And the relation of being 20 meters apart, M. Then whatever two coordinates a,b are 100m apart (Rab), there are four other coordinates, say c, d, e, f so that Mac, Mcd, Mde, Mef, Mfb. This can be written in FOL with identity as:

∀x∀y(Rxy ⊃ ∃t∃u∃v∃w(Mxt & Mtu & Muv & Mvw & Mwy & x≠t & t ≠ u & u ≠ v & v ≠ w & w ≠ y))

Now suppose I only want to make the statement that R is divisible by M. So without specifying the 100m and 20m, we want to say that there is a natural number n, such that there are n-1 coordinates different than the two coordinates for which R holds, and n M relations hold between them. How can this be written in FOL or SOL?

Edit I think I found it:

∀x∀y(Rxy ⊃ Sxy);

∀x∀y(Sxy ⊃ (∃Z∃t( ( Z = ∅ & t = y) ∨ ( Mxt & Zty & (Zty ⊃ Sty ∨ Z = M) & x≠t & t≠y )))

So we introduce a new relation S (for "separable") for which we state that it can be divided by a new coordinate t into an M relation and another relation that can be either the empty set, the M relation or is itself separable.

Any opinions would be appreciated.

Second edit Thanks to Derek Elkins, my first solution was proved wrong. However, I found this first-order solution

∀x∀y(Rxy ⊃ Sxy);

∀x∀y(Sxy ⊃ ( Mxy ∨ ∃t(Mxt & Sty & x≠t & t≠y) )

It states that R is separable (S), meaning that it either implies M or there is another coordinate such that it has an M relation with x and another separable relation with y.

Any opinions would be appreciated.

Third edit

My second proposal was wrong too. See correct answer below

1

There are 1 best solutions below

1
On BEST ANSWER

I'm pretty sure you can't do this in first-order logic. One way of formulating this would be to say that $R$ is in the transitive closure1 of $M$ (i.e. $\forall x,y.R(x,y)\to M^+(x,y)$), but FOL can't express transitive closures. This isn't a proof, but it is suggestive.

We can express the transitive closure of a first-order predicate in second-order logic. We just formulate it as the smallest relation that contains the generating relation and is transitive. Write $\mathsf{Trans}_M(S)$ for the expression $$(\forall x,y.M(x,y)\to S(x,y))\land(\forall x,y,z.S(x,y)\land S(y,z)\to S(x,z))$$ which states that $S$ is a transitive relation that contains $M$. Then $$\mathsf{Trans}_M(M^+)\land\forall S.\mathsf{Trans}_M(S)\to(\forall x,y.M^+(x,y)\to S(x,y))$$ states that $M^+$ is the transitive closure of $M$. We can then use the formula from the first paragraph and wrap the whole thing in an $\exists M^+$. That is,$$\begin{align}\exists M^+.\mathsf{Trans}_M(M^+)&\land(\forall S.\mathsf{Trans}_M(S)\to(\forall x,y.M^+(x,y)\to S(x,y)))\\&\land(\forall x,y.R(x,y)\to M^+(x,y))\end{align}$$

1 You can add reflexivity if you want.