THE EQUATIONAL THEORIES OF REPRESENTABLE POSITIVE CYLINDRIC AND RELATION ALGEBRAS ARE DECIDABLE. First draft.

H. Andréka August, 1990.

THEOREM. (i) The equational theory of Cs_{n}^{+} = {⟨P(^{n}U), ∪, ∩, ∅,^{n}U, C_{i}, D_{ij}⟩_{i,j<n} : U is a set} is decidable for any ordinal n.

(ii) The equational theory of Rs^{+} = {⟨P(U × U), ∪, ∩, ∅, U × U, ∘, Id,˘ ⟩ : U is a set} is decidable.

Proof: Let n < ω. To any Cs_{n}^{+}–term τ we will associate an existential formula ∃\overline{w}ψ with free variables v_{0}, ..., v_{n−1}, such that \overline{v} is disjoint from \overline{w} and ψ is quantifier–free, and further

(*)  the meanings of τ and ∃\overline{w}ψ are the same.

By this latter we mean the following. Assume that the variables occurring in τ are x_{1}, ..., x_{m} ∈ X. In our first–order language we will consider the elements x ∈ X to be n–ary relation symbols. Let 𝔄 ∈ Cs_{n}^{+} with A ⊆ P(^{n}U), let k : X ⟶ A be an evaluation of the variables and let \overline{u} = ⟨u_{0}, ..., u_{n−1}⟩ ∈ ^{n}U. Then τ^{𝔄}[k] denotes the n–ary relation on U (by evaluating the variables in τ along k), and (U, k(x))_{x∈X} denotes the first–order model with universe U where the relation symbol x ∈ X is realized by k(x) ⊆ ^{n}U. Now (*) means that for any 𝔄, k and \overline{u} we have

⟨u_{0}, ..., u_{n−1}⟩ ∈ τ^{𝔄}[k] iff (U, k(x))_{x∈X} ⊧ ∃\overline{w}ψ[u_{0}, ..., u_{n−1}].

Let trans(τ) denote the first–order formula associated to τ. We now define trans by induction on τ (we will be a little sloppy in doing so): For x ∈ X let trans(x) = x(v_{0}, ..., v_{n−1}). Assume that trans(τ) = ∃\overline{w}ψ, trans(σ) = ∃\overline{z}φ. We may assume (by sloppyness) that \overline{w} and \overline{z} are disjoint. Now

trans(τ + σ) = ∃\overline{w}∃\overline{z}(ψ ∨ φ)
trans(τ · σ) = ∃\overline{w}∃\overline{z}(ψ ∧ φ)
trans(0) = (v_{0} ≠ v_{0})
trans(1) = (v_{0} = v_{0})
trans(c_{i}τ) = ∃v_{j}∃\overline{w}ψ(v_{i}/v_{j}) where v_{j} is a new variable
trans(d_{ij}) = (v_{i} = v_{j})

Now, Cs_{n}^{+} ⊭ τ = σ iff (Cs_{n}^{+} ⊭ τ ≤ σ or Cs_{n}^{+} ⊭ σ ≤ τ). Thus, it is enough to decide whether Cs_{n}^{+} ⊧ τ ≤ σ. Let trans(τ) = ∃\overline{w}ψ, trans(σ) = ∃\overline{z}φ with \overline{w} and \overline{z} disjoint. Then Cs_{n}^{+} ⊭ τ ≤ σ iff ∃\overline{v}(∃\overline{w}ψ ∧ ¬∃\overline{z}φ) is satisfiable, but the latter formula is equivalent to the ∃∀–formula ∃\overline{v}∃\overline{w}∀\overline{z}(ψ ∧ ¬φ) and satisfiability of ∃∀–formulas is decidable.

0This work was supported by the Hungarian National Foundation for Scientific Research Grant No 1810.

The case of n ≥ ω follows from the result in [HMTII] saying that ⟨SPCs_{α} : α ∈ Ord⟩ is a strong system of varieties definable by a schema (i.e. that for an equation e in the language of Cs_{3} we have Cs_{3} ⊧ e iff Cs_{ω} ⊧ e).

The relational algebraic case is completely analogous, therefore we omit its proof. QED.

REMARK. (i) The above proof fails if \underline{dual cylindrifications} c_{i}^{∂} (=−c_{i}−) are added. (Dual cylindrifications are the algebraic counterparts of universal quantifiers.)

(ii) If we omit intersection but add transitive reflexive closure ^{∗} , then we obtain the class of Kleene relation algebras. It is proved in Fischer–Ladner[77], that the equational theory of this class, i.e. that the equational theory of {⟨P(U × U), ∪, ∅, U × U, ∘, Id,˘ ,^{∗}⟩ : U is a set} is decidable. It would be interesting to know what the situation is if we allow both intersection and transitive closure.

PROBLEM 1. Is the equational theory EqK of K = {⟨P(U × U), ∪, ∩, ∅, U × U, ∘, Id,˘ ,^{∗}⟩ : U is a set} decidable? Is EqK the same as the equational theory of {𝔄 : 𝔄 is finite, 𝔄 ⊆ 𝔅 for some 𝔅 ∈ K}?

PROBLEM 2. Let Cs_{n}^{++} be Cs_{n}^{+} expanded with {c_{i}^{∂} : i < n}. Is the equational theory Eq(Cs_{n}^{++}) decidable (for n > 2)?

References

HMTII. Henkin,L. Monk.J.D. and Tarski,A., Cylindric Algebras. Part II. North-Holland, Amsterdam, 1985.

Keywords. Relation algebras, Kleene algebras, cylindric algebras, decidability, algebraic logic. 1980 Mathematics subject classifications: 03G15, 06, 08

H. Andréka : Mathematical Institute of the Hungarian Acad. of Sci., Budapest, Pf.127, H–1364, Hungary