Checking if a quasiequation is admissible in a finite algebra is a decidable problem, but the naive approach, i.e., checking validity in the corresponding free algebra, is computationally unfeasible. We give an algorithm for obtaining smaller algebras to check admissibility and a range of examples to demonstrate the advantages of this approach. R.K. Rendsvig and S. Katrenko (Eds.): ESSLLI 2012 Student Session Proceedings, CEUR Workshop Proceedings vol.: see http://ceur-ws.org/, 2012, pp. 133-141.
Rules and axioms are the building blocks of a logic. Axioms are the assumptions of the logic, whereas rules are used to derive new facts from previously derived facts. Rules are usually formulated as IF-THEN statements, e.g. “IF x is an integer and x is positive THEN x+1 is a natural number”. More generally, a rule is a set of premises followed by a conclusion. In logic, the premises and the conclusion are formulas. In algebra they are usually equations, as in the cancellation rule “IF x + y = x + z THEN y = z”. Axioms are rules without a premise and can be read as, e.g., “x + y = y + x always holds”. In algebra one often uses Σ to denote a finite set of equations and calles the rule “IF Σ THEN ϕ ≈ ψ”, written Σ ⇒ ϕ ≈ ψ, a quasiequation. A quasiequation Σ ⇒ ϕ ≈ ψ is called valid in the finite algebra A if whenever every equation in Σ is true in A for a specific choice of elements of A for the variables occuring in Σ ∪ {ϕ ≈ ψ}, then also ϕ ≈ ψ is true in A for this choice.
Checking validity in finite algebras (similarly, derivability in finite-valued logics) has
been studied extensively in the literature, and may be considered a “solved problem”
in the sense that there exist both general methods for obtaining proof systems for
checking validity (tableaux, resolution, multisequents, etc.) and standard optimization
techniques for such systems (lemma generation, indexing, etc.) (see, e.g., [
Showing the admissibility of rules can play an important role in establishing completeness results. That means for example, that one proves the admissibility of the cut-rule “IF x = y and y = z THEN x = z” to show that the system can derive the same equations without the cut-rule. Moreover, in some cases adding admissible rules to a system can simplify or speed up reasoning in this system.
✯Supported by Swiss National Science Foundation grant 20002 129507.
Often it is possible to transform logical settings to algebraic settings and vice versa
(see, e.g., [
This paper (based on joint research with my supervisor [
Let us first recall some basics from universal algebra. A language is a set of operation symbols L such that to each operation symbol f ∈ L a nonnegative integer ar(f ) is assigned called the arity of f . An L-algebra A is an ordered pair A = hA, {f1A, . . . , fkA}i such that A is a set, called the universe of A, and each fiA is an operation on A, corresponding to an operation symbol fi ∈ L. We often omit superscripts when describing the operations of an algebra. Let A and B be two algebras of the same language. Then B is a subalgebra of A, written B ≤ A, if B ⊆ A and every operation of B is the restriction of the corresponding operation of A. For {a1, . . . , ak} ⊆ A the smallest subalgebra of A containing {a1, . . . , ak} is denoted by ha1, . . . , aki. We use the letters x, y, z, possibly indexed, to denote variables.
Example 1. Let L = {→, e} be a language with ar(→) = 2 and ar(e) = 0. Define the algebra S4→e = h{−2, −1, 1, 2}, →, ei with the operations x → y = (max{−x, y} x ≤ y min{−x, y} otherwise and e = 1.
The algebra S2→e = h{−1, 1}, →, ei is a subalgebra of S4→e, i.e., S2→e ≤ S4→e. Example 2. Let L consist of one operation symbol ⋆ with arity 1. Then consider the algebra P = h{a, b, c, d}, ⋆i where the unary operation ⋆ is described by the diagram below. The algebra h{a, b, d}, ⋆i is then clearly a subalgebra of P.
P c a b d
The set TmL of L-terms is inductively defined: every variable is an L-term and if ϕ1, . . . , ϕn are L-terms and the operation symbol f ∈ L has arity n, then also f (ϕ1, . . . , ϕn) is an L-term. We denote the term algebra over countably infinitely many variables by TmL (i.e., for each f ∈ L with ar(f ) = n, ϕ1, . . . , ϕn ∈ TmL, f TmL (ϕ1, . . . , ϕn) is just the L-term f (ϕ1, . . . , ϕn)) and let ϕ, ψ stand for arbitrary members of the universe TmL. An L-equation is a pair of L-terms, written ϕ ≈ ψ. If Σ is a finite set of L-equations, we call Σ ⇒ ϕ ≈ ψ an L-quasiequation. As usual, if the language is clear from the context we may omit the prefix L.
Example 3. Terms in the language of Example 1 are, e.g., x, x → x or (x → e) → y whereas terms corresponding to Example 2 have the form ⋆(x) or ⋆(⋆(⋆(y))). The following is a quasiequation in the language of Example 1 {x ≈ y → x, x → e ≈ y} ⇒ x ≈ e.
A homomorphism h between two algebras A and B of the same language L is a map h : A → B between their universes that preserves all the operations, i.e., for all a1, . . . , an ∈ A and every operation f ∈ L with ar(f ) = n, h(f A(a1, . . . , an)) = f B(h(a1), . . . , h(an)). The homomorphism h : A → B is called surjective if for all b ∈ B, there exists an a ∈ A such that h(a) = b. Two algebras A and B are said to be isomorphic, if there exists a surjective homomorphism h : A → B with h(a) 6= h(b) for all a 6= b. The algebra C with the universe C = {h(a) : a ∈ A} ⊆ B and the restrictions of the operations of B to C as operations is called a homomorphic image of A, written C ∈ H(A).
We say that the quasiequation Σ ⇒ ϕ ≈ ψ is valid in A or “holds in A”, written Σ |=A ϕ ≈ ψ, if for every homomorphism h : TmL → A, h(ϕ′) = h(ψ′) for all ϕ′ ≈ ψ′ ∈ Σ implies h(ϕ) = h(ψ).
Example 4. The quasiequation of Example 3 is not valid in S4→e since the homomorphism h : TmL → S4→e with h(x) = −1 and h(y) = 1 satisfies h(x) = h(y → x) and h(x → e) = h(y), but not h(x) = h(e).
We also need the well-known fact (see, e.g., [
Lemma 1. Let A be an algebra and Σ ∪ {ϕ ≈ ψ} a finite set of equations. Then (a) |=A ϕ ≈ ψ implies |=B ϕ ≈ ψ for all B ∈ H(A). (b) Σ |=A ϕ ≈ ψ implies Σ |=B ϕ ≈ ψ for all B ≤ A.
For a nonnegative integer m, let FA(m) denote the free algebra with m generators of the L-algebra A, i.e., the algebra of equivalence classes [ϕ] of L-terms ϕ containing at most m variables x1, . . . , xm such that two terms ϕ and ψ belong to the same class if and only if |=A ϕ ≈ ψ. The free algebra of the algebra A has the same language as A and for L-terms ϕ1, . . . , ϕn and the operation f with ar(f ) = n we have f FA(m)([ϕ1], . . . , [ϕn]) = [f A(ϕ1, . . . , ϕn)].
Lemma 2 ([
Intuitively an L-quasiequation Σ ⇒ ϕ ≈ ψ is admissible in an L-algebra A, if every substitution (i.e., every homomorphism from the term algebra to the term algebra), that makes every equation of Σ hold in A, also makes ϕ ≈ ψ hold in A. More formally, an L-quasiequation Σ ⇒ ϕ ≈ ψ is called admissible in A, if for every homomorphism σ : TmL → TmL: |=A σ(ϕ′) ≈ σ(ψ′) for all ϕ′ ≈ ψ′ ∈ Σ implies |=A σ(ϕ) ≈ σ(ψ).
Quasiequations admissible in the n-element algebra A are, equivalently, quasiequations valid in FA(n).
Lemma 3 ([
If a quasiequation Σ ⇒ ϕ ≈ ψ is valid in an algebra A, then it is also admissible in A. However, the other direction is not true in general. We say that A is structurally complete, if admissibility and validity coincide for A, i.e., Σ ⇒ ϕ ≈ ψ is admissible in A if and only if Σ |=A ϕ ≈ ψ.
Example 5. Consider the two-valued Boolean algebra 2 = h{0, 1}, ∧, ∨, ¬, 1, 0i.
Suppose that a {∧, ∨, ¬, 1, 0}-quasiequation Σ ⇒ ϕ ≈ ψ is not valid in 2, i.e., there exists
a homomorphism h : TmL → 2 such that h(ϕ′) = h(ψ′) for all ϕ′ ≈ ψ′ ∈ Σ and
h(ϕ) 6= h(ψ). Define the homomorphism σ : TmL → TmL by sending each variable x
to 1, if h(x) = 1 and to 0, if h(x) = 0. It follows immediately that |=2 σ(ϕ′) ≈ σ(ψ′)
for all ϕ′ ≈ ψ′ ∈ Σ, but 6|=2 σ(ϕ) ≈ σ(ψ). So Σ ⇒ ϕ ≈ ψ is not admissible in 2, hence
2 is structurally complete.
3 A Procedure to Check Admissibility
To check if a given quasiequation Σ ⇒ ϕ ≈ ψ is admissible in a finite algebra A, it
suffices by Lemma 3 to check whether the quasiequation is valid in the free algebra
FA(|A|), which we know is always finite. The validity of quasiequations in finite algebras
is well studied and decidable (see, e.g., [
Proposition 1. Let A, B be L-algebras such that B is a subalgebra of FA(|A|) and A is a homomorphic image of B. Then Σ ⇒ ϕ ≈ ψ is admissible in A iff Σ |=B ϕ ≈ ψ. Proof. Let Σ ⇒ ϕ ≈ ψ be admissible in A. So Σ |=FA(|A|) ϕ ≈ ψ by Lemma 3 and then Σ |=B ϕ ≈ ψ by Lemma 1. For the other direction suppose that Σ |=B ϕ ≈ ψ and |=A σ(ϕ′) ≈ σ(ψ′) for all ϕ′ ≈ ψ′ ∈ Σ. Then |=FA(n) σ(ϕ′) ≈ σ(ψ′) for all ϕ′ ≈ ψ′ ∈ Σ by Lemma 2 and therefore |=B σ(ϕ′) ≈ σ(ψ′) for all ϕ′ ≈ ψ′ ∈ Σ by Lemma 1. But then |=B σ(ϕ) ≈ σ(ψ) and since A is a homomorphic image of B, |=A σ(ϕ) ≈ σ(ψ) by Lemma 1. ⊓⊔
Note that every subalgebra B of a subalgebra C of the free algebra FA(|A|), i.e.,
B ≤ C ≤ FA(|A|), is a subalgebra of FA(|A|). So since FA(m1) ≤ FA(m2) for all
m1 ≤ m2 (see, e.g., [
We now give some explanation how to implement the first two steps of the procedure. For a given A, we want to find the smallest free algebra FA(m) (m ≤ |A|) such that A is a homomorphic image of FA(m). The idea is to calculate first FA(0) and to check whether A ∈ H(FA(0)). Stop if this is the case, otherwise calculate FA(1) and check whether A ∈ H(FA(1)) and so on.
Suppose that, given a finite algebra A = h{a1, . . . , an}, f1, . . . , fki, we want to calculate the elements of FA(m). Recall that the elements of the free algebra can be seen as equivalence classes of terms. Therefore we need to know all the terms that are definable using the given generators. To decide whether two terms ϕ and ψ are the same, i.e., |=A ϕ ≈ ψ, we would have to check all the possible homomorphisms h : TmL → A. So we simulate the truth table checking by storing the elements by sequences of elements of A.
We represent the m generators of FA(m) by sequences hπi(a¯1), . . . , πi(a¯nm )i where a¯1, . . . , a¯nm are the elements of Am and πi, i = 1, . . . , m the i-th projection-map from Am to A and collect them in a set G. Then we run the function DefinableTerms (see Fig. 1) to get the elements of FA(m), stored as sequences of length nm in the set F .
function DefinableTerms(G, {f1, . . . , fk})
F ← G repeat
F0 ← F for all f ∈ {f1, . . . , fk} do
F ← F ∪ { hf (g1), . . . , f (gar(f))i : g1, . . . , gar(f) ∈ F } end for until F0 == F return F end function Example 6. Suppose that we want to calculate the elements of the free algebra for the algebra P = h{a, b, c, d}, ⋆i defined in Example 2. We certainly need generators for the free algebra since P has no constants, i.e., no nullary operations. So the first step will be to calculate FP(1): our generator is the sequence (a, b, c, d). Running the function DefinableTerms((a, b, c, d), {⋆}) gives us F = {(a, b, c, d), (b, a, b, b), (a, b, a, a)}. It is easy to see that there cannot be a surjective homomorphism from FP(1) to A since A has four elements. So we have to calculate the algebra FP(2) with generators (a, a, a, a, b, b, b, b, c, c, c, c, d, d, d, d) and (a, b, c, d, a, b, c, d, a, b, c, d, a, b, c, d), which will give us a six element algebra that fulfills the requirement of the homomorphism.
The second step of the procedure requires us to calculate subalgebras of the free algebra, increasing in their size. We could, at least theoretically, check A ∈ H(B) for all B ≤ FA(m). But since we are interested in the smallest algebras with this property, we generate the subalgebras by increasing their size and always testing whether they satisfy the property. The principles for the calculation of subalgebras are those of DefinableTerms defined in Fig. 1. Using the generating elements as arguments for the operations, we increase the set of “reached” elements as long as we get new elements.
We first calculate all the one-generated subalgebras of the free algebra FA(m), i.e., hϕi for ϕ ∈ FA(m) and store their sizes |hϕi|. Now we know that the size of the two-generated subalgebra hϕ1, ϕ2i of FA(m) is at least max{|hϕ1i|, |hϕ2i|}. Suppose that k = min{|hϕi| : ϕ ∈ FA(m)}. If there is more than one ϕ ∈ FA(m) with |hϕi| = k, then we generate all the algebras (increasing the number of generators) hϕ1, . . . , ϕri with max{|t1|, . . . , |tr|} ≤ k, again testing if there exists a surjective homomorphism to A and storing their sizes. We then proceed similarly for k′ = min{|hϕi| : ϕ ∈ FA(m), |hϕi| > k}. As soon as we find an algebra B with A ∈ H(B) we have an upper-bound for the size of the algebras to test (note that this upper-bound always exists since it cannot exceed the size of the free algebra FA(m)). However, we then have to continue until we know that every combination of generators will lead to a subalgebra B′ with B ≤ B′.
It is not hard to see that step (i) is sound and terminating since we use the opeorfaAtio.nSso otfhethree agreenaertamtinosgt a|lAg|e|bAr|ma A to calculating new, finite sequences of elements sequences. The soundness of step (ii) is, similar to the previous step, given by the construction of the subalgebras and the used bounds of the cardinalities of the algebras. The algorithm terminates since there are only finitely many subalgebras of the free algebra.
Example 7. Consider the algebra S3→¬ = h{−1, 0, 1}, →, ¬i, where → is defined as in Example 1 and ¬x = −x. Note that an equation of the form ϕ ≈ ϕ → ϕ holds in S3→¬ iff ϕ is a theorem of the {→, ¬}-fragment of the logic RM. Now, following our procedure, we obtain: (i) S3→¬ 6∈ H(FS3→¬ (1)), but S3→¬ ∈ H(FS3→¬ (2)). (ii) FS3→¬ (2) has 264 elements and the smallest subalgebras B ≤ FS3→¬ (2) with S3→¬ ∈
H(B) have 6 elements.
The fact that we first check the smaller subalgebras is useful here: We only had to check the 264 one-generated algebras, 15 two-generated and 3 three-generated algebras rather than all the 5134 possible subalgebras of FS3→¬ (2).
Example 8. Small changes in the universe or language of an algebra can dramatically change the size and structure of its free algebra. Consider the algebra S4→¬e = h{−2, −1, 1, 2}, →, ¬, ei where → and ¬ are defined as in Example 7 and =1. Although this algebra is only slightly different to S4→e and S3→¬ of the Examples¯1 and 7, the appropriate free algebra is much smaller and only needs one generator: (i) S4→¬e 6∈ H(FS4→¬e (0)), but S4→¬e ∈ H(FS4→¬e (1)). (ii) FS4→¬e (1) has 18 elements and the smallest subalgebras B ≤ FS4→¬e (1) with
S4→¬e ∈ H(B) have 6 elements.
Example 9. In some cases, it is possible to establish structural completeness results for the algebra A using the described procedure. The smallest B ≤ FA(m) with A ∈ H(B) may be an isomorphic copy of A itself. In particular, known structural completeness results have been confirmed for L3→ = h{0, 21 , 1}, →Li the 3-element Komori C-algebra B1 = h{0, 12 , 1}, min, max, ¬Gi the 3-element Stone algebra G3 = h{0, 12 , 1}, min, max, →Gi the 3-element positive Go¨del algebra S3→ = h{−1, 0, 1}, →Si the 3-element implicational Sugihara monoid where x →L y = min(1, 1 − x + y), x →G y is y if x > y, otherwise 1, ¬Gx = x →G 0, and →S is the operation → of S3→¬ from Example 7. A new structural completeness result has also been established for the psuedocomplemented distributive lattice B2 obtained by adding a top element to the 4-element Boolean algebra.
Example 10. There are even cases where we do not need any generators for the free algebra since the constants alone suffice. Consider the 5-valued Post algebra P5 = h{0, 1, 2, 3, 4}, ∧, ∨,′ , 0, 1i where h{0, 1, 2, 3, 4}, ∧, ∨i builds a 5-chain with 0 < 4 < 3 < 2 < 1 and 0′ = 1, 1′ = 2, 2′ = 3, 3′ = 4, 4′ = 0. This algebra builds the algebraic counterpart to the Post logic P5. Running our procedure we recognize that P5 is isomorphic to FP5 (0), i.e., P5 is also structurally complete.
Example 11. Consider the algebra D4 = h{⊥, a, b, ⊤}, ∧, ∨, ¬, ⊥, ⊤i, called the 4-element De Morgan algebra, consisting of a distributive bounded lattice with an involutive negation defined as shown below and also its constant-free case called the 4-element De Morgan lattice D4L = h{⊥, a, b, ⊤}, ∧, ∨, ¬i.
a b
b b ⊤ b b ⊥ Following our procedure, we obtain: (i) D4 6∈ H(FD4 (1)) and D4L 6∈ H(FD4L (1)), but D4 ∈ H(FD4 (2)) and D4L ∈ H(FD4L (2)). (ii) FD4 (2) has 168 elements, FD4L (2) has 166 elements and the smallest subalgebras of the free algebras, for which D4 and D4L are homomorphic images, have 10 and 8 elements, respectively.
Example 12. Similar results were also obtained in [
Example 13. Consider the 3-valued Lukasiewicz algebra L3 = h{0, 21 , 1}, →, ¬i with x → y = min(1, 1 − x + y) and ¬x = 1 − x. Following our procedure: (i) L3 6∈ H(FL3 (0)), but L3 ∈ H(FL3 (1)). |A|
Quasivariety Q(A) |Output algebra| L3 B1 C3 L3→
L C3 S3→¬ S3→ G3
L D4 D4
P S4→¬e B2 P5
However, P can be embedded into FP(1) × FP(1); that is, P is structurally complete
(see, e.g., [
This last issue, but also possibilities of improving the given procedure for checking admissibility (e.g., ruling out symmetric cases of generators when calculating a free algebra) will be the subject of future work. The given examples for our procedure are summarized in Table 1.