Introduction A first application of the theory of hyperidentities and solid model classes can be found in [2]

General Algebra and Applications 29 (2009 ) 123–151

HYPERSATISFACTION OF FORMULAS IN AGEBRAIC SYSTEMS

Klaus Denecke and Dara Phusanga Universit¨at Potsdam Institut f¨ur Mathematik Am Neuen Palais 10, D–14469 Potsdam (Germany)

e-mail: kdenecke@rz.uni-potsdam.de e-mail: p.phu2514@hotmail.com

Abstract

In [2] the theory of hyperidentities and solid varieties was extended to algebraic systems and solid model classes of algebraic systems. The disadvantage of this approach is that it needs the concept of a formula system. In this paper we present a different approach which is based on the concept of a relational clone. The main result is a characterization of solid model classes of algebraic systems. The results will be applied to study the properties of the monoid of all hypersubstitutions of an ordered algebra.

Keywords: algebraic system, formula, relational clone, hyperformula.

2000 Mathematics Subject Classification: 03B50, 08A30.

1. Introduction

A first application of the theory of hyperidentities and solid model classes can be found in [2]. The main problem of this approach is that the ap- plication of a hypersubstitution to an algebraic system does not give an alge- braic system, but a structure which is called a formula system. In this paper we want to avoid this problem. Here we define the application of a hypersub- stitution to the fundamental relations of a given algebraic system to be ele- ments of the relational clone generated by the set of fundamental relations.

This leads to a derived algebraic system. It is not necessary to consider the class of formula systems.

We notice that our approach is an example of the concept of an institu- tion (see [7]). We describe how hypersubstitution can be used to come from first order logic to a restricted version of second order logic.

An algebraic system of type (τ , τ⁰) is a triple A := (A; (f_i^A)_i∈I, (γ^A_j )_j∈J) consisting of a set A, an indexed set (f_i^A)_i∈I of operations defined on A where f_i^A : Aⁿⁱ → A is n_i-ary and an indexed set of relations γ^A_j ⊆ A^nj where γ^A_j is n_j-ary. The pair (τ , τ⁰) with τ = (n_i)_i∈I, τ⁰ = (n_j)_j∈J of sequences of integers n_i, n_j ∈ N⁺:= N\{0}, is called the type of the algebraic system. For algebraic systems of type (τ , τ⁰) subsystems, homomorphic images, congruences and direct products can be defined and most theorems known from Universal Algebra are valid also in this situation ([5]).

Terms and formulas are expressions in a first-order language which are used to describe properties of algebraic systems and to classify algebraic systems. Our definition of terms and formulas goes back to [5] (see also [2]).

Let Xn= {x₁, . . . , xn} be a finite set of variables, let X = {x₁, . . . , xn, . . . } be countably infinite, let (f_i)_i∈I be an indexed set of operation symbols and let (γ_j)_j∈J be an indexed set of relation symbols. Then the set Wτ(Xn) of all n-ary terms of type τ and the set F_{(τ ,τ}0)(Wτ(Xn)) of all n-ary formulas of type (τ , τ⁰) are defined in the usual way by the following conditions:

(i) Every x_k∈ Xn is an n-ary term of type τ .

(ii) If t₁, . . . , tn_k are n-ary terms of type τ and if f_kis an n_k-ary operation symbol of type τ , then fk(t1, . . . , tnk) is an n-ary term of type τ . Let W_τ(X) := S

n≥1

W_τ(X_n) be the set of all terms of type τ . To define for- mulas of type (τ , τ⁰) we need the logical connectives ∨ and ¬, the quantifier

∃ and the equation symbol ≈.

Definition 1.1. Let n ≥ 1. An n-ary formula of type (τ , τ⁰) is defined in the following inductive way:

(i) If t₁, t₂are n-ary terms of type τ , then the equation t₁ ≈ t₂ is an n-ary formula of type (τ , τ⁰). All variables in t₁ ≈ t₂ are free.

(ii) If t₁, . . . , tnj are n-ary terms of type τ and if γ_j is an nj-ary relation symbol, then γ_j(t₁, . . . , tnj) is an n-ary formula of type (τ , τ⁰). All variables in such a formula are free.

(iii) If F is an n-ary formula of type (τ , τ⁰), then ¬F is an n-ary formula of type(τ , τ⁰). All free variables in F are also free in ¬F . All bound variables in F are also bound in ¬F .

(iv) If F₁ and F₂ are n-ary formulas of type (τ , τ⁰) such that variables occurring simultaneously in both formulas are free in each of them, then F₁ ∨ F₂ is an n-ary formula of type (τ , τ⁰). If a variable occurs in F₁ and F₂ and is not free in both formulas, then F₁ ∨ F₂ is not a formula. Variables that are free in at least one of the formulas F₁ or F₂ are also free in F₁ ∨ F₂. Variables that are bound in either F₁ or F₂ are also bound in F₁∨ F₂.

(v) If F is an n-ary formula of type (τ , τ⁰) and xi ∈ Xn occurs freely in F , then ∃x_i(F ) is an n-ary formula of type (τ , τ⁰). The variable x_i is bound in the formula ∃xi(F ) and all other free or bound variables in F are of the same nature in ∃xi(F ).

Let F_{(τ ,τ}0)(W_τ(X_n)) be the set of all n-ary formulas of type (τ , τ⁰) and let F_{(τ ,τ0)}(Wτ(X)) :=S

n≥1 F_{(τ ,τ0)}(Wτ(Xn)) be the set of all formulas of type (τ , τ⁰).

All free or bound variables occur in Xn or X, resp.. Our definition of formulas follows [5], pp. 115–116.

2. Clones of term operations and relational clones of algebraic systems

We denote by Oⁿ(A) the set of all n-ary operations defined on A and let Relⁿ(A) be the set of all n-ary relations defined on A. Then O(A) :=

S

n≥1Oⁿ(A), Rel(A) := S

n≥1Relⁿ(A) are the sets of all operations and the set of all relations defined on A. Let Sm^n,A be the usual superposition operation for operations, i.e. for m-ary operations t^A₁, . . . , t^A_n and for an n-ary operation s^A on A we define:

S_m^n,A s^A, t^A₁, . . . , t^A_n

a₁, . . . , am

:= s^A t^A₁ a₁, . . . , am

, . . . , t^A_n a₁, . . . , am

for all a₁, . . . , am ∈ A, m, n ∈ N⁺. The projection operations e^n,A_k ∈ Oⁿ(A) are defined by e^n,A_k (a₁, . . . , an) := ak, 1 6 k 6 n. Then one obtains a many- sorted algebra ((Oⁿ(A))_n≥1, (Sm^n,A)_m,n≥1, (e^n,A_k )_{1≤k≤n,n∈N}⁺) which is called clone of all operations defined on A. This algebra satisfies the superasso- ciative identity ;

S_m^p,A s^A, S_m^n,A t^A₁, s₁^A, . . . , snA

, . . . , S_m^n,A tpA

, s₁^A, . . . , snA

= S_m^n,A S_n^p,A s^A, t1A

, . . . , tpA
, s1A

, . . . , snA

), m, n, p = 1, 2, . . .
. Sometimes one speaks of a clone (of operations) as a set of operations defined on the same set A, closed under all superposition operations Sm^n,A, m, n ≥ 1, and containing all projections.

The clone generated by the fundamental operations {f_i^A|i ∈ I} of the algebraic system A = (A; (f_i^A)_i∈I, (γ^A_j)_j∈J) is called the clone of term oper- ations of A and is denoted by T (A). We note that the elements of T (A) can be obtained as induced term operations of A. If (Wτ(X))^Adenotes the set of all induced term operations, then T (A) = (Wτ(X))^A. It is well-known that for algebraic constructions like the formation of subsystems and homomor- phic images the term operations of A play a similar role as the fundamental operations.

Now we are looking for a clone of relations which is generated by the fundamental relations of the algebraic system A. We will use the concept of a relational algebra (see [6]). Usually one considers the following operations on sets of relations:

Definition 2.1. Assume that a₁, a₂, . . . , an, a_n+1, . . . , a_n+mare elements of the set A.

(1) The operation ξ : Relⁿ(A) → Relⁿ(A) defines the cyclic permutation of the inputs by ρ 7→ ξρ with

ξρ := {(a₁, a₂, . . . , a_n)| (a₂, . . . , a_n, a₁) ∈ ρ}.

(2) The operation τ : Relⁿ(A) → Relⁿ(A) exchanges the first and the second input of each n-tuple belonging to the relation ρ by ρ 7→ τ ρ with

τ ρ := {(a₁, a₂, . . . , an)| (a₂, a₁, a₃, . . . , an) ∈ ρ}.

(3) The operation 4 : Relⁿ(A) → Relⁿ⁻¹(A) identifies the first and the second input of each n-tuple in ρ by

4ρ := {(a₁, a₂, . . . , a_n−1)| (a₁, a₁, a₂, . . . , a_n−1) ∈ ρ}.

(4) ◦ : Rel^m(A) × Relⁿ(A) → Rel^n+m−2(A) is the relational product of the relations ρ₁ and ρ₂ and is defined by (ρ₁, ρ₂) 7→ ρ₁◦ ρ₂ with ρ₁◦ ρ₂ := {(a₁, a₂, . . . , a_n−1, an, a_n+1, . . . , a_n+m−2)| ∃b ∈ A, (a₁, a₂, . . . , a_n−1, b) ∈ ρ₂ and (b, an, a_n+1, . . . , a_n+m−2) ∈ ρ₁}.

(5) The operation ∇ : Relⁿ(A) → Relⁿ⁺¹(A) allows the addition of a fictitious coordinate and is defined by ρ 7→ ∇ρ with

∇ρ := {(a₁, a₂, . . . , a_n+1)| (a₂, a₃, . . . , a_n+1) ∈ ρ}.

(6) The projection operations prα1,...,αr : Relⁿ(A) → Rel^r(A) are defined by ρ 7→ prα1,...,αr(ρ) with

prα1,...,αr(ρ) := {(aα1, . . . , aαr) ∈ A^r|∀j ∈ {1, . . . , n}\ {α₁, . . . , αr}

∃a_j ∈ A, ((a₁, . . . a_n) ∈ ρ)}.

(7) × : Relⁿ(A) × Rel^m(A) → Rel^n+m(A) is the cartesian product of two relations ρ₁, ρ₂ and is defined by (ρ₁, ρ₂) 7→ ρ₁× ρ₂ with

ρ₁× ρ₂ := {(a₁, a₂, . . . , a_n, a_n+1, . . . , a_n+m)| (a₁, . . . , a_n) ∈ ρ₁and (a_n+1, . . . , a_n+m) ∈ ρ₂}.

(8) ∩ : Relⁿ(A) × Relⁿ(A) → Relⁿ(A) is the intersection of two relations and is defined by (ρ₁, ρ₂) 7→ ρ₁∩ ρ₂ with

ρ₁∩ ρ₂ := {(a₁, . . . , an)| (a₁, . . . , an) ∈ ρ₁ and (a₁, . . . , an) ∈ ρ₂}.

(9) Let ε be an equivalence relation on {1, . . . , n}. Then δ^ε_n is defined by δ^ε_n:= {(a1, . . . , an) ∈ Aⁿ| (i, j) ∈ ε ⇒ ai = aj}.

To select δ^ε_n from Relⁿ(A) can be regarded as a nullary operation.

Let δ^{{1; 2,3}}₃ be the ternary relation of the form δ^ε_n where ε is given by the partition {{1}, {2, 3}}. The algebra Rel(A) := (Rel(A); ξ, τ , 4, ◦, δ^{{1; 2,3}}₃ )

of type (1, 1, 1, 2, 0) is called the full relational algebra on A. Any subalgebra of Rel(A) is called a relational algebra on A. It turns out (see [6]) that relational algebras are also closed under the operations ∇, prα1,...,αr, × and ∩ and that they contain all relations δ^ε_n. Let Q be the universe of a relational algebra and let R be a non-empty subset of Q. Then we can form the relational subalgebra of the relational algebra Q which is generated by R, i.e. the relational algebra with the universe hRi := T

{B|B is a relational subalgebra of Q and R ⊆ B}.

Let A = (A; (f_i^A)_i∈I, (γ^A_j )_j∈J) be an algebraic system of type (τ , τ⁰).

Then the relational subalgebra of Rel(A) which is generated by the set {γ^A_j|j ∈ J} is said to be the relational clone of the algebraic system A and is denoted by R(A). More precisely, the set h{γ^A_j |j ∈ J}i can be inductively defined by the following steps:

(1) If ρ^A∈ {γ^A_j |j ∈ J}, then ρ^A∈ h{γ^A_j|j ∈ J}i.

(2) Assume that ρ^A, ρ^A₁, ρ^A₂ ∈ h{γ^A_j |j ∈ J}i, then ξρ^A, τ ρ^A, 4ρ^A and (ρ^A₁ ◦ ρ^A₂) ∈ h{γ^A_j|j ∈ J}i.

Since δ^{{1; 2,3}}₃ belongs to the fundamental operations of every relational al- gebra, this relation is contained in h{γ^A_j|j ∈ J}i.

3. Hypersubstitutions for algebraic systems

Hypersubstitutions are originally defined as mappings which send operation symbols of a given type τ to terms and preserve arities. Every hypersubsti- tution σ can inductively be extended to a mapping bσ : Wτ(X) → W_τ(X).

In [2] hypersubstitutions were defined for algebraic systems of type (τ , τ⁰) as mappings σ : {fi|i ∈ I}²∪ {γ_j|j ∈ J} → F_{(τ ,τ}0)(Wτ(X)). The disadvantage of this approach is that it needs the set F_{(τ ,τ}0)(Wτ(X)) of all formulas of type (τ , τ⁰). Our new approach maps fundamental operations to elements of T (A) and fundamental relations to elements of R(A).

Definition 3.1. Let σF : {f_i^A|i ∈ I} → T (A) be a mapping assigning to every ni-ary fundamental operation f_i^A of type τ an ni-ary term operation σF(f_i^A). Any such mapping σF will be called a concrete hypersubstitution.

Every concrete hypersubstitution induces a mappingbσ^F : T (A) → T (A) on the set of all term operations of type τ , as follows:

(1) If t^A = e^n,A_k , then bσF[e^n,A_k ] := e^n,A_k .

(2) If t^A = f_i^A(t^A₁, . . . , t^A_ni) and t^A₁, . . . , t^A_ni ∈ Oⁿ(A), then bσF[f_i^A(t^A₁, . . . , t^A_ni)] := Sn^ni,A(σ_F(f_i^A),bσ_F[t^A₁], . . . ,σb_F[t^A_ni]).

Definition 3.2. Let σR : {γ^A_j |j ∈ J} → R(A) be a mapping assigning to every nj-ary fundamental relation γ^A_j of type τ⁰ an nj-ary relation σR(γ^A_j ) of the relational clone. Any such mapping σR will be called a relational hypersubstitution.

Every relational hypersubstitution of type τ⁰induces a mappingσbR: R(A) → R(A) on the relational clone, as follows:

(1) If ρ^A∈ {γ^A_j |j ∈ J}, then bσ^R[ρ^A] := σR(ρ^A) and bσR[δ^{{1; 2,3}}₃ ] := δ^{{1; 2,3}}₃ .

(2) If ρ^A∈ h{γ^A_j |j ∈ J}i\{γ^A_j |j ∈ J} and if we inductively assume that bσR[ρ^A], bσR[ρ^A₁],σb_R[ρ^A₂] are already defined, then

bσ^R[ξρ^A] := ξ(bσ^R[ρ^A]), bσ^R[τ ρ^A] := τ (bσ^R[ρ^A]),

bσ^R[4ρ^A] := 4(bσ^R[ρ^A]), bσ^R[ρ^A₁ ◦ ρ^A₂] :=bσ^R[ρ^A₁] ◦bσR[ρ^A₂].

Definition 3.3. Any mapping σ : {f_i^A|i ∈ I} ∪ {γ^A_j |j ∈ J} → T (A) ∪ R(A) with σ(f_i^A) := σF(f_i^A) for all i ∈ I and σ(γ^A_j ) := σR(γ^A_j ) for all j ∈ J is called hypersubstitution for the algebraic system A. Let RelhypA(τ , τ⁰) be the set of all hypersubstitutions for the algebraic system A.

Clearly any such hypersubstitution can be written as a pair σ := (σF, σR).

Using the extensions bσ_F and bσ_R we can define an extension bσ : T (A) ∪ R(A) → T (A) ∪ R(A) by bσ := (bσF,σbR). If σ₁, σ₂ ∈ RelhypA(τ , τ⁰), then a product can be defined by σ₁ ◦_hr σ₂ := σb₁ ◦ σ₂. For bσ1 ◦ σ₂ we have b

σ1◦ σ2 = ((bσ1)F, (bσ1)R) ◦ ((σ2)F, (σ2)R) = ((bσ1)F ◦ (σ2)F, (bσ1)R◦ (σ2)R).

Next we prove that the extension of this product is equal to the composition of the extensions.

Lemma 3.4. For any σ₁, σ₂ ∈ RelhypA(τ , τ⁰) we have (σ₁◦_hrσ₂)^b=bσ1◦bσ2.

P roof. Because of the last remark we have to show that (σ₁ ◦hr σ₂)^b= ((σ₁◦_hrσ₂)^b_F,(σ₁◦_hrσ₂)^b_R)=((bσ1)F, (bσ1)R) ◦ ((bσ2)F, (bσ2)R)=((bσ1)F ◦ (bσ2)F, (bσ1)R◦ (bσ2)R), i.e. that (σ1◦hrσ2)^b_F = (bσ1)F ◦ (bσ2)F and (σ1 ◦hrσ2)^b_R = (bσ1)R◦ (bσ2)R. For the functional part we will give a proof by induction on the complexity of the definition of term operations.

(1) If t^A= e^n,A_k , then (σ1◦hrσ2)^b_F [e^n,A_k ]

= e^n,A_k

= (bσ2)_F[e^n,A_k ]

= (bσ1)F[(bσ2)F[e^n,A_k ]]

= ((bσ1)F ◦ (bσ2)F)[e^n,A_k ].

(2) If t^A = f_i^A(t^A₁, . . . , t^A_ni) for i ∈ I and if we assume that

(σ1◦hrσ2)^b_F [t^A_j ] = ((bσ1)F ◦ (bσ2)F)[t^A_j ] for every j ∈ {1, . . . , ni}.

Then

(σ1◦hrσ2)^b_F [f_i^A(t^A₁, . . . , t^A_ni)]

= Sn^ni,A((σ₁◦hrσ₂)F(f_i^A), (σ₁◦hrσ₂)^b_F [t^A₁], . . . , (σ₁◦hrσ₂)^b_F [t^A_ni])

= Sn^ni,A(((bσ1)_F ◦ (σ₂)_F)(f_i^A), ((bσ1)_F ◦ (bσ2)_F)[t^A₁], . . . , ((bσ1)_F ◦ (bσ2)_F)[t^A_ni])

= Sn^ni,A((bσ1)F[(σ2)F(f_i^A)], (bσ1)F[(bσ2)F[t^A₁]], . . . , (bσ1)F[(bσ2)F[t^A_ni]])

= (bσ1)F[Sn^ni,A((σ₂)F(f_i^A), (bσ2)F[t^A₁], . . . , (bσ2)F[t^A_ni])

(using that (bσ1)F is compatible with the operation Sn^ni,A, see e.g [1])

= (bσ1)_F[(bσ2)_F[f_i^A(t^A₁, . . . , t^A_ni)]]

= ((bσ1)F ◦ (bσ2)F)[f_i^A(t^A₁, . . . , t^A_ni)].

For the relational part we will give a proof by induction on the complexity of the definition of a relational clone.

(1) If ρ^A∈ {γ^A_j | j ∈ J}, then

(σ₁◦_hrσ₂)^b_R[ρ^A] = ((σ₁)_R◦ (σ₂)_R)[ρ^A]

= ((bσ1)R◦ (σ₂)R)(ρ^A)

= (bσ1)R[(σ₂)R(ρ^A)]

= (bσ1)_R[(bσ2)_R[ρ^A]]

= ((bσ1)_R◦ (bσ2)_R)(ρ^A).

(2) Assume that ρ^A ∈ h{γ^A_j | j ∈ J}i\{γ^A_j | j ∈ J} and let us inductively assume that (σ1◦hrσ2)^b_R[ρ^A] = ((bσ1)R◦ (bσ2)R) [ρ^A], (σ1◦hrσ2)^b_R[ρ^A₁] = ((bσ1)_R◦ (bσ2)_R)[ρ^A₁], (σ₁◦_hrσ₂)^b_R[ρ^A₂] = ((bσ1)_R◦ (bσ2)_R)[ρ^A₂]. Then

(σ₁◦hrσ₂)^b_R[ξρ^A] = ξ((σ₁◦hrσ₂)^b_R[ρ^A])

= ξ((bσ1)R◦ (bσ2)R[ρ^A])

= ξ((bσ1)_R[(bσ2)_R[ρ^A]])

= (bσ1)R[ξ((bσ2)R[ρ^A])]

= (bσ1)R[(bσ2)R[ξρ^A]]

= ((bσ1)R◦ (bσ2)R)[ξρ^A].

The inductive steps for τ and 4 may be handled similarly.

(σ₁◦_hrσ₂)^b_R[ρ^A₁ ◦ ρ^A₂] = (σ₁◦_hrσ₂)^b_R[ρ^A₁] ◦ (σ₁◦_hrσ₂)^b_R[ρ^A₂]

= (((bσ1)R◦ (bσ2)R)(ρ^A₁)) ◦ (((bσ1)R◦ (bσ2)R)(ρ^A₂))

= (bσ1)R[(bσ2)R[ρ^A₁]] ◦ (bσ1)R[(bσ2)R[ρ^A₁]]

= (bσ1)R[(bσ2)R[ρ^A₁] ◦ (bσ2)R[ρ^A₂]]

= (bσ1)R[(bσ2)R[ρ^A₁ ◦ ρ^A₂]]

= ((bσ1)_R◦ (bσ2)_R)[ρ^A₁ ◦ ρ^A₂].

Finally we have

(σ₁◦_hrσ₂)^b_R[δ^{{1; 2,3}}₃ ]=δ^{{1; 2,3}}₃ =(bσ2)_R[δ^{{1; 2,3}}₃ ]=((bσ1)_R◦ (bσ2)_R)[δ^{{1; 2,3}}₃ ].

An identity element with respect to the multiplication ◦hr can be defined by σ_id:= ((σ_id)F, (σ_id)R) with (σ_id)F(f_i^A) := f_i^Afor all i ∈ I and (σ_id)R(γ^A_j ) :=

γ^A_j for all j ∈ J.

By induction on the complexity of the definition of a term operation t^A∈ T (A) and of the definition of an element ρ^A∈ R(A) one can prove:

Lemma 3.5. For any t^A ∈ T (A) and for any ρ^A ∈ R(A) the following equations are satisfied: (bσid)_F[t^A] = t^Aand (bσid)_R[ρ^A] = ρ^A.

Then as a consequence of Lemma 3.4 and Lemma 3.5 we obtain.

Theorem 3.6. For any algebraic system A of type (τ , τ⁰), (RelhypA(τ , τ⁰),

◦_hr, σ_id) is a monoid.

P roof. Associativity of the operation ◦_hr follows from Lemma 3.4 by (σ1 ◦hr σ2) ◦hr σ3=(σ1 ◦hr σ2)^b◦ σ3=(σc1 ◦ σc2) ◦ σ3=cσ1 ◦ (cσ2 ◦ σ3)=bσ1 ◦ (σ₂◦hrσ₃)= σ₁◦hr(σ₂◦hrσ₃). σid is an identity element since for any σ ∈ RelhypA(τ , τ⁰) we get σ_id◦_hrσ =bσid◦σ=((bσid)_F, (bσid)_R)◦(σ_F, σ_R)=((bσid)_F◦ σF, (bσid)R ◦ σR). From Lemma 3.5 we obtain for any f_i^A, i ∈ I, that ((bσ^id)F ◦ σF)(f_i^A)=(bσ^id)F[σF(f_i^A)]=σF(f_i^A), i.e. (bσ^id)F ◦ σF=σF and for any γ^A_j , j ∈ J we have ((bσid)_R ◦ σ_R)(γ^A_j)= (bσid)_R[σ_R(γ^A_j )]=σ_R(γ^A_j) i.e.

(bσid)R◦ σR=σR. This gives σid ◦hr σ = σ. The equation σ ◦hr σid = σ is clear.

4. Extension of hypersubstitutions to mappings defined on the realizations of formulas

Classes of algebraic systems can be described as model classes of sets of formulas. For a given set of formulas the model class of this set consists precisely of those algebraic systems which satisfy all formulas of the given set. Since we want to use a stronger concept of satisfaction we have to apply hypersubstitutions to formulas. The first step is to define a mapping which maps a relation defined on a set A and an n_j-tuple of operations on A to a relation defined on Oⁿ(A). The operation Rⁿn^j,A with

Rⁿn^j,A : Rel^nj(A) × (Oⁿ(A))^nj → Rel^nj(Oⁿ(A))

by (γ^A_j , f₁^A, . . . , f_n^A_j) 7→ Rⁿn^j,A(γ^A_j , f₁^A, . . . , f_n^A_j) where Rⁿn^j,A(γ^A_j , f₁^A, . . . , f_n^A_j) is true iff for all a₁, . . . , an∈ A we have (f₁^A(a₁, . . . , an),. . . , f_n^A_j(a₁, . . . , an)) ∈ γ^A_j maps each nj-ary relation γ^A_j and each nj-tuple of n-ary operations on A to an n_j-ary relation R^A_γ

j on Oⁿ(A) where (f₁^A, . . . , f_n^A_j) ∈ R_γ^A

j iff for every n-tuple a = (a₁, . . . , an) ∈ A we have (f₁^A(a), . . . , f_n^A_j(a)) ∈ γ^A_j. For the properties of the operations Rⁿn^j,A, n, nj ∈ N⁺ see [2].

The operations Rⁿn^j,Acan especially be applied to the fundamental rela- tions and term operations of the algebraic system A = (A; (f_i^A)_i∈I, (γ^A_j )_j∈J) of type (τ , τ⁰). Then the extension to arbitrary relations of the relation algebra generated by {γ^A_j |j ∈ J} can be defined as follows:

(1) Rn^nj,A(ξρ^A, t^A₁, . . . , t^A_nj) := ξRⁿn^j,A(ρ^A, t^A₁, . . . , t^A_nj), (2) Rn^nj,A(τ ρ^A, t^A₁, . . . , t^A_nj) := τ Rⁿn^j,A(ρ^A, t^A₁, . . . , t^A_nj), (3) Rn^nj,A(4ρ^A, t^A₁, . . . , t^A_nj) := 4Rⁿn^j,A(ρ^A, t^A₁, . . . , t^A_nj),

(4) Rn^nj,A(ρ^A₁◦ρ^A₂, t^A₁,. . . , t^A_nj) := Rn^nj,A(ρ^A₁, t^A₁,. . . , t^A_nj)◦Rn^nj,A(ρ^A₂, t^A₁,. . . , t^A_nj), (5) Rn^3,A δ^{{1; 2,3},A}₃ , t^A₁, t^A₂, t^A₃

:= δ{1; 2,3}, Oⁿ(A)

3 .

Besides formulas of type (τ , τ⁰) we now define formulas of type (τ , τ⁰⁰) intro- ducing to each relation from h{γ^A_j|j ∈ J}i a new relation symbol Rl. This gives an indexed set (R_l)_l∈L of relation symbols where R_l is n_l-ary. Let τ⁰⁰ be the new type of all these relation symbols.

Let F_{(τ ,τ}00)(W_τ(X_n)) be the set of all n-ary formulas of type (τ , τ⁰⁰) and let F_{(τ ,τ}00)(Wτ(X)) := S

n≥1 F_{(τ ,τ00)}(Wτ(Xn)) be the set of all formulas of type (τ , τ⁰⁰). Now we will define the realization of an n-ary formula of type (τ , τ⁰⁰) as a relation defined on Oⁿ(A).

Definition 4.1. Let A = (A; (f_i^A)_i∈I, (γ^A_j )_i∈J) be an algebraic system of type (τ , τ⁰). The realization of a formula F of type (τ , τ⁰⁰) on A is defined as follows :

(i) If F has the form s ≈ t, then (s ≈ t)^A := s^A= t^Awhere s^A, t^Aare the term operations induced by the terms s, t on the algebra (A; (f_i^A)_i∈I).

(ii) If F has the form Rl(t₁, . . . , tnl), then

Rl(t1, . . . , tnl)^A:= Rⁿ_n^l,A(R^A_l , t^A₁, . . . , t^A_nl).

Here R^A_l is an element of the relational algebra generated by {γ^A_j |j ∈ J}

(iii) If the formula has the form ¬F , then (¬F )^A:= ¬F^A (where ¬F^A is true iff F^A is not true).

(iv) If the formula has the form F₁∨ F₂, then (F₁∨ F₂)^A:= F₁^A∨ F₂^A (where F₁^A∨ F₂^A is true iff F₁^A is true or F₂^A is true).

(v) If the formula has the form ∃xi(F ), then (∃xi(F ))^A:= ∃xi(F )^A(where

∃x_i(F )^A is true iff there exists an a_i such that after substituting a_ifor xi the realization F^A becomes true).

Let (F_{(τ ,τ}00)(Wτ(Xn)))^A be the set of all realizations of n-ary formulas of type (τ , τ⁰⁰) and let (W_τ(X_m))^A be the set of all m-ary term operations induced by terms of type τ on the algebra (A; (f_i^A)i∈I) of type τ . Then for all m, n ∈ N⁺ an operation

R˙^n,A_m : (F_{(τ ,τ}00)(Wτ(Xn)))^A× ((Wτ(Xm))^A→ Rel^nj(O^m(A))

is inductively defined in the following way:

Definition 4.2. Let A be an algebraic system of type (τ , τ⁰). For any F^A ∈ (F_{(τ ,τ}00)(Wτ(Xn))^A and any n-tuple of m-ary term operations R˙m^n,A(F^A, t^A₁, . . . , t^A_n) is defined inductively by the following steps :

(i) If F^Ahas the form s^A= t^A, then ˙R^n,Am (s^A= t^A, t^A₁, . . . , t^A_n) := Sm^n,A(s^A, t^A₁, . . . , t^A_n) = S^n,Am (t^A, t^A₁, . . . , t^A_n).

(ii) If F has the form R^A_l (s₁, . . . , s_nl), then ˙R^n,Am (R_l^A(s₁, . . . s_nl)^A, t^A₁, . . . , t^A_n)

= R^A_l (Sm^n,A(s^A₁, t^A₁, . . . , t^A_n), . . . , Sm^n,A(s^A_nl, t^A₁, . . . , t^A_n)).

(iii) If F^A has the form (¬F )^A, then ˙R^n,Am ((¬F )^A, t^A₁, . . . , t^A_n) := ¬ ˙R^n,Am (F^A, t^A₁, . . . , t^A_n).

(iv) If F^A has the form (F₁∨ F₂)^A, then ˙R^n,Am ((F₁∨ F₂)^A, t^A₁, . . . , t^A_n) := ˙R^n,Am (F₁^A, t^A₁, . . . , t^A_n) ∨ ˙R^n,Am (F₂^A, t^A₁, . . . , t^A_n).

(v) If F^A has the form (∃x_i(F ))^A, then ˙R^n,Am ((∃x_i(F ))^A, t^A₁, . . . , t^A_n) := ∃xi( ˙R^n,Am (F^A, t^A₁, . . . , t^A_n)).

The operation ˙R^n,Am , m, n ∈ N⁺satisfies an equation similar to the supperas- sociative identity mentioned in Section 2.

In Section 3 we defined extensions bσ of hypersubstitutions for the al- gebraic system A as mappingsσ : T (A) ∪ R(A) → T (A) ∪ R(A). Now web define another kind of extension of hypersubstitution σ^Awhich is also based on a pair (σF, σR), σF : {f_i^A|i ∈ I} → T (A), σR: {γ^A_j |j ∈ J} → R(A). We need the fact that for any relation symbol Rl corresponding to a relation in R(A) there exists a formula F such that the realization of F gives R^A_l (see [6]).

Definition 4.3. Let σ ∈ Relhyp_A(τ , τ⁰). Then we define a mapping

˙σ^A: (F_{(τ ,τ}00)(Wτ(X)))^A → (F_{(τ ,τ}00)(Wτ(X)))^A inductively as follows :

(i) ˙σ^A[s^A = t^A] :=σb_F[s^A] =bσF[t^A].

(ii) ˙σ^A[R^A_l (t^A₁, ..., t^A_nl)] := Rⁿn^l,A(bσR[R^A_l ],bσF[t^A₁], ...,σbF[t^A_nl]).

Here bσR[R^A_l ] is an element of the relational clone generated by {γ^A_j |j ∈ J}.

(iii) ˙σ^A[¬F^A] := ¬( ˙σ^A[F^A]).

(iv) ˙σ^A[F₁^A∨ F₂^A] := ˙σ^A[F₁^A] ∨ ˙σ^A[F₂^A].

(v) ˙σ^A[∃xi(F^A)] := ∃xi( ˙σ^A[F^A]).

Theorem 4.4. Let σ ∈ Relhyp_A(τ , τ⁰), let m, n ∈ N⁺. Then ˙σ^A is a mapping from ((F_{(τ ,τ}00)(W_τ(X_n))^A)_n≥1 to ((F_{(τ ,τ}00)(W_τ(X_n))^A)_n≥1 with ˙σ^A[ ˙Rm^n,A(F^A, s^A₁, . . . , s^A_n)] = ˙R^n,Am ( ˙σ^A[F^A],σbF[s^A₁], . . . ,σbF[s^A_n]) for all F ∈ F_{(τ ,τ}00)(Wτ(Xn)) and s1, . . . , sn∈ Wτ(Xn).

P roof.We will give a proof by induction on the definition of the realization of formula F^A.

(i) If F^A has the form t^A₁ = t^A₂, then

˙σ^A[ ˙R^n,Am (t^A₁ = t^A₂, s^A₁, . . . , s^A_n)]

= ˙σ^A[Sm^n,A(t^A₁, s^A₁, . . . , s^A_n) = Sm^n,A(t^A₂, s^A₁, . . . , s^A_n)]

= bσ^F[(Sm^n,A(t^A₁, s^A₁, . . . , s^A_n)] =σbF[Sm^n,A(t^A₂, s^A₁, . . . , s^A_n)]

= Sm^n,A(bσF[t^A₁],σb_F[s^A₁], . . . ,bσF[s^A_n]) = Sm^n,A(bσF[t^A₂],σb_F[s^A₁], . . . ,σbF[s^A_n])

= ˙Rm^n,A(bσF[t^A₁] =σbF[t^A₂],bσ_F[s^A₁], . . . ,σbF[s^A_n])

= ˙Rm^n,A( ˙σ^A[t^A₁ = t^A₂],σbF[s^A₁], . . . ,σbF[s^A_n]).

(ii) If F^A has the form R^A_l (t^A₁, . . . , t^A_nl), then

˙σ^A[ ˙R^n,Am (R^A_l (t^A₁, . . . , t^A_nl), s^A₁ . . . , s^A_n)]

= ˙σ^A[R^A_l (Sm^n,A(t^A₁, s^A₁ . . . , s^A_n), . . . , Sm^n,A(t^A_nl, s^A₁, . . . s^A_n))]

= Rⁿm^l,A(bσR[R^A_l ],bσ_F[Sm^n,A(t^A₁, s^A₁, . . . , s^A_n)], . . . ,σb_F[Sm^n,A(t^A_n

l, s^A₁, . . . , s^A_n)])

= Rⁿm^l,A(bσ^R[R^A_l ], Sm^n,A(bσ^F[t^A₁],σbF[s^A₁], . . . ,bσ^F[s^A_n]), . . . , Sm^n,A(bσ^F[t^A_nl],σbF[s^A₁], . . . ,bσF[s^A_n]))

= ˙R^n,Am (Rⁿm^l,A(bσR([R^A_l ],bσF[t^A₁], . . . ,bσF[t^A_nl]),σbF[s^A₁], . . . ,σbF[s^A_n])

by Lemma 4.3

= ˙R^n,Am ( ˙σ^A[R^A_l (t^A₁, . . . , t^A_nl)],bσ_F[s^A₁] . . . ,bσ_F[s^A_n]).

(iii) If F^A has the form ¬F^A and assume that

˙σ^A[ ˙R^n,Am (F^A, s^A₁, . . . , s^A_n)] = ˙Rm^n,A( ˙σ^A[F^A],σb_F[s^A₁], . . . ,bσ_F[s^A_n]), then

˙σ^A[ ˙R^n,Am (¬F^A, s^A₁, . . . , s^A_n)]

= ¬( ˙σ^A[ ˙Rm^n,A(F^A, s^A₁, . . . , s^A_n)])

= ¬( ˙R^n,Am ( ˙σ^A[F^A],bσF[s^A₁], . . . ,bσF[s^A_n]))

= ˙Rm^n,A( ˙σ^A[¬F^A],σbF[s^A₁], . . . ,bσF[s^A_n]).

The inductive steps for F^A= F₁^A∨ F₂^A and F^A = ∃xi(F^A) may be handled similarly.