Relational clones

This section is only a remark, not needed for the next ones.

Truth of formulas in products

Given a product P=∏_i_∈_I E_i of any family of L-systems E_i, and any formula Φ with any number n of free variables, let us compare the truth of Φ(x) in P for some tuple x∈Pⁿ of values of free variables, with the value (∀i∈I, Φ(x_i)) obtained as the product of the structures defined by the same formula in each E_i, where x=∏_i∈Ix_i, i.e.
∀i∈I, x_i = π_i ० x ∈E_iⁿ.
We will do it with elementary formulas, from which the behavior of some more complex formulas can eventually be deduced.

There is equivalence with the equality symbol: ∀x,y∈P, (x=y ⇔∀i∈I, x_i = y_i), and also for a formula Φ made of a relation symbol s with a choice of substitution h of its arguments by free variables:

Φ(x) ⇔ s_P(x०h) ⇔ (∀i∈I,s_i(x०h)) ⇔ (∀i∈I,Φ(x_i))

which simplifies the remaining needed study, to cases without substitutions. Now let us see the effects of connectives and quantifiers (between relation symbols s interpreted in P as s_P(x)⇔ ∀i∈I, s_i(x_i)):

(r_P(x) ∧s_P(x)) ⇔	∀i∈I,(r_i(x_i)∧s_i(x_i))
(r_P(x)∨s_P(x)) ⇒	∀i∈I,(r_i(x_i)∨s_i(x_i))
(r_P(x) ⇒ s_P(x)) ⇐	∀i∈I,(r_i(x_i)⇒s_i(x_i))
(∀y∈P, r_P(x,y)) ⇐	∀i∈I, ∀y_i∈E_i, r_i(x_i,y_i)
(P≠ⵁ ∧ ∀y∈P, r_P(x,y)) ⇒	∀i∈I, ∀y_i∈E_i, r_i(x_i, y_i)
(∃y∈P, r_P(x,y,...)) ⇒	∀i∈I, ∃y_i∈E_i, r_i(x_i,y_i)
(∃y∈P, r_P(x,y,...)) ⇐	(AC_I∧∀i∈I, ∃y_i∈E_i, r_i(x_i,y_i))

The ⇒ cases (white and in green) can be understood as deduced from π_i ∈ Mor_L(P,E_i) as seen in 3.1, plus the preservation of ∀ by surjective morphisms.
The converse implications (⇐, in white and yellow, where AC_I is the axiom of choice over I, see 2.10), describe which properties are "preserved by taking the product of systems".
For example if each member of a product satisfies an axiom of the form (∀ variables) (F₁ ∧ ... ∧ F_n) ⇒ G where F₁,..., F_n and G are relation symbols applied to variables, then the product also satisfies this axiom.
For example, any product of ordered sets is an ordered set; but a product of totally ordered sets, is a set with an order that is usually not a total order.

Relational clones

For any set R ⊂ Rel_E of relations in E, the relational clone generated by R, is the set Cl'(R)⊂ Rel_E of relations defined by formulas with symbols in R∪{∃,=,∧, variables}. This is also a closure, whose closed elements are the relational clones (or clones of relations).

For any system E and formula Φ, the truth of Φ in E is written E⊨Φ .

Theorem. The set of invariants Inv S of any S ⊂ Op_E, is a relational clone. In other words, for any R ⊂ Rel_E we have Cl'(R) ⊂ Inv Pol R.

Proof 1:

Let R ⊂ Rel_E and s ∈ Mor_R(Eⁿ,E)⊂Pol R.
Let m∈ℕ, and a formula Φ with symbols in R∪{∃,=,∧}, variables bound by ∃, and m free variables.
Let r ∈Cl'(R) the m-ary relation defined by Φ in E.
We saw that (∀i<n, E⊨Φ(π_i०x)) ⇒ (Eⁿ⊨Φ(x)) using the truth of the axiom of choice over finite sets.
Then, (s∈Mor_R(Eⁿ,E) ∧ Eⁿ⊨Φ(x)) ⇒ (E⊨Φ(s०x)).
We conclude ∀x∈(Eⁿ)^m, (∀i<n, r(π_i०x)) ⇒ r(s०x), i.e. s ▷r.

Proof 2:

For any S ⊂ Op_E, let us verify that Inv S is a clone of relations, that is, ∀m∈ℕ, ∀r⊂E^m defined by a term with language in {∃,=,∧}∪Inv S, we have r∈Sub_S(E^m). We can verify that we stay in Inv S in the following steps of building formulas:

Substitutions : for the relation r' defined by a relation symbol r with a substitution map u from r's arguments list I to the variables list J, let f=∏_i_∈_I π_u(i) ∈Mor(E^J,E^I).
Then r∈Sub_S(E^I) ⇒ r'=f^-1(r)∈Sub_S(E^J).

∃: the relation defined by (∃x∈E, r(x,y,...)) is the image of r by the morphism ∏_i_≠0 π_i

=: this relation is Gr Id_E = Im (Id_E⊓Id_E) ∈ Sub_S(E×E)

∧: intersections of subalgebras are subalgebras.

Other ways to operate on subalgebras reflect formulas with these symbols: for example
A∈Sub_S(E) ⇒ (Id_E⊓Id_E)[A] = {(x,y)∈E²|x∈A ∧ x=y}

For each relational clone R, the set Gr*R is a clone of operations : for example, the graph of the term "x" with variables x,y, is {(x,y,z)|z=x};
if f,g∈E^E we have (x,y)∈ Gr(g०f) ⇔ (∃z∈E, (x,z)∈Gr(f) ∧ (z,y)∈Gr(g)).

Duality theories with structures

A duality theory is a theory describing duality systems. Let R be a relational language, that is interpreted in K. We may even see it as R⊂Rel_K.

For any set E, we have a Galois connection between interpretations of R in E and subsets E' ⊂ K^E, defined as follows:

Any E' ⊂ K^E defines an interpretation of each n-ary r∈R in E as r_E={(x₁,..., x_n)∈Eⁿ|∀y∈E' , r(y(x₁),...,y(x_n))}. This is the only one making (∏_y_∈_E' y) an embedding from E to K^E'.
Any interpretation of R in E gives a set E*= Mor_R(E,K) ⊂ K^E.

Now let us consider duality theories, or kinds of K-duality systems (E,E',〈 , 〉), that interpret R in E as defined from E' in this way. (This forms a first-order theory, while the claim of using of E* would form a second order theory).

By the properties of closures of the above Galois connection we have:

E' ⊂ E*
As ∏_y_∈_E' y is an embedding of E into K^E' (injective as E is assumed to be separated by E'),
∏_y_∈_E* y is also an embedding of E into K^E^* (which means that the used R-structure on E is closed), i.e. (E,E*) is another K-duality system giving the same R-structure on E.

Thus, as the system E is a subset of an exponentiation of K (namely K^E'), every axiom of the form (∀ variables) (F₁ ∧ ... ∧ F_n) ⇒ G (where (F₁ ,..., F_n, G) are relation symbols applied to variables) that is true in K, is also true in E.

Theorem. For any two K-duality systems (E,E',〈 , 〉) and (F,F',〈 , 〉') interpreting R in E and F in this way,

Mor((E,E'),(F,F')) ⊂ Mor_R(E,F)
Mor((E,E*),(F,F')) = Mor_R(E,F)

Proof.

As (∏_y_∈_F' y) is an R-embedding from F to K^F', we have

∀f∈F^E, f ∈ Mor_R(E,F) ⇔ (∏_y_∈_F' y)०f ∈ Mor_R(E,K^F')

⇔ ∀y∈F', y०f ∈ Mor_R(E,K)=E*

⇔ f ∈ Mor((E,E*),(F,F'))

As E'⊂E*, the condition f∈Mor((E,E'),(F,F')), that is ∀y∈F', y०f ∈ E', is more restrictive, thus the inclusion.

Now, let S ⊂ Pol R ⊂ Op_K. As seen above, in any K-duality system (E,E') we have E* ∈ Sub_S(K^E).
As the R-structure in E stays unchanged whether it is defined from E' or from E*, it remains also unchanged using any X such that E' ⊂ X ⊂ E*. This is the case for X = E'_S = the S-algebra generated by E', that is the smallest sub-S-algebra of E* (or equivalently of K^E) such that E' ⊂ X.

∀f∈F^E, f ∈ Mor_R(E,F)	⇔ (∏_y_∈_F' y)०f ∈ Mor_R(E,K^F')
	⇔ ∀y∈F', y०f ∈ Mor_R(E,K)=E*
	⇔ f ∈ Mor((E,E*),(F,F'))