On Löb algebras

Math. Log. Quart. 52, No. 1, 95 – 105 (2006) / DOI 10.1002/malq.200510016

On L¨ob algebras Majid Alizadeh∗1 and Mohammad Ardeshir∗∗2 1 2

Institute for Studies in Theoretical Physics and Mathematics (IPM), P.O. Box 19395-5746, Tehran, Iran Department of Mathematics, Sharif University of Technology, P.O. Box 11365-9415, Tehran, Iran

Received 9 February 2005, revised 4 September 2005, accepted 6 September 2005 Published online 2 January 2006 Key words Basic propositional logic, formal propositional logic, basic algebra, L¨ob algebra, Heyting algebra. MSC (2000) 03G25, 03D20, 03B20 We study the variety of L¨ob algebras, the algebraic structures associated with formal propositional calculus. Among other things, we prove a completeness theorem for formal propositional logic with respect to the variety of L¨ob algebras. We show that the variety of L¨ob algebras has the weak amalgamation property. Some interesting subclasses of the variety of L¨ob algebras, e. g. linear, faithful and strongly linear L¨ob algebras are introduced. c 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim


1 Introduction Formal propositional logic, FPC, is the propositional logic of the provability logic or the G¨odel-L¨ob logic founded by A. Visser in [7]. FPC is an extension of a weaker logic, Basic propositional logic, BPC, augmented by the L¨ob axiom schema, (
→ A) → A ⇒
→ A. It is worth mentioning that intuitionistic propositional logic, IPC, is obtained from BPC by adding a variant of the modus ponens, i. e.
→ A ⇒ A. The associated algebraic structure with BPC, so called Basic algebra, is introduced in [3] and is studied in [1, 2]. In this paper we study the variety of L¨ob algebras, a subvariety of the variety of Basic algebras. For axiomatizations of BPC, FPC and their elementary properties we refer the reader to [4]. We use sequent notation for axiomatization of BPC and FPC. A sequent is an expression of the form A ⇒ B, where A and B are formulas in the language L = {∧, ∨, →,
, ⊥}. Let us denote derivations in BPC and FPC by b and f , respectively.

2 L¨ob algebras To define the variety of L¨ob algebras, we first recall the definition of the variety of Basic algebras and some of its elementary facts which will be needed in the sequel of this paper. See [1, 2, 3, 4] for more details. Definition 2.1 A Basic algebra M = M, ∧, ∨, →, 0, 1 is a structure with constants 0 and 1, and binary functions ∧, ∨, and →, such that 1. with respect to 0, 1, ∧, and ∨ we have a distributive lattice with top and bottom; 2. for → we have the additional equations a → (b ∧ c) = (a → b) ∧ (a → c), (b ∨ c) → a = (b → a) ∧ (c → a), a ≤ (1 → a), (a → b) ∧ (b → c) ≤ (a → c).

a → a = 1,

The relation ≤ is expressible in term of equations with ∧ or ∨ in the standard way, i. e. a≤b ∗ ∗∗

iff a ∧ b = a

iff a ∨ b = b.

e-mail: [email protected] Corresponding author: e-mail: [email protected]

c 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim


96

M. Alizadeh and M. Ardeshir: On L¨ob algebras

So the class of all Basic algebras is a variety. Ba is an abbreviation for “Basic algebra”, and we denote the variety of all Basic algebras by B. Recall that a Heyting algebra (Ha) is a distributive lattice with constants 0 and 1, and a binary relation →, which satisfies a≤b→c

iff

a ∧ b ≤ c.

The item 4. of the following proposition shows that in a Ba we have one direction of the above biconditional. Proposition 2.2 Let M be a Basic algebra. Then for a, b, c ∈ M , 1. if a ≤ b, then c → a ≤ c → b; 2. if a ≤ b, then b → c ≤ a → c; 3. if a ≤ b, then a → b = 1; 4. if a ∧ b ≤ c, then a ≤ b → c; 5. a ∧ (a → b) = a ∧ (1 → b). P r o o f. See [1]. Note that every Ha is a Ba, so the variety H of all Heyting algebras is a subvariety of B. As a trivial example of a Ba which is not a Ha, take M = {0, 1} with the usual definition of ∨, ∧, and a → b = 1 for all a, b ∈ M . Then M = M, ∨, ∧, →, 0, 1 is a Ba, but is not a Ha, since 1 → 0 = 1 = 0. The following proposition shows a tight relation between Ba’s and Ha’s: Proposition 2.3 Let M be a Basic algebra. Then M is a Heyting algebra iff for every a ∈ M , 1 → a = a. P r o o f. See [1]. Now we define: Definition 2.4 A Basic algebra M = M, ∧, ∨, →, 0, 1 is called a L¨ob algebra (La) iff for all x ∈ M , (1 → x) → x = 1 → x. From the above definition it is immediate that the class L of all L¨ob algebras is a subvariety of B. We know that FPC ∪ IPC is inconsistent [4]. In algebraic terms it means that a non-degenerate L¨ob algebra is not a Heyting algebra and vice versa. We note that for every L¨ob algebra M and any element x ∈ M , if x = 1, then x = 1 → x. The concept of an algebraic model for FPC is defined in the usual way and we have: Theorem 2.5 (Soundness and completeness) For all sequent theories T over FPC and sequents s, T f s iff T
s. P r o o f. For the soundness we must verify that all the axioms and rules of FPC are satisfied in any L¨ob algebra. We only consider the L¨ob rule. Let M , I be a model of T , and let a = I(A), b = I(B). By induction, a ∧ (1 → b) ≤ b. Then a ≤ (1 → b) → b = 1 → b, so a ≤ 1 → b. Then a ≤ a ∧ (1 → b) ≤ b, thus a ≤ b. For the completeness, suppose T
A ⇒ B. For every formula A of the language, define [A]T = {B : T f A ⇔ B}. The associated Lindenbaum algebra is a L¨ob algebra UT . Set I(A) = [A]T . Then UT , I
T . So UT , I
A ⇒ B, and then I(A) ≤ I(B). Thus I(A) ∧ I(B) = I(A). So T f A ∧ B ⇔ B. That means T f A ⇒ B.

c 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim


www.mlq-journal.org

Math. Log. Quart. 52, No. 1 (2006)

97

Proposition 2.6 Let M be a L¨ob algebra, then for all x, y ∈ M we have (x → y) → y = 1 → y. P r o o f. We have 1 → y ≤ (x → y) → y. On the other hand, since 1 → y ≤ x → y, then (x → y) → y ≤ (1 → y) → y = 1 → y. Then the result holds. Combining the above proposition and Theorem 2.5 shows that the sequent (A → B) → B ⇒
→ B is derivable in FPC. Let M be a Basic algebra. We define the Heyting part of M by H(M ) = {x ∈ M : 1 → x = x}. Proposition 2.7 Let M be a Basic algebra and x ∈ M . Then x ∈ H(M ) iff there is an element y ∈ M such that x = ((1 → y) → y) → (1 → y). P r o o f. If x ∈ H(M ), then ((1 → x) → x) → (1 → x) = x. For the converse, it is enough to show that for every x ∈ M , ((1 → x) → x) → (1 → x) ∈ H(M ). We have ((1 → x) → x) ∧ (((1 → x) → x) → (1 → x)) = ((1 → x) → x) ∧ (1 → (1 → x)) ≤ 1 → x. Since for all elements a, b ∈ M we have a ∧ (a → b) = a ∧ (1 → b), and since 1 → x is equal or less than the left hand of the above inequality, we will have ((1 → x) → x) ∧ (((1 → x) → x) → (1 → x)) = 1 → x. So ((1 → x) → x) → [((1 → x) → x) ∧ (((1 → x) → x) → (1 → x))] = ((1 → x) → x) → (1 → x). Then ((1 → x) → x) → [((1 → x) → x) → (1 → x)] ≤ ((1 → x) → x) → (1 → x). Note that for above inequality, we used the property a → b ∧ c = (a → b) ∧ (a → c). Then 1 → (((1 → x) → x) → (1 → x)) ≤ ((1 → x) → x) → (1 → x). On the other hand we know that ((1 → x) → x) → (1 → x) ≤ 1 → ((1 → x) → x) → (1 → x). Then ((1 → x) → x) → (1 → x) ∈ H(M ). The following proposition shows a tight relation between Ba’s and La’s: Proposition 2.8 Let M be a Basic algebra such that for every element x in M we have 1 → x = x iff x = 1. Then M is a L¨ob algebra. Moreover in every L¨ob algebra M and for a ∈ M , if a = 1 → a, then a = 1. P r o o f. By Proposition 2.7, for every element x in M we have 1 → [((1 → x) → x) → (1 → x)] = ((1 → x) → x) → (1 → x). Then ((1 → x) → x) → (1 → x) = 1. So (1 → x) → x ≤ 1 → (1 → x). On the other hand we know that (1 → (1 → x)) ∧ ((1 → x) → x) = 1 → x. Then (1 → x) → x = 1 → x. So M is a L¨ob algebra. Let a ∈ M and a = 1 → a. Then (1 → a) → a = (1 → a) → (1 → a) = 1, so 1 → a = 1. Then a = 1. www.mlq-journal.org

c 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim


98

M. Alizadeh and M. Ardeshir: On L¨ob algebras

Let M be a Basic algebra and a ∈ M . We define an , for every natural number n, by a0 = a,

an+1 = 1 → an .

The following is an algebraic version of [4, Proposition 5.20]: Lemma 2.9 Let M be a Basic algebra. Then for a, b ∈ M , and for all m, n ≥ 0, 1. 1 → (a → b) ≤ (1 → a) → (1 → b), 2. am+1 → a = (1 → a) → a, 3. (1 → a) → a ≤ am → an , 4. 1 → a ≤ (1 → a) → a, 5. am+1 ∧ ((1 → a) → a) = 1 → a, 6. am+2 → ((1 → a) → a) = a2 → (1 → a), 7. (am+1 → am ) → a = 1 → a, 8. ((1 → a) → a) → am+1 = ((1 → a) → a) → (1 → a). P r o o f. Translate [4, proof of Proposition 5.20] into algebraic terms. Corollary 2.10 Let M be a Basic algebra, then it is a L¨ob algebra iff for all a, b ∈ M , if a ∧ (1 → b) ≤ b, then a ≤ b. P r o o f. By item 5. of the above lemma, a2 ∧ ((1 → a) → a) = 1 → a. Then (1 → a) → a ≤ 1 → a, i. e. M is a L¨ob algebra. For the other direction, suppose M is a L¨ob algebra and there exist a, b ∈ M such that a ∧ (1 → b) ≤ b. Then a ≤ ((1 → b) → b), and so a ≤ 1 → b. Then a ≤ a ∧ (1 → b). Therefore a ≤ b. The L¨ob algebra generated by {0, 1} can be characterized as follows: Theorem 2.11 The L¨ob algebra generated by 0 and 1 is a chain: q p p p q

1 0n+1

q p p p q

0n

q

01

q

0

02

.

P r o o f. We show that the only elements of the algebra are the 0n , for n ∈ ω, and since 0n ≤ 0n+1 , then it is a chain. By Lemma 2.9, 0n+1 → 0 = (1 → 0) → 0 = 1 → 0. Let a = 1 → 0. Then ak → a2 = a3 , . . . , ak → ak−1 = ak , for k ≥ 2. Generally, for k ≥ m + 1, we have ak → am = am+1 . That means → does not generate any other elements except the elements of the form 0n . c 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim


www.mlq-journal.org

Math. Log. Quart. 52, No. 1 (2006)

99

3 Weak amalgamation property It is shown in [2] that the variety B has the amalgamation property. To show the amalgamation property for the variety of B, we used a property of Basic algebras, which says that for every Basic algebra M , the so called Stone algebra of M , st(K M), is also a Basic algebra. Here we will show that for a Noetherian L¨ob algebra M , its Stone algebra is also a L¨ob algebra. Then we will show that the variety L of L¨ob algebras has the weak amalgamation property, which will be defined later in this section. First we need some general notions on L¨ob algebras, which are similar to the same notions defined for Basic algebras, see [3] or [1]. Recall that a filter F on a Basic algebra M is called proper if F = M . A proper filter F is called prime if a ∨ b ∈ F implies that a ∈ F or b ∈ F . For two filters F and F  on M , define F ≺ F  iff b ∈ F  whenever a → b ∈ F and a ∈ F  . It is easy to see that this relation ≺ is a transitive relation on the set of all filters on M . A filter F is called reflexive iff F ≺ F . Similarly, we may define the notion of a (proper) ideal on an La. Then a proper ideal I on M is called prime if a ∧ b ∈ I implies that a ∈ I or b ∈ I. We note that a nonempty subset F of M is a (prime) filter on M iff M − F is a (prime) ideal on M . Lemma 3.1 Let F be a filter on a Basic algebra M , then 1.
−1 F = {a : 1 → a ∈ F } is a filter and F ≺
−1 F ; 2. for every filter G, if F ≺ G, then
−1 F ⊆ G. P r o o f. See [2]. Lemma 3.2 Let F be a filter on a Basic algebra M such that a → b ∈ F . Then there is a prime filter F  on M such that F ≺ F  , a ∈ F  and b ∈ F  . P r o o f. See, e. g., [3] or [6]. Lemma 3.3 Let M be a Basic algebra, a, b ∈ M such that a ≤ b. Then there is a prime filter F on M such that a ∈ F and b ∈ F . P r o o f. See, e. g., [5]. Proposition 3.4 A Basic algebra M is a Heyting algebra iff all its prime filters are reflexive. P r o o f. We know that every filter in a Heyting algebra is reflexive. For the converse, by Proposition 2.3, it is enough to show that for every element x ∈ M , 1 → x = x. Suppose there is an element x ∈ M such that 1 → x ≤ x. Then there is a prime filter F such that 1 → x ∈ F and x ∈ F . This contradicts to the reflexivity of F . By a Kripke frame K = K, ≺ we mean a nonempty set K equipped with a transitive relation ≺. A subset X ⊆ K is called an open subset of K, ≺ iff for all k, k  ∈ K, if k ∈ X and k ≤ k  , then k  ∈ X. Let mK be the set of all open subsets of K, ≺ . The structure mK = mK, ∩, ∪, →, ∅, K is a Ba [1], where X → Y = {k ∈ K : for all k   k, if k  ∈ X, then k  ∈ Y }. Let us call mK = mK, ∩, ∪, →, ∅, K , with tolerance, the Stone algebra of the Kripke frame K. Now let M be an La and let K M = K, ≺ be the frame of all prime filters on M . Then the Stone algebra of K M is also a Ba, and we denote it by st(K M) to indicate that it comes from a L¨ob algebra M . We call st(K M) the Stone algebra of M . Proposition 3.5 Let a mapping f from K = K, ≺ onto K  = K  , ≺ satisfy the following conditions (such a mapping is called a p-morphism): 1. If a ≺ b, then f (a) ≺ f (b). 2. If f (a) ≺ f (b), then there is c ∈ K such that f (b) = f (c) and a ≺ c. Then mK
can be embedded into mK. P r o o f. It is easy to see that the pre-image of any open subset Y ⊆ K  is open and the image of any open subset X ⊆ K is open, i. e. f is a continuous and open mapping of K onto K  . Now define a mapping h from mK
into mK by h(Y ) = f −1 (Y ). Then h is an embedding.

www.mlq-journal.org

c 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim


100

M. Alizadeh and M. Ardeshir: On L¨ob algebras

Proposition 3.6 Let N be a subalgebra of a Basic algebra M . Then there exists a p-morphism f from K M onto K N. P r o o f. For a prime filter F on M , we set f (F ) = F ∩ N . Obviously, f (F ) is a prime filter on N , and if F1 ≺ F2 , then f (F1 ) ≺ f (F2 ). We prove that f satisfies condition 2. of Proposition 3.5. Let F1 ∩ N ≺ F2 ∩ N and define Σ = {F : F is a filter on M , F  F1 and F ∩ N = F2 ∩ N }. Let F  = [
−1 F1 ∪ (F2 ∩ N )), the filter generated by the set
−1 F1 ∪ (F2 ∩ N ). We show that F  ∈ Σ, i. e. Σ is nonempty. To show that F  is a proper filter, suppose x ∧ y = 0 for some x ∈
−1 F1 and y ∈ F2 ∩ N . Then 1 → x ∈ F1 and note that y → 0 ∈ N . Thus 1 → x ≤ (y → x) ∧ (y → y) = y → (x ∧ y) = y → 0 ∈ F1 . Hence y → 0 ∈ F1 ∩ N ≺ F2 ∩ N . Then 0 ∈ F2 ∩ N , which is a contradiction. So F  is a proper filter. Note that F2 ∩ N ⊆ F  ∩ N . We show that, conversely, F  ∩ N ⊆ F2 ∩ N . Let z ∈ F  ∩ N . Then z ≥ x ∧ y, for some x ∈
−1 F1 and y ∈ F2 ∩ N . Then 1 → x ∈ F1 and also y → z ∈ N . Then 1 → x ≤ (y → x) ∧ (y → y) = y → (x ∧ y) ≤ y → z ∈ F1 . So y → z ∈ F1 ∩ N ≺ F2 ∩ N . Then z ∈ F2 ∩ N . Therefore F  ∩ N = F2 ∩ N . It is easy to verify that the union of chains of elements of Σ belongs to Σ. Then, by Zorn’s lemma, there exists in Σ a maximal element F . It remains to show that F is a prime filter on M . Let x ∨ y ∈ F , x ∈ F , y ∈ F . Set Fx = [F ∪ {x}) and Fy = [F ∪ {y}). Assume that Fx ∩ N ⊆ F2 ∩ N and Fy ∩ N ⊆ F2 ∩ N . Then u ∈ F2 ∩ N , v ∈ F2 ∩ N for some u ∈ Fx ∩ N and v ∈ Fy ∩ N . So u ∨ v ∈ F2 . On the other hand, u ∧ x ≤ u ≤ u ∨ v, v  ∧ y ≤ v ≤ u ∨ v for some u , v  ∈ F . Then (u ∧ v  ) ∧ (x ∨ y) ≤ u ∨ v and so u ∨ v ∈ F . Since u ∨ v ∈ N , we obtain a contradiction with F ∩ N = F2 ∩ N . Then Fx ∩ N = F2 ∩ N or Fy ∩ N = F2 ∩ N , i. e. at least one of the filters Fx and Fy belongs to Σ, contradicting the maximality of F . Consequently, F is a prime filter on M . Then f (F ) = f (F2 ) and F1 ≺ F . A Basic algebra M is called an irreflexive Basic algebra if all prime filters of M are irreflexive. A Basic algebra M is called a Noetherian Basic algebra if it is irreflexive and there is no infinite ascending chain (with respect to the relation ≺) of prime filters. We have the following relation between Ba’s and La’s: Proposition 3.7 Every Noetherian Basic algebra is a L¨ob algebra. P r o o f. Suppose not. Then there is an element x ∈ M such that (1 → x) → x = 1 → x. Then there is a prime filter F such that (1 → x) → x ∈ F and 1 → x ∈ F . So there is a prime filter F1 such that F ≺ F1 and x ∈ F1 . From (1 → x) → x ∈ F and F ≺ F1 we conclude that 1 → x ∈ F1 . By applying the same argument, we will have an infinite ascending chain of prime filters F ≺ F1 ≺ F2 ≺ · · · . Contradiction. On the other hand, we have: Proposition 3.8 Every finite L¨ob algebra is irreflexive. P r o o f. Let F be a reflexive proper filter on the finite L¨ob algebra M . Then, since M is finite, there is n ∈ ω such that 0n+1 = 0n . By Proposition 2.8, 0n = 1 ∈ F . Then 0 ∈ F , since F is reflexive. Contradiction. Proposition 3.9 Let M be a Noetherian L¨ob algebra. Then its Stone algebra st(K M) is also a L¨ob algebra. P r o o f. Suppose not and let X be an element of M K such that (1 → X) → X = 1 → X. Then there is a prime filter F on M such that F ∈ (1 → X) → X and F ∈ 1 → X. So there is a prime filter F  on M such that F ≺ F  and F  ∈ X. Note that F = F  , since M is irreflexive. We also have F  ∈ 1 → X, otherwise F ≺ F  and F ∈ (1 → X) → X imply F  ∈ X. The same argument can be applied to F  and then we get an infinite ascending chain of prime filters. c 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim


www.mlq-journal.org

Math. Log. Quart. 52, No. 1 (2006)

101

Corollary 3.10 Let M be a finite L¨ob algebra. Then its Stone algebra st(K M) is also a finite L¨ob algebra. Corollary 3.11 Let K be a finite irreflexive Kripke frame. Then its Stone algebra mK is also a finite L¨ob algebra. By the usual correspondence between interpretations on a L¨ob algebra M and the associated forcing relations on the Kripke frames of all prime filters on M , we have: Theorem 3.12 Let K = K, ≺ be a finite irreflexive Kripke frame and mK be the L¨ob algebra of its open subsets. Then there is a one-to-one correspondence between interpretations in mK and forcing relations on K given by: (i) If I is an interpretation on mK, define I by k I p iff k ∈ I(p), for atomic p. (ii) If  is a forcing relation on K, define I
by I
(p) = {k : k  p}, for atomic p. Furthermore, relations (i) and (ii) extend to all formulas. Proposition 3.13 A sequent A ⇒ B is valid in a finite irreflexive Kripke frame K iff it is valid in mK. Theorem 3.14 FPC is complete with respect to the class of all finite L¨ob algebras. P r o o f. Combine Proposition 3.13 with Visser’s result on the completeness of FPC with respect to the class of all finite irreflexive Kripke models [7]. In the sequel of this section we want to show that the variety L of L¨ob algebras has the weak amalgamation property. We need some notations and definitions. Definition 3.15 Let D be a class of algebras. We say that the class D is amalgamable if for any algebras M 0 , M 1 , M 2 ∈ D and embeddings f1 : M 0 −→ M 1 and f2 : M 0 −→ M 2 , there exist an algebra M ∈ D and embeddings g1 : M 1 −→ M and g2 : M 2 −→ M such that g1 ◦ f1 = g2 ◦ f2 . If D is amalgamable, we say that D has the amalgamation property (AP). D is said to have the weak amalgamation property if AP is satisfied for all finite M 0 , M 1 , M 2 ∈ D. Without loss of generality we may assume that M 0 is a subalgebra of M 1 and M 2 . Theorem 3.16 The variety L has the weak amalgamation property. P r o o f. Suppose M 0 is a subalgebra of both finite L¨ob algebras M 1 and M 2 . By Proposition 3.6, there are onto mappings fi : K Mi −→ K M0 defined by fi (F ) = F ∩ M0 , for i ∈ {1, 2}, satisfying the conditions of Proposition 3.5. Put W = {F1 , F2 : F1 is a prime filter on M 1 , F2 is a prime filter on M 2 , and F1 ∩ M0 = F2 ∩ M0 }. Define F1 , F2 ≺ F1 , F2 iff F1 ≺ F1 and F2 ≺ F2 , for F1 , F2 , F1 , F2 ∈ W . Clearly, the relation ≺ on W is transitive, so we may view W = W, ≺ as a Kripke frame. Note that W is finite and irreflexive. Then by Corollary 3.11, mW is a finite L¨ob algebra. For i ∈ {1, 2}, the map gi : M i −→ mW defined by gi (b) = {F1 , F2 ∈ W : b ∈ Fi } is an embedding. For every element x ∈ M0 we have g1 (x) = g2 (x). We want to show that each gi is one-to-one. We first note that since f2 is onto, for every prime filter F1 on M 1 there is a prime filter F2 on M 2 such that (F1 , F2 ) ∈ W . A similar statement holds for f2 , f1 . Now to see that, for example, g1 is one-to-one, let a, b ∈ M1 such that a = b. Then either a ≤ b or b ≤ a. Suppose a ≤ b. Then there is a prime filter F on M 1 such that a ∈ F and b ∈ F . By the above fact, there exists a prime filter F  on M 2 such that F, F  ∈ W . Then F, F  ∈ g1 (a) and F, F  ∈ g1 (b). So g1 (a) = g1 (b). Now we show that, for example, g1 is a homomorphism. Assume that 1. F1 , F2 ∈ W , 2. x, y ∈ M1 , 3. F1 , F2 ∈ g1 (x → y), 4. F1 , F2 ∈ W , 5. F1 , F2 ≺ F1 , F2 , 6. F1 , F2 ∈ g1 (x). www.mlq-journal.org

c 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim


102

M. Alizadeh and M. Ardeshir: On L¨ob algebras

Then x ∈ F1 , and since F1 ≺ F1 , we will have y ∈ F1 . So F1 , F2 ∈ g1 (y). That means F1 , F2 ∈ g1 (x) → g1 (y). Similarly, we will have g1 (x) → g1 (y) ⊆ g1 (x → y). To show that g1 preserves ∧ and ∨ is almost immediate. Passing through it is worth mentioning that the argument of Theorem 3.16 works if one of the L¨ob algebras {M 1 , M 2 } is Noetherian and the other one arbitrary. So for a negative answer to the following question, we should look at two non-Noetherian L¨ob algebras. Question 3.17 Does the variety L have the amalgamation property?

4 Faithful, linear and strongly linear L¨ob algebras In this section we study some special subclasses of L, called faithful L¨ob algebras, linear L¨ob algebras, faithful linear L¨ob algebras, etc. First let us recall from [4]: Definition 4.1 A set of sequents Γ is called faithful over BPC if Γ b (A1 → B1 ) ∧ · · · ∧ (An → Bn ) ⇒ A → B implies Γ ∪ {(A1 ⇒ B1 ) ∧ · · · ∧ (An ⇒ Bn )} b (A ⇒ B). It turns out that BPC is faithful, and IPC and FPC are interesting faithful extensions of BPC, see [4]. For the algebraic counterpart of faithfulness, we define: Definition 4.2 A L¨ob algebra (resp. Basic algebra) M is a faithful L¨ob algebra (fLa) (resp. faithful Basic algebra (fBa)) iff for all a, b ∈ M , if (1 → a) → (1 → b) = 1, then a ≤ b. It is easy to see that every faithful L¨ob algebra M is infinite. Otherwise, for the element 0 ∈ M we must have 0n = 0n+1 , for some n ∈ ω. Then 0n+1 = 1, and so by faithfulness, 0 = 1, a contradiction. By the same argument, we conclude that there does not exist any finite chain of elements in any fLa. It is shown in [2]: Theorem 4.3 Let Γ be a sequent theory over BPC. Then Γ is a faithful theory iff its Lindenbaum algebra is a faithful Basic algebra. Using the fact that FPC is a faithful sequent theory (by [4, Theorem 3.14]) and by the above theorem, we may conclude that the Lindenbaum algebra U of FPC is a faithful L¨ob algebra. So we have: Theorem 4.4 FPC is complete with respect to the class of all faithful L¨ob algebras. P r o o f. Apply Theorem 4.3. Let us introduce an extension of FPC by FPC = FPC+(A → B)∨(B → A). We show that the logic FPC is sound and complete with respect to the class of all linear L¨ob algebras. Definition 4.5 An La is a L¨ob algebra in which (x → y) ∨ (y → x) = 1 holds for all x, y. Definition 4.6 A chain is a linear L¨ob algebra, i. e. such that x ≤ y or y ≤ x for all x, y. Clearly every chain is an La. As usual, the elements of the Lindenbaum algebra of FPC are the equivalence classes of formulas in the language of FPC, |A| = {B : FPC  A ⇔ B}. It is easy to verify that the Lindenbaum algebra U of FPC is an La. Then by the canonical interpretation, we have: Theorem 4.7 (Soundness and completeness) For all theories T and sequents s, T f s iff T
s. We want to show that FPC is complete with respect to the class of all faithful linear L¨ob algebras. To do that, it is sufficient to show that FPC is a faithful theory. Given a Kripke model K with root k, let K  be the model built up from K by adding a new root node k0 ≺ k which is reflexive exactly when k is, and such that k0
p exactly when k
p. c 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim


www.mlq-journal.org

Math. Log. Quart. 52, No. 1 (2006)

103

Theorem 4.8 FPC is faithful. P r o o f. Let K be a rooted Kripke model of FPC with root k. By [4, Proposition 3.11], it is enough to show that K  is a model of FPC. Let k0 be the root of K  . Suppose k0
(A → B) ∨ (B → A). Then k0
A → B and k0
B → A. So there are k1 , k2  k0 such that k1  A, k1
B, k2  B and k2
A. Since K is a model of FPC, it is not the case that both k1 , k2  k. On the other hand, if one of k1 or k2 , say k1 , is k, then k1  k2 . This contradicts to k1  A and k2
A. So K  is a model of FPC. By Theorems 4.3 and 4.8, the Lindenbaum algebra of FPC is a faithful L¨ob algebra. So we have: Theorem 4.9 FPC is complete with respect to the class of all faithful linear L¨ob algebras. Let M be an La and F be a filter on M . For any a, b ∈ M , we shall write a ≤F b iff a → b ∈ F . The relation ≤F is a quasi-ordering on M . Write a ∼F b iff (a → b) ∧ (b → a) ∈ F . It is easy to check that ∼F is a congruence relation on M . So we can consider the quotient algebra M /F . Lemma 4.10 Let F be a proper filter on an La M , then F is a prime filter iff M /F is a chain. P r o o f. This is routine. Lemma 4.11 Let M be a faithful L¨ob algebra and F be the unit filter on M , i. e. F = {1}. Then M /F  M . P r o o f. This is easy. Theorem 4.12 If M is a faithful linear L¨ob algebra, then it is a subalgebra of a direct product of chains. P r o o f. Use Lemmas 4.10 and 3.3. Since the Lindenbaum algebra U of FPC is faithful, then for F = {1}, U/F  U, and also U is a subalgebra of a direct product of chains. So we have: Theorem 4.13 For any sequent A ⇒ B, the following are equivalent: 1. FPC  A ⇒ B. 2. For every La M , M
A ⇒ B. 3. For every chain M , M
A ⇒ B. 4. U
A ⇒ B. It is easily verified that in any Heyting algebra, the usual linearity axiom (a → b) ∨ (b → a) = 1 is equivalent to the axiom (a → b) ∨ ((a → b) → b) = 1. In the following example we present a chain which does not satisfy the latter one. Example 4.14 Let M = {0, x, y, 1}, where 0 < x < y < 1, and ∨ and ∧ are defined as usual. Define → by the following table: → 0 x y 1

0 1 y y y

x 1 1 y y

y 1 1 1 y

1 1 1 1 1 .

M = M, ∧, ∨, →, 0, 1 is a chain, but (x → 0) ∨ ((x → 0) → x) = y. By the above example and Theorem 4.13 we have: Corollary 4.15 FPC  (A → B) ∨ ((A → B) → A). Corollary 4.16 FPC is not complete with respect to the class of all linear Kripke models. P r o o f. We note that both of the axiom schemas (A → B) ∨ ((A → B) → A) and (A → B) ∨ (B → A) are valid in every linear Kripke model. The result follows from Corollary 4.15. We know that the axiom (a → b) ∨ (b → a) = 1 holds in every chain. Example 4.14 shows a chain that does not satisfy (a → b) ∨ ((a → b) → a) = 1. These facts lead us to consider chains in which this equality holds. www.mlq-journal.org

c 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim


104

M. Alizadeh and M. Ardeshir: On L¨ob algebras

Let us define: Definition 4.17 A L¨ob algebra M is called a weakly faithful L¨ob algebra iff for all a, b ∈ A, a→b=1

iff a ≤ b.

Every faithful algebra is a weakly faithful algebra. The following example shows that the converse is not true. Example 4.18 Let M = Q+ ∪ {∞}, ∧, ∨, 0, ∞ , where Q+ is the set of all non-negative rationals, ∧ and ∨ are defined as usual, and → is defined by
[b] + 1 if b < a, where [b] is the integer part of b, a→b= ∞ otherwise. It is easy to see that M is a weakly faithful L¨ob algebra. Now take any a, b ∈ Q+ such that 0 < a < b < 1. Then ∞ → a = ∞ → b = 1 and so (∞ → b) → (∞ → a) = ∞, but b ≤ a. Definition 4.19 A L¨ob algebra M is called strongly linear iff for all a, b ∈ M , (a → b)∨((a → b) → a) = 1. For example, the free L¨ob algebra is a strongly linear L¨ob algebra (see Theorem 2.11). By a strong chain, we mean a strongly linear L¨ob algebra which is also a chain. It is routine to check that for every finite irreflexive linear Kripke frame K = K, ≺ , mK is a strong chain. Let us define sFPC to be FPC plus the axiom schema (A → B) ∨ ((A → B) → A). Then Theorem 4.20 sFPC is complete with respect to the class of all finite strong chains. P r o o f. Combine Theorem 3.12 with Visser’s result on the completeness of sFPC with respect to the class of all finite irreflexive linear Kripke models, [7]. Proposition 4.21 Let M be a L¨ob algebra and let for every prime filter F the set S = {G : F ≺ G and G is a prime filter} be linearly ordered by ≺. Then M is a strongly linear L¨ob algebra. P r o o f. Suppose (x → y) ∨ ((x → y) → x) = 1 for some x, y ∈ M . Then there is a prime filter F on M such that (x → y) ∨ ((x → y) → x) ∈ F . So x → y ∈ F and (x → y) → x ∈ F . Then there are prime filters F  , F   F such that x ∈ F  , y ∈ F  , x → y ∈ F  and x ∈ F  . This contradicts to the linearity of S. Note that every strongly linear algebra is an La, but the converse is not necessarily true, see Example 4.14. It is easy to see that every chain which has the property that for every element a there is no element between a and 1 → a is a strongly linear L¨ob algebra. We have the following proposition for weakly faithful chains: Proposition 4.22 A weakly faithful chain M is a strong chain iff for every element b ∈ M there is no element between b and 1 → b. P r o o f. Suppose M is a weakly faithful chain L¨ob algebra which is also strong chain. Let a, b ∈ M be such that b ≤ a ≤ 1 → b. The equation (a → b) ∨ ((a → b) → a) = 1 together with linearity implies a → b = 1 or (a → b) → a = 1. Then, by weak faithfulness, a ≤ b or a → b ≤ a. So a = b or 1 → b ≤ a. Then a = b or a = 1 → b. The other direction is obvious. Now let F be a filter on a L¨ob algebra M . We shall write a ≤F b iff there exists a natural number n such that (a → b)n ∈ F . The relation ≤F is a quasi-ordering on M . Write a ∼F b iff there exists a natural number n such that (a → b)n ∧ (b → a)n ∈ F . Clearly ∼F is an equivalence relation. We shall call ∼F the equivalence relation determined by the filter F , and we shall write M/F instead of M/ ∼F . Elements of M/F will be denoted by [a]. Let us define an ordering relation ≤ in M/F by [a] ≤ [b] iff there exists n such that (a → b)n ∈ F . The relation ≤ is transitive and M/F, ≤ is a partially ordered set. For [a], [b] ∈ M/F define 1. [a] ∧ [b] = [a ∧ b], 2. [a] ∨ [b] = [a ∨ b], 3. [a] → [b] = [a → b].

c 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim


www.mlq-journal.org

Math. Log. Quart. 52, No. 1 (2006)

105

It is routine to check that the above relations are well defined and [a ∧ b] and [a ∨ b] are the meet and the join of [a] and [b], respectively, and → satisfies the rules for implication in the L¨ob algebras. Let us denote this algebra by M /F . Then we have: Theorem 4.23 If F is a filter on a weakly faithful L¨ob algebra M , then M /F is a weakly faithful L¨ob algebra as well. By a similar argument for the linear L¨ob algebra and using the above theorem we can also show that the quotient algebra of every strongly linear L¨ob algebra is also a strong chain. Moreover, it can be shown that a weakly faithful strongly linear L¨ob algebra can be embedded into the direct product of weakly faithful strong chains. Now we wish to determine the set of all formulas which are valid in every weakly faithful strongly linear L¨ob algebra. By a similar argument for FPC, we can show that sFPC is faithful. Then the Lindenbaum algebra U of sFPC is a weakly faithful strongly linear L¨ob algebra. Thus it is a subalgebra of the direct product of weakly faithful strong chains. Finally we have: Theorem 4.24 For any sequent A ⇒ B, the following are equivalent: 1. sFPC  A ⇒ B. 2. For every weakly faithful strongly linear L¨ob algebra M , M
A ⇒ B. 3. For every weakly faithful strong chain M , M
A ⇒ B. 4. U
A ⇒ B. Acknowledgements The first author was in part supported by a grant from IPM (No. 83030313). The second author was in part supported by Sharif University of Technology, Iran.

References [1] M. Alizadeh and M. Ardeshir, On the linear Lindenbaum algebra of basic propositional logic. Math. Logic Quarterly 50, 65 – 70 (2004). [2] M. Alizadeh and M. Ardeshir, Amalgamation property for the class of Basic algebras and some of its natural subclasses. Submitted to Archive for Mathematical Logic. [3] M. Ardeshir, Aspects of Basic logic. Ph. D. thesis, Department of Mathematics, Statistics and Computer Science, Marquette University Milwaukee, 1995. [4] M. Ardeshir and W. Ruitenburg, Basic propositional calculus I. Math. Logic Quarterly 44, 317 – 343 (1998). [5] H. Rasiowa and R. Sikorski, The Mathematics of Metamathematics. Monografie Matematyczne 4 (PWN, 1963). [6] Y. Suzuki, F. Wolter, and M. Zakharyaschev, Speaking about transitive frames in propositional languages. J. Logic, Language and Information 7, 317 – 339 (1998). [7] A. Visser, A propositional logic with explicit fixed points. Studia Logica 40, 155 – 175 (1981).

www.mlq-journal.org

c 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim