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

∀

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*) ⇔ *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 (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 π

The converse implications (⇐, in white and yellow, where AC

For example if each member of a product satisfies an axiom of the form (∀ variables) (

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.

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:

Proof 2:Let

R⊂ Rel_{E}ands∈Mor_{R}(E^{n},E)⊂PolR.

Letm∈ℕ, and a formula Φ with symbols inR∪{∃,=,∧}, variables bound by ∃, andmfree variables.

Letr∈Cl'(R) them-ary relation defined by Φ inE.

We saw that (∀i<n,E⊨Φ(π_{i}०x)) ⇒ (E^{n}⊨Φ(x)) using the truth of the axiom of choice over finite sets.

Then, (s∈Mor_{R}(E^{n},E) ∧E^{n}⊨Φ(x)) ⇒ (E⊨Φ(s०x)).

We conclude ∀x∈(E^{n})^{m}, (∀i<n,r(π_{i}०x)) ⇒r(s०x), i.e.s▷r.

For anyOther ways to operate on subalgebras reflect formulas with these symbols: for exampleS⊂ Op_{E}, let us verify that InvSis a clone of relations, that is, ∀m∈ℕ, ∀r⊂E^{m}defined by a term with language in {∃,=,∧}∪InvS, we haver∈Sub_{S}(E^{m}). We can verify that we stay in InvSin the following steps of building formulas:

- Substitutions : for the relation
r' defined by a relation symbolrwith a substitution mapufromr's arguments listIto the variables listJ, letf=∏_{i}_{∈}_{I}π_{u(i)}∈Mor(E,^{J}E).^{I}

Thenr∈Sub_{S}(E^{I}) ⇒r'=f^{ -1}(r)∈Sub_{S}(E^{J}).- ∃: the relation defined by (∃
x∈E,r(x,y,...)) is the image ofrby 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.

For each relational clone

if