=Paper=
{{Paper
|id=None
|storemode=property
|title=Checking Admissibility in Finite Algebras
|pdfUrl=https://ceur-ws.org/Vol-954/paper14.pdf
|volume=Vol-954
}}
==Checking Admissibility in Finite Algebras==
https://ceur-ws.org/Vol-954/paper14.pdf
Checking Admissibility in Finite Algebras
Christoph Röthlisberger✯
Mathematics Institute, University of Bern
Sidlerstrasse 5, 3012 Bern, Switzerland
christoph.roethlisberger@math.unibe.ch
Abstract. 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.
1 Introduction
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., [1, 12, 24]).
A rule which can be added to a given system without producing new valid equations is
called admissible. This notion was introduced by Lorenzen in 1955 [18], but the property
of being admissible was already used by Gentzen twenty years earlier [7]. Admissibility
has been studied intensively in the context of intermediate and transitive modal logics
and their algebras [6, 8, 9, 13, 15, 21], leading also to proof systems for checking
admissibility [2, 10, 14], and certain many-valued logics and their algebras [5, 16, 17,
19, 21], but a general theory for this latter case has so far been lacking.
Showing the admissibility of rules can play an important role in establishing com-
pleteness 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.
R.K. Rendsvig and S. Katrenko (Eds.): ESSLLI 2012 Student Session Proceedings, CEUR Work-
shop Proceedings vol.: see http://ceur-ws.org/, 2012, pp. 133–141.
134 Christoph Röthlisberger
Often it is possible to transform logical settings to algebraic settings and vice versa
(see, e.g., [3]). In this sense rules and logics correspond to quasiequations and classes of
algebras satisfying the same quasiequations, respectively. In this work we concentrate
on the question, whether a given quasiequation is admissible in a finite algebra. This
corresponds to the question, whether the quasiequation holds in a corresponding free
algebra on countably infinitely many generators. Although it is well known that admis-
sibility is decidable in finite algebras, the naive approach is computationally unfeasible.
We give an algorithm to answer this question in a more efficient way.
This paper (based on joint research with my supervisor [20]) focuses on proce-
dural aspects of the given problem and its solution. Necessary algebraic definitions
are provided, so that also readers without experience in universal algebra are able to
understand the text.
2 Validity and Admissibility
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 as-
signed 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, corre-
sponding 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 , . . . , ak i. 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 S→e
4 = h{−2, −1, 1, 2}, →, ei with the operations
(
max{−x, y} x ≤ y
x→y= and e = 1.
min{−x, y} otherwise
The algebra S→e
2 = h{−1, 1}, →, ei is a subalgebra of S→e →e
4 , i.e., S2 ≤ S→e
4 .
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 a
b
c 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
Checking Admissibility in Finite Algebras 135
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 S→e
4 since the homomor-
phism h : TmL → S→e4 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., [4]) that taking homomorphic images
and subalgebras preserves equations and quasiequations, respectively.
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 ([21], [4]). Let A be a finite L-algebra and Σ ∪ {ϕ ≈ ψ} a finite set of
L-equations. Then
(a) FA (m) is finite for all m ∈ N.
(b) |=FA (|A|) ϕ ≈ ψ if and only if |=A ϕ ≈ ψ.
(c) Σ |=FA (|A|) ϕ ≈ ψ if and only if Σ |=FA (k) ϕ ≈ ψ, |A| ≤ k ∈ N.
136 Christoph Röthlisberger
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 ([19]). Σ ⇒ ϕ ≈ ψ is admissible in A iff Σ |=FA (|A|) ϕ ≈ ψ.
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. Sup-
pose 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., [1, 12, 24]). However, even free algebras on a
small number of generators can be very large. E.g., the free algebra FS→e 4
(2) has 453
elements, where S→e
4 is the algebra of Example 1. We therefore seek smaller algebras
B such that, as for FA (|A|):
Σ ⇒ ϕ ≈ ψ is admissible in A ⇐⇒ Σ |=B ϕ ≈ ψ.
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., [4]), we possibly do not need |A| generators. This suggests the
following procedure when A is finite:
Checking Admissibility in Finite Algebras 137
(i) Find the smallest free algebra FA (m) such that A ∈ H(FA (m)).
(ii) Compute subalgebras B of FA (m), increasing in their size, and check for each
whether A ∈ H(B).
(iii) Derive a proof system for a smallest B with the properties of (ii).
Steps (i) and (ii) of the procedure have been implemented using macros implemented
for the Algebra Workbench [23]. Step (iii) can be implemented directly making use of
a system such as MUltlog/MUltseq [11, 22].
We now give some explanation how to implement the first two steps of the proce-
dure. 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 , . . . , fk i, 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 (ā1 ), . . . , πi (ānm )i where
ā1 , . . . , ā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
Fig. 1. Algorithm to generate all the definable terms, given a set of generators G
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 func-
tion 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.
138 Christoph Röthlisberger
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 , ϕ2 i of FA (m) is at least max{|hϕ1 i|, |hϕ2 i|}.
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 gener-
ators) hϕ1 , . . . , ϕr i with max{|t1 |, . . . , |tr |} ≤ k, again testing if there exists a sur-
jective 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 op-
erations of the generating algebra A to calculating new, finite sequences of elements
m
of A. So there are at most |A||A| 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 S→¬
3 = h{−1, 0, 1}, →, ¬i, where → is defined as in
Example 1 and ¬x = −x. Note that an equation of the form ϕ ≈ ϕ → ϕ holds in
S→¬
3 iff ϕ is a theorem of the {→, ¬}-fragment of the logic RM. Now, following our
procedure, we obtain:
(i) S→¬
3 6∈ H(FS→¬3
(1)), but S→¬
3 ∈ H(FS→¬
3
(2)).
(ii) FS→¬
3
(2) has 264 elements and the smallest subalgebras B ≤ FS→¬
3
(2) with S→¬
3 ∈
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 FS→¬
3
(2).
Example 8. Small changes in the universe or language of an algebra can dramati-
cally change the size and structure of its free algebra. Consider the algebra S→¬e
4 =
h{−2, −1, 1, 2}, →, ¬, ei where → and ¬ are defined as in Example 7 and =1. Although
¯
this algebra is only slightly different to S→e
4 and S→¬
3 of the Examples 1 and 7, the
appropriate free algebra is much smaller and only needs one generator:
(i) S→¬e
4 6∈ H(FS→¬e
4
(0)), but S→¬e
4 ∈ H(FS→¬e
4
(1)).
(ii) FS→¬e
4
(1) has 18 elements and the smallest subalgebras B ≤ FS→¬e
4
(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
Checking Admissibility in Finite Algebras 139
L→ 1
3 = h{0, 2 , 1}, →L i the 3-element Komori C-algebra
B1 = h{0, 12 , 1}, min, max, ¬G i the 3-element Stone algebra
G3 = h{0, 12 , 1}, min, max, →G i the 3-element positive Gödel algebra
S→
3 = h{−1, 0, 1}, →S i 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, ¬G x = x →G 0,
and →S is the operation → of S→¬ 3 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 DL4 = h{⊥, a, b, ⊤}, ∧, ∨, ¬i.
⊤
b
a b b
b
b
⊥
Following our procedure, we obtain:
(i) D4 6∈ H(FD4 (1)) and DL L
4 6∈ H(FDL (1)), but D4 ∈ H(FD4 (2)) and D4 ∈ H(FDL (2)).
4 4
(ii) FD4 (2) has 168 elements, FDL (2) has 166 elements and the smallest subalgebras
4
of the free algebras, for which D4 and DL
4 are homomorphic images, have 10 and
8 elements, respectively.
Example 12. Similar results were also obtained in [19] for Kleene algebras and lat-
tices generated by the 3-element chains C3 = h{⊤, a, ⊥}, ∧, ∨, ¬, ⊥, ⊤i and CL 3 =
h{⊤, a, ⊥}, ∧, ∨, ¬i where ¬ swaps ⊥ and ⊤ and leaves a fixed. In both cases the small-
est subalgebra of the free algebra, for which C3 and CL
3 are homomorphic images, is a
4-element chain.
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)).
140 Christoph Röthlisberger
A |A| Quasivariety Q(A) |Free algebra| |Output algebra|
L3 3 algebras for L3 (Ex. 13) |FA (1)| = 12 6
B1 3 Stone algebras (Ex. 9) |FA (1)| = 6 3
C3 3 Kleene algebras (Ex. 12) |FA (1)| = 6 4
L→3 3 algebras for L→
3 (Ex. 9) |FA (2)| = 40 3
CL 3 3 Kleene lattices (Ex. 12) |FA (2)| = 82 4
S→¬
3 3 algebras for RM→¬ (Ex. 7) |FA (2)| = 264 6
S→3 3 algebras for RM→ (Ex. 9) |FA (2)| = 60 3
G3 3 algebras for G3 (Ex. 9) |FA (2)| = 18 3
DL 4 4 De Morgan lattices (Ex. 11) |FA (2)| = 166 8
D4 4 De Morgan algebras (Ex. 11) |FA (2)| = 168 10
P 4 Q(P) (Ex. 2) |FA (2)| = 6 6
S→¬e
4 4 Q(S→¬e
4 ) (Ex. 8) |FA (1)| = 18 6
B2 5 Q(B2 ) (Ex. 9) |FA (1)| = 7 5
P5 5 algebras for P5 (Ex. 10) |FA (0)| = 5 5
Table 1. Algebras for checking admissibility
(ii) FL3 (1) has 12 elements and the smallest subalgebras B ≤ FL3 (1) with L3 ∈ H(B)
have 6 elements.
Note that our procedure does not necessarily find the smallest algebra B for check-
ing admissibility in A. I.e., there may be an algebra C with C ≤ B and
Σ ⇒ ϕ ≈ ψ is admissible in A ⇐⇒ Σ |=C ϕ ≈ ψ.
Example 14. Following our procedure for the algebra P defined in Example 2:
(i) P 6∈ H(FP (1)), but P ∈ H(FP (2)).
(ii) FP (2) has 6 elements and the smallest subalgebra B ≤ FP (2) with P ∈ H(B) is
FP (2) itself.
However, P can be embedded into FP (1) × FP (1); that is, P is structurally complete
(see, e.g., [5]). But this means that a quasiequation Σ ⇒ ϕ ≈ ψ is admissible in P iff
Σ ⇒ ϕ ≈ ψ is valid in P.
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.
References
1. M. Baaz, C. G. Fermüller, and G. Salzer. Automated Deduction for Many-Valued
Logics. In Handbook of Automated Reasoning, volume II, chapter 20, pages 1355–
1402. Elsevier Science B.V., 2001.
2. S. Babenyshev, V. Rybakov, R. A. Schmidt, and D. Tishkovsky. A Tableau Method
for Checking Rule Admissibility in S4. In Proceedings of UNIF 2009, volume 262
of ENTCS, pages 17–32, 2010.
Checking Admissibility in Finite Algebras 141
3. W. J. Blok and D. Pigozzi. Algebraizable Logics. Number 396 in Memoirs of the
American Mathematical Society volume 77. American Mathematical Society, 1989.
4. S. Burris and H. P. Sankappanavar. A Course in Universal Algebra, volume 78 of
Graduate Texts in Mathematics. Springer-Verlag, New York, 1981.
5. P. Cintula and G. Metcalfe. Structural Completeness in Fuzzy Logics. Notre Dame
Journal of Formal Logic, 50(2):153–183, 2009.
6. P. Cintula and G. Metcalfe. Admissible Rules in the implication-negation fragment
of intuitionistic logic. Annals of Pure and Applied Logic, 162(10):162–171, 2010.
7. G. Gentzen. Untersuchungen über das Logische Schliessen. Math. Zeitschrift,
39:176–210,405–431, 1935.
8. S. Ghilardi. Unification in Intuitionistic Logic. Journal of Symbolic Logic,
64(2):859–880, 1999.
9. S. Ghilardi. Best Solving Modal Equations. Annals of Pure and Applied Logic,
102(3):184–198, 2000.
10. S. Ghilardi. A resolution/tableaux algorithm for projective approximations in IPC.
Logic Journal of the IGPL, 10(3):227–241, 2002.
11. A. J. Gil and G. Salzer. Homepage of MUltseq. http://www.logic.at/multseq.
12. R. Hähnle. Automated Deduction in Multiple-Valued Logics. OUP, 1993.
13. R. Iemhoff. On the Admissible Rules of Intuitionistic Propositional Logic. Journal
of Symbolic Logic, 66(1):281–294, 2001.
14. R. Iemhoff and G. Metcalfe. Proof Theory for Admissible Rules. Annals of Pure
and Applied Logic, 159(1–2):171–186, 2009.
15. E. Jeřábek. Admissible Rules of Modal Logics. Journal of Logic and Computation,
15:411–431, 2005.
16. E. Jeřábek. Admissible rules of Lukasiewicz logic. Journal of Logic and Computa-
tion, 20(2):425–447, 2010.
17. E. Jeřábek. Bases of admissible rules of Lukasiewicz logic. Journal of Logic and
Computation, 20(6):1149–1163, 2010.
18. P. Lorenzen. Einführung in die operative Logik und Mathematik, volume 78 of
Grundlehren der mathematischen Wissenschaften. Springer, 1955.
19. G. Metcalfe and C. Röthlisberger. Admissibility in De Morgan algebras. Soft
Computing, to appear.
20. G. Metcalfe and C. Röthlisberger. Unifiability and Admissibility in Finite Algebras.
In Proceedings of CiE 2012, volume 7318 of LNCS, pages 485–495. Springer, 2012.
21. V.V. Rybakov. Admissibility of Logical Inference Rules, volume 136 of Studies in
Logic and the Foundations of Mathematics. Elsevier, Amsterdam, 1997.
22. G. Salzer. Homepage of MUltlog. http://www.logic.at/multlog.
23. M. Sprenger. Algebra Workbench. http://www.algebraworkbench.net.
24. R. Zach. Proof theory of finite-valued logics. Master’s thesis, Technische Univer-
sität Wien, 1993.