Soft Comput DOI 10.1007/s00500-014-1317-6

FOUNDATIONS

An algebraic axiomatization of the Ewald’s intuitionistic tense logic Aldo V. Figallo · Gustavo Pelaitay

© Springer-Verlag Berlin Heidelberg 2014

Abstract Ewald (J Symbolic Logic 51(1):166–179, 1986) considered tense operators G, H , F and P on intuitionistic propositional calculus and constructed an intuitionistic tense logic system called IKt. The aim of this paper is to give an algebraic axiomatization of the IKt system. We will also show that the algebraic axiomatization given by Chajda (Cent Eur J Math 9(5):1185–1191, 2011) of the tense operators P and F in intuitionistic logic is not in accordance with the Halmos definition of existential quantifiers. In this paper, we will study the IKt variety of IKt-algebras. First, we will introduce some examples and we will prove some properties. Next, we will prove that the IKt system has IKt-algebras as algebraic counterpart. We will also describe a discrete duality for IKtalgebras bearing in mind the results indicated by Orłowska and Rewitzky (Fundam Inform 81(1–3):275–295, 2007) for Heyting algebras. We will also get a general construction of tense operators on a complete Heyting algebra, which is a power lattice via the so-called Heyting frame. Finally, we will introduce the notion of tense deductive system which allowed us both to determine the congruence lattice in an IKt-

Communicated by L. Spada. The support of CONICET is gratefully acknowledged by Gustavo Pelaitay. A. V. Figallo · G. Pelaitay (B) Instituto de Ciencias Básicas, Universidad Nacional de San Juan, Avda. Ignacio de la Roza 230 (O), 5400 San Juan, Argentina e-mail: [email protected] A. V. Figallo e-mail: [email protected] G. Pelaitay Departamento de Matemática, Universidad Nacional del Sur, Avda. Alem 1253, 8000 Bahía Blanca, Argentina

algebra and to characterize simple and subdirectly irreducible algebras of the IKt variety. Keywords Heyting algebras · Tense operators · Intuitionistic logic · Intuitionistic tense logic

1 Introduction It is known that propositional logics, both classic or nonclassic, does not incorporate the dimension of time. To obtain a tense logic, we enrich the given propositional logic by new unary operators which are usually denoted by G, H , F and P, see e.g., Chiri¸ta˘ (2010, 2012), Diaconescu and Georgescu (2007), Figallo and Pelaitay (2011, 2014), and Figallo et al. (2012). These tense operators were firstly introduced in the classical propositional logic, see Burges (1984). Thus, tense algebras (or tense Boolean algebras) appeared. Tense algebras are algebras (A, G, H ), where A = A, ∨, ∧, −, 0, 1 is a Boolean algebra and, G and H are unary operators on A that satisfy the axioms: (B1) G(1) = 1 and H (1) = 1, (B2) G(x ∧ y) = G(x)∧G(y) and H (x ∧ y) = H (x)∧ H (y), (B3) x ≤ G P(x) and x ≤ H F(x), where P(x) = −H (−x) and F(x) = −G(−x). On the other hand, intuitionistic tense logic IKt was introduced by Ewald (1986) by extending the language of intuitionistic propositional logic with the unary operators P (it was the case), F (it will be the case), H (it has always been the case) and G (it will always be the case). The Hilbertstyle axiomatization of IKt can be found in Ewald (1986) [p. 171]:

123

A. V. Figallo, G. Pelaitay

(A1) All axioms of intuitionistic logic (Int). (A2) G(α → β) → (Gα → Gβ), H (α → β) (H α → Hβ), (A3) G(α ∧ β) ↔ Gα ∧ Gβ, H (α ∧ β) ↔ H α ∧ Hβ, (A4) F(α ∨ β) ↔ Fα ∨ Fβ, P(α ∨ β) ↔ Pα ∨ Pβ, (A5) G(α → β) → (Fα → Fβ), H (α → β) (Pα → Pβ), (A6) Gα ∧ Fβ → F(α ∧ β), H α ∧ Pβ → P(α ∧ β), (A7) G¬α → ¬Fα, H ¬α → ¬Pα, (A8) F H α → α, P Gα → α, (A9) α → G Pα, α → H Fα, (A10) (Fα → Gβ) → G(α → β), (Pα → Hβ) H (α → β), (A11) F(α → β) → (Gα → Fβ), P(α → β) → (H α Pβ).

→

→

→ →

The rules of inference are modus ponens, and (RG)

α , Gα

(R H )

α . Hα

It is well known that the axiomatization of Ewald is not minimal, because several axioms can be deduced from the other axioms. Besides, in contrast to classical tense logic, F and P cannot be defined in terms of G and H . The aim of this paper is to give an algebraic axiomatization of the IKt system. We will also show that the algebraic axiomatization given by Chajda (2011) of the tense operators P and F in intuitionistic logic is not in accordance with the Halmos definition of existential quantifiers. The paper is organized as follows: in Sect. 2, we review some results on Heyting algebras. In Sect. 3, we show that the algebraic axiomatization given by Chajda of the tense operators F and P in intuitionistic logic is not in accordance with the Halmos defintion of existential quantifiers. In Sect. 4, we define the IKt variety of the IKtalgebras, we introduce some examples and we prove some of their properties. In Sect. 5, we prove that the IKt system has IKt-algebras as algebraic counterpart. In Sect. 6, we describe a discrete duality for IKt-algebras. In Sect. 7, we get a general construction of tense operators on a complete Heyting algebra which is a power lattice via the socalled H-frame. Finally, in Sect. 8, we introduce the notion of tense deductive system which allowed us both to determine the congruence lattice in an IKt-algebra and to characterize simple and subdirectly irreducible algebras of the IKt variety.

2 Preliminaries In this paper, we take for granted the concepts and results on Heyting algebras. To obtain more information on this topic, we direct the reader to the bibliography indicated in Balbes

123

and Dwinger (1974), Birkhoff (1967) and Chajda (2007). However, to simplify the reading of the following sections, we summarize the fundamental concepts we use. Let us recall that an algebra A = A, ∨, ∧, →, 0, 1 is a Heyting algebra if the following conditions hold: (H1)A, ∨, ∧, 0, 1 is a lattice with 0, 1, (H2) x ∧ (x → y) = x ∧ y, (H3) x ∧ (y → z) = x ∧ [(x ∧ y) → (x ∧ z)], (H4)(x ∧ y) → x = 1. Let us recall that a complete Heyting algebra is a Heyting algebra, which is complete as a lattice. A subset D of a Heyting algebra A = A, ∨, ∧, →, 0, 1 is a deductive system if it satisfies: (D1) 1 ∈ D (D2) x, x → y ∈ D implies y ∈ D. In what follows, we denote by D(A), the sets of all deductive systems of A. Monteiro (1980) proves both that the notion of a deductive system and filter coincides in a Heyting algebra. Besides, Monteiro showed that if A = A, ∨, ∧, →, 0, 1 is a Heyting algebra and Con(A) is the lattice of all congruences on A, then the following properties are verified: (C1) Con(A) = {R(D) : D ∈ D(A)}, where R(D) = {(x, y) ∈ A × A : x → y ∈ D, y → x ∈ D}, (C2) the lattices Con(A) and D(A) are isomorphic considering the applications θ → [1]θ and D → R(D), which are mutually inverse and where [x]θ stands for the equivalence class of x modulo θ . Next, we recall the discrete duality described in Orłowska and Rewitzky (2007) for Heyting algebras. Let T be a binary relation on a set X , and let U be a subset of X . In what follows, we will denote by [T ]U the set {x ∈ X : T (x) ⊆ U } and by T U the set {x ∈ X : T (x) ∩ U = ∅}. Orłowska and Rewitzky (2007) introduced the notion of Heyting frame (or H-frame, for short) as a pair (X, ≤) where X is a non-empty set and ≤ is a quasi-order on X . These authors proved that if A, ∨, ∧, →, 0, 1 is a Heyting algebra, then its canonical frame is (X (A), ≤c ), where X (A) is the set of all prime filters of A and ≤c is ⊆. It is easy to see that this canonical frame is an H-frame. On the other hand, given an H-frame (X, ≤), they show that its complex algebra is C(X ), ∨c , ∧c , →c , 0c , 1c , where C(X ) = {U ⊆ X : [≤]U = U }, 0c = ∅, 1c = X , U ∨c V = U ∪ V , U ∧c V = U ∩ V and U →c V = [≤]((X \U ) ∪ V ) for all U, V ∈ C(X ). These results allowed them to obtain a discrete duality for Heyting algebras by defining the embeddings as follows:

An algebraic axiomatization

h : A → C(X (A)), defined by h(a) = {M ∈ X (A) : a ∈ M}, k : X → X (C(X )), defined by k(x) = {U ∈ C(X ) : x ∈ U }. General principles and applications of discrete duality are briefly presented in Orłowska and Rewitzky (2007).

3 Tense operators on Heyting algebras In this section, we will show that the algebraic axiomatization given by Chajda of the tense operators F and P in intuitionistic logic is not in accordance with the Halmos definition of existential quantifiers. The notion of tense operators on a Heyting algebra was introduced by Chajda (2011). We repeat the definition given in Chajda (2011). Definition 1 Let A = A, ∨, ∧, →, 0, 1 be a Heyting algebra. Denote by ¬x = x → 0 (the so-called pseudocomplement of x). The unary operators G, H on A are called tense operators if the following conditions are fulfilled: (ch1) G(1) = 1 and H (1) = 1, (ch2) G(x → y) ≤ G(x) → G(y) and H (x → y) ≤ H (x) → H (y), (ch3) G(x) ∨ G(y) ≤ G(x ∨ y) and H (x) ∨ H (y) ≤ H (x ∨ y), (ch4) G(x ∧ y) = G(x) ∧ G(y) and H (x ∧ y) = H (x) ∧ H (y), (ch5) x ≤ G P(x) and x ≤ H F(x), where P(x) = ¬H (¬x) and F(x) = ¬G(¬x). Our aim is to prove that the axioms (ch2) and (ch3) are redundant. To do this, we will need the following lemma. Lemma 1 Let G, H be two unary operators on the Heyting algebra A = A, ∨, ∧, →, 0, 1, satisfying the axiom (ch4). Then, the axioms (ch2) and (ch3) holds. Proof First, we will prove that G is increasing. Let x, y ∈ A such that x ≤ y. From (ch4), we have that G(x) = G(x ∧ y) = G(x) ∧ G(y), i.e., G(x) ≤ G(y). Taking into account that G is increasing, we obtain that G(x) ≤ G(x ∨ y) and G(y) ≤ G(x ∨ y). Hence, G(x) ∨ G(y) ≤ G(x ∨ y). On the other hand, from (H2) and (ch4), we have that G(x)∧G(x → y) = G(x ∧ (x → y)) = G(x ∧ y) ≤ G(y). Therefore, G(x → y) ≤ G(x) → G(y). In a similar way, we can prove that H (x) ∨ H (y) ≤ H (x ∨ y) and H (x → y) ≤ H (x) → H (y), which completes the proof.   Bearing in mind the Lemma 1, we can reformulate the Definition 1 as follows: Definition 2 Let A = A, ∨, ∧, →, 0, 1 be a Heyting algebra. The unary operators G, H on A are called tense operators if the following conditions are fulfilled:

(ch1) G(1) = 1 and H (1) = 1, (ch2) G(x ∧ y) = G(x) ∧ G(y) and H (x ∧ y) = H (x) ∧ H (y), (ch5) x ≤ G P(x) and x ≤ H F(x), where P(x) = ¬H (¬x) and F(x) = ¬G(¬x). We note that this last definition is similar to the definition of tense algebra where (B3) was replaced by (ch5). Another objection to Chajda’s work is that in Chajda (2011)[Remark 8], the author states that if in a Heyting algebra A the tense operators G and H satisfy G(0) = 0 and H (0) = 0, then F and P can be considered as existential quantifiers.1 Such denomination is not clear since F and P are not existential quantifiers in the sense of Halmos (1956), as we prove in Figallo and Pelaitay (2012)[Example 2.5.]. Furthermore, in the intuitionistic tense logic, the tense operators F and P cannot be defined by G and H , i.e., the following equivalences are not satisfied: Fα ↔ ¬G¬α and Pα ↔ ¬H ¬α. Thus, the definition of F and P given in (ch5) is not correct. Therefore, we can say that the algebraic axiomatization given by Chajda (2011) of tense operators P and F is not in accordance with the Halmos approach to existential operators. 4 IKt-algebras In order to obtain an algebraic characterization of the IKt system, in this section, we introduce the IKt variety. More precisely: Definition 3 Let A = A, ∨, ∧, →, 0, 1 be a Heyting algebra, let G, H , F and P be unary operations on A satisfying: (t1) (t2) (t3) (t4) (t5) (t6) (t7)

G(1) = 1 and H (1) = 1, G(x ∧ y) = G(x)∧G(y) and H (x ∧ y) = H (x)∧ H (y), x ≤ G P(x) and x ≤ H F(x), F(0) = 0 and P(0) = 0, F(x ∨ y) = F(x)∨ F(y) and P(x ∨ y) = P(x)∨ P(y), P G(x) ≤ x and F H (x) ≤ x, F(x → y) ≤ G(x) → F(y) and P(x → y) ≤ H (x) → P(y).

Then the algebra (A, G, H, F, P) will be called an IKtalgebra and G, H , F and P will be called tense operators. The following are some useful examples. Example 1 Let (A, G, H ) be a tense algebra. If we define x → y = −x ∨ y, for each x, y ∈ A, then (A, G, H, F, P) is an IKt-algebra, where F and P are defined as in (B3). A unary operator ∃ defined on a Heyting algebra A is an existential quantifier if it satisfies the following conditions: ∃0 = 0, x ∧ ∃x = x, ∃(x ∧ ∃y) = ∃x ∧ ∃y and ∃(x ∨ y) = ∃x ∨ ∃y.

1

123

A. V. Figallo, G. Pelaitay

Fig. 1 Figure of the Example 2

Example 2 Let us consider a Heyting algebra A visualized in Fig. 1. Define operators G, H , F and P by the table: Then, it is x

0

a

b

c

d

e

f

g

1

G(x)

0

0

b

0

d

e

d

g

1

H(x)

0

a

0

c

d

0

f

d

1

F(x)

0

a

d

c

d

1

f

1

1

P(x)

0

d

b

1

d

e

1

g

1

easy to see that (A, G, H, F, P) is an IKt-algebra. We will list some basic properties valid in the IKt-algebras, proving just some of them. Lemma 2 Let (A, G, H, F, P) be an IKt-algebra. Then (t8) x ≤ y implies G(x) ≤ G(y) and x ≤ y implies H (x) ≤ H (y), (t9) x ≤ y implies F(x) ≤ F(y) and x ≤ y implies P(x) ≤ P(y), (t10) F(x) → G(y) ≤ G(x → y) and P(x) → H (y) ≤ H (x → y), (t11) G(x → y) ≤ F(x) → F(y) and H (x → y) ≤ P(x) → P(y), (t12) G(x)∧ F(y) ≤ F(x ∧ y) and H (x)∧ P(y) ≤ P(x ∧ y), (t13) x ∧ F(y) ≤ F(P(x)∧ y) and x ∧ P(y) ≤ P(F(x)∧ y), (t14) F(x) ∧ y = 0 if and only if x ∧ P(y) = 0. Proof Axioms (t8) and (t9) are a consequence of axioms (t2) and (t5), respectively. Next, let us prove (t10). From (t7), we obtain F(P(x) → H (y)) ≤ G P(x) → F H (y). Since x ≤ G P(x) and F H (y) ≤ y we can deduce that G P(x) → F H (y) ≤ x → y. Hence, F(P(x) → H (y)) ≤ x → y. From this last statement and from (t8) it results that H F(P(x) → H (y)) ≤ H (x → y). Then from (t3), we have that P(x) → H (y) ≤ H (x → y). The other inequality is analogous. Let us prove that it verifies (t11). Taking into account axiom (t7), we have that G(x → y) ≤ F((x →

123

y) → y) → F(y). On the other hand, from (H2) it can be deduced that x ≤ (x → y) → y. Then, from (t9) it results F(x) ≤ F((x → y) → y)). Then F((x → y) → y) → F(y) ≤ F(x) → F(y). Hence, G(x → y) ≤ F(x) → F(y). The other inequality is proved similarly. Next, let us prove (t12). Since x ≤ y → (x ∧ y), from (t8), we obtain G(x) ≤ G(y → (x ∧ y)). From this last statement and (t11), it results that G(x) ≤ F(y) → F(x ∧ y), i.e., G(x) ∧ F(y) ≤ F(x ∧ y). The other inequality is proved similarly. Then, let us prove (t13). From (t3), we have that x ∧ F(y) ≤ G P(x)∧F(y). From this statement and from (t12), we obtain x ∧ F(y) ≤ F(P(x) ∧ y). The other inequality is analogous. Finally, let us verify (t14). Let us assume that F(x) ∧ y = 0. From (t13) and (t4), we obtain x ∧ P(y) ≤ P(F(x) ∧ y) = P(0) = 0. Hence, x ∧ P(y) = 0. Similarly, we can prove the other direction.   Our presentation of tense operators differs from that of Chajda since our operators P and F cannot be derived by means of G and H , see the following example: Example 3 Let us consider the IKt-algebra (A, G, H, F, P), defined in the Example 2, then it can be seen: ¬G(¬a) = c = a = F(a) and ¬H (¬a) = 1 = d = P(a). The following Lemma allows us to get an equivalent definition of an IKt-algebra. Lemma 3 Let G, H be two unary operations on the Heyting algebra A = A, ∨, ∧, →, 0, 1 such that G(1) = 1 and H (1) = 1. Then the axiom (t2) is equivalent to the following one: (t2) G(x → y) ≤ G(x) → G(y) and H (x → y) ≤ H (x) → H (y). Proof We will only prove the equivalence between (t2) and (t2) in the case of G. From (t2), (t8) and (H2), we have that G(x) ∧ G(x → y) = G(x ∧ (x → y)) = G(x ∧ y) ≤ G(y). Therefore, G(x → y) ≤ G(x) → G(y). Conversely, let x, y ∈ A be such that x ≤ y. Then x → y = 1 and so, from (t2) and the hypothesis, we obtain that 1 = G(x → y) ≤ G(x) → G(y). Hence, G(x) ≤ G(y) from which we get that G is increasing. From this last assertion and (t2) , we infer that G(x) ≤ G(y → (x ∧ y)) ≤ G(y) → G(x ∧ y). Thus, G(x) ∧ G(y) ≤ G(x ∧ y). From this statement and taking into account that G is increasing, we conclude that G(x) ∧ G(y) = G(x ∧ y).   Thus, if in Definition 3 we replace the axiom (t2) by (t2) , we obtain an equivalent definition of an IKt-algebra. The Lemma 4 shows the relationship between tense operators and the pseudocomplement in an IKt-algebra (A, G, H, F, P).

An algebraic axiomatization

Lemma 4 Let (A, G, H, F, P) be an IKt-algebra. Then (t15) G(0) = 0 if and only if G(¬x) ≤ ¬G(x), (t16) H (0) = 0 if and only if H (¬x) ≤ ¬H (x). (t17) G(¬x) = ¬F(x) and H (¬x) = ¬P(x), (t18) F(x) ≤ ¬G(¬x) and P(x) ≤ ¬H (¬x), (t19) F(¬x) ≤ ¬G(x) and P(¬x) ≤ ¬H (x). Proof First, let us prove (t15). Let us assume that G(0) = 0. Then by (t2) , we have that G(¬x) = G(x → 0) ≤ G(x) → G(0) = ¬G(x). Conversely, if G(¬x) ≤ ¬G(x) then G(0) = G(x ∧ ¬x) = G(x) ∧ G(¬x) ≤ G(x) ∧ ¬G(x) = 0. Therefore, G(0) = 0. Due to the symmetry of tense operators G and H , (t16) can be proved in a similar way to (t15). Let us verify (t17). Since 0 ≤ G(0), we have F(x) → 0 ≤ F(x) → G(0). Applying (t10), we obtain ¬F(x) ≤ G(¬x). On the other hand, from (t11) and (t4), we have: G(¬x) = G(x → 0) ≤ F(x) → F(0) = ¬F(x). Hence, G(¬x) = ¬F(x). The other equality is proved in a similar way. Let us prove (t18). Since F(x) ≤ ¬¬F(x), applying (t17), we have that F(x) ≤ ¬G(¬x). Similarly, P(x) ≤ ¬H (¬x). Finally, let us verify (t19). From (t4) and (t7), we have that : F(x → 0) ≤ G(x) → F(0) = G(x) → 0, that is, F(¬x) ≤ ¬G(x). P(¬x) ≤ ¬H (x) is proved in a similar way.  

5 Algebraic completeness In this section, we will prove that the IKt-algebras are the algebraic counterpart of the IKt system. Let (A, G, H, F, P) be an IKt-algebra. We will denote by V the set of all propositional variables and by For[V] the set of all IKt-formulas. Let v be a function v : V → A assigning to each propositional variable p in V an element v( p) of the Heyting algebra A. Such functions are called valuations. The valuation v can be extended uniquely to the set For[V] of all IKt-formulas inductively by the following way: 1. 2. 3. 4. 5. 6. 7. 8.

v(α ∧ β) = v(α) ∧ v(β), v(α ∨ β) = v(α) ∨ v(β), v(¬α) = ¬v(α), v(α → β) = v(α) → v(β), v(Gα) = Gv(α), v(H α) = H v(α), v(Fα) = Fv(α), v(Pα) = Pv(α).

We say that an IKt-formula α ∈ For [V ] is valid if v(α) = 1 for any valuation v : For [V ] → A on any IKt-algebra (A, G, H, F, P). Theorem 1 Every probable IKt-formula is valid.

Proof The proof concerning the axioms of intuitionistic logic and modus ponens are standard (see e.g., Rasiowa and Sikorski 1968). The validity of the axiom (A2) is a consequence of Lemma 3. Moreover, the proof of the validity of the axioms (A3), (A4), (A5), (A6), (A8), (A9), (A10) and (A11) are consequences of the axioms (t2), (t5), (t11), (t12), (t6), (t3), (t10) and (t7) respectively. Finally, the proof of the validity of the axiom (A7) follows from (t17). So it only remains to prove that the rules (RG) and (RH) preserve validity. Let v be a valuation from the set of all formulas For[V] to some IKtalgebra (A, G, H, F, P) and suppose that v(α) = 1. Hence, from (t1) we have that v(Gα) = G(vα) = G(1) = 1. Therefore, Gα is valid. In a similar way, we can prove that (RH) preserve validity.   To obtain completeness, we show that the valid formulas are probable by applying Lindenbaum–Tarski algebras (see Rasiowa and Sikorski 1968, for instance). First, we define an equivalence relation ≡ on the set For[V]: α ≡ β ⇐⇒ α → β and

 β → α,

where  α means that α is probable in IKt. Lemma 5 The equivalence relation ≡ is a congruence on For [V ]. Proof We will only prove that ≡ is compatible with the connective G and F. Suppose that α ≡ β. Then  α → β and  β → α, which give  G(α → β) and  G(β → α). Hence, from the axiom (A2) and modus ponens we have that  G(α) → G(β) and  G(β) → G(α), that is, G(α) ≡ G(β). Now, we will prove that F is compatible with ≡. Suppose that α ≡ β. Then, we can deduce that  G(α → β) and  G(β → α). Hence, from (A5) and modus ponens we obtain that  Fα → Fβ and  Fβ → Fα. Therefore, Fα ≡ Fβ.   For an IKt-formula α ∈ For [V ], we denote by [α]≡ the equivalence class of α, that is, [α]≡ = {β ∈ For [V ] : α ≡ β}. The set of all IKt-classes is denoted by For [V ]/ ≡. Since the equivalence ≡ is a congruence on the set For[V], we may define its quotient algebra by introducing the following operations on the quotient set For [V ]/ ≡. For α, β ∈ For [V ], we set: 1. 2. 3. 4. 5. 6. 7.

[α]≡ ∨ [β]≡ = [α ∨ β]≡ , [α]≡ ∧ [β]≡ = [α ∧ β]≡ , [α]≡ → [β]≡ = [α → β]≡ , ¬[α]≡ = [¬α]≡ , G[α]≡ = [Gα]≡ , H [α]≡ = [H α]≡ , F[α]≡ = [Fα]≡ ,

123

A. V. Figallo, G. Pelaitay

8. P[α]≡ = [Pα]≡ , 9. 0 = [⊥]≡ , 10. 1 = []≡ . where  is the constant true defined by  := p → p for some fixed propositional variable p ∈ V and ⊥ is the constant false defined by ⊥ := ¬. Since the class of IKt-algebras is equational and the relation ≡ is a congruence, the quotient algebra is an IKt-algebra as stated in the following proposition. Proposition 1 The quotient algebra For [V ]/ ≡, ∨, ∧, →, G, H, F, P, 0, 1 is an IKt-algebra. The IKt-algebra For [V ]/ ≡, ∨, ∧, →, G, H, F, P, 0, 1 is referred to the Lindenbaum–Tarski IKt-algebra. We may now define a valuation v ∗ : V → For [V ]/ ≡ by setting v ∗ ( p) = [ p]≡ It can be easily verified by a straightforward formula induction that we have v ∗ (α) = [α]≡ for all IKt-formula α ∈ For [V ]. The following lemma will be useful to prove the algebraic completeness of IKt. Lemma 6 For any IKt-formula α ∈ For [V ],  α ⇐⇒ v ∗ (α) = 1. Proof If  α, then   → α. The inverse,  α → , always holds. Thus, α ≡  and v ∗ (α) = [α]≡ = []≡ = 1. Conversely, if v ∗ (α) = [α]≡ = 1, then   → α. Hence,  α.  

We end this section by proving that IKt is conservative over intuitionistic logic Int. Let For [V ]∗ denote the set of all Int-formulas, i.e., the set For [V ]∗ is the subset of IKt-formulas For [V ] not containing the symbols G, H , F and P. Obviously, For [V ]∗ is the set of all formulas of intuitionistic propositional logic Int. For any Int-formula α ∈ For [V ]∗ , Int α denotes that α is probable in Int. This means that there is a proof of α that uses the axioms of (A1) and the modus ponens only. Proposition 2 IKt is conservative over intuitionistic logic, i.e., for any IKt-formula α ∈ For [V ]∗ ,  α ⇐⇒ Int α. Proof Let α ∈ For [V ]∗ and suppose that Int α. Since intuitionistic logic Int is known to be complete with respect to Heyting algebras semantics, there exists a Heyting algebra A = A, ∨, ∧, →, 0, 1 and a valuation v ∗ : For [V ]∗ → A such that v ∗ (α) = 1. By setting G(x) = x, H (x) = x, F(x) = x and P(x) = x for any x ∈ A, we may expand this Heyting algebra into an IKt-álgebra (A, G, H, F, P). Also the valuation v ∗ can be extended to a valuation v : For [V ] → A by setting v(Gp) = v ∗ ( p), v(H p) = v ∗ ( p), v(F p) = v ∗ ( p) and v(P p) = v ∗ ( p) for all p ∈ V . Then we have that v(α) = 1, which means that  α by Theorem 2. The converse is trivial.  

6 A discrete duality for IKt-algebras In this section, we describe a discrete duality for IKt-algebras taking into account the one indicated in Sect. 2 for Heyting algebras. To this end, we introduce the following: Definition 4 A structure (X, ≤, R, R −1 ) is an IKt-frame if (X, ≤) is a H-frame, R is a binary on X , and R −1 is the converse of R such that: (K1) (≥ ◦R) ⊆ (R◦ ≥), (K2) (≥ ◦R −1 ) ⊆ (R −1 ◦ ≥).

The next theorem shows the algebraic completeness of IKt

In what follows, IKt-frames will be denoted simply by X when no confusion may arise. Besides, we denote by [x) the set {y ∈ X : x ≤ y} and by (x] the set {y ∈ X : y ≤ x}.

Theorem 2 An IKt-formula is probable if and only if it is valid.

Definition 5 A canonical frame of an IKt-algebra (A, G, H, F, P) is a structure (X (A), ≤c , R c , Q c ), where:

Proof Suppose that α is valid. Then, v(α) = 1 for every valuation v on any IKt-algebra (A, G, H, F, P). In particular, we have v ∗ (α) = 1 in the Lindenbaum–Tarski IKt-algebra. From Lemma 6, we obtain that α must be probable. The other direction is already proved in Theorem 1.  

(a) (X (A), ≤c ) is the canonical frame associated with A = A, ∨, ∧, →, 0, 1, (b) R c and Q c are two binary relations on X (A), (c) R c = (Q c )−1 , (d) (S, T ) ∈ R c ⇐⇒ G −1 (S) ⊆ T ⊆ F −1 (S).

123

An algebraic axiomatization

Lemma 7 The canonical frame of an IKt-algebra is an IKtframe. Proof Taking into account the results established in Orłowska and Rewitzky (2007), we only have to prove (K1) and (K2). Suppose that (S, T ) ∈ (≥c ◦R c ). Then there exists U ∈ X (A) such that S ⊇ U and G −1 (U ) ⊆ T ⊆ F −1 (U ). Consider the filter K generated by T ∪ G −1 (S). We will show that K ⊆ F −1 (S). Assume x ∈ K . Then, there is y ∈ T and z ∈ G −1 (S) such that y ∧ z ≤ x. Hence, y ≤ z → x so F(y) ≤ F(z → x), and thus by (t7), we obtain that F(y) ≤ G(z) → F(x). Since y ∈ T and T ⊆ F −1 (S), we have that G(z) → F(x) ∈ S. From this last statement and the fact that S is a deductive system we have that F(x) ∈ S, i.e., x ∈ F −1 (S). Therefore, K ∩ (A \ F −1 (S)) = ∅. Then by the Birkhoff–Stone theorem there is a prime filter W ∈ X (A) such that W ⊆ F −1 (S), G −1 (S) ⊆ T and W ⊇ T , i.e., (S, T ) ∈ (R c ◦ ≥c ). We can prove (K2) similarly to (K1).   Definition 6 The complex algebra of an IKt-frame (X, ≤, R, R −1 ) is C(X ), G c , H c , F c , P c , where C(X ) is the complex algebra of the H-frame (X, ≤), G c (U ) = [≤ ◦R]U , H c (U ) = [≤ ◦R −1 ]U , F c (U ) = RU and P c (U ) = R −1 U for all U ∈ C(X ). The following result is necessary to the proof of Theorem 3. Lemma 8 C(X ) is closed under the operations G c , H c , F c and P c . Proof We will only prove that C(X ) is closed under the operations G c and F c , i.e., for any U ∈ C(X ), [≤][≤ ◦R]U = [≤ ◦R]U and [≤]RU = RU . In both cases, the inclusion ⊆ follows from reflexivity of ≤. First, we will prove that [≤ ◦R]U ⊆ [≤][≤ ◦R]U . Let x, y ∈ X such that R([x)) ⊆ U and x ≤ y. Let us prove that R([y)) ⊆ U . Now assume z ∈ R([y)). Then, there is w ∈ [y) such that (w, z) ∈ R. By the transitivity of the relation ≤ we obtain that x ≤ w. Since (w, z) ∈ R we can deduce that z ∈ R([x)) therefore z ∈ U . Next, we will prove that RU ⊆ [≤]RU . Let x ∈ RU such that x ≤ y. Then, R(x) ∩ U = ∅, i.e., there exists w ∈ U such that (x, w) ∈ R. Therefore, from (K1) we can deduce that (y, w) ∈ (R◦ ≥). From this last assertion there exists z ∈ X such that (y, z) ∈ R and w ≤ z. Since U ∈ C(X ) we have that z ∈ R(y) ∩ U . Therefore y ∈ RU . Theorem 3 The complex algebra of an IKt-frame is an IKtalgebra.

Proof From the results established in Orłowska and Rewitzky (2007), C(X ) is a Heyting algebra. Besides from Lemma 8, C(X ) is closed under the operations G c , H c , F c and P c . From the definition of the operations G c , H c , F c and P c we can obtain (t1), (t2), (t4) and (t5). Let us prove to verify the remaining axioms. Let us to prove that U ⊆ [≤ ◦R]R −1 U . Let x, y ∈ X such that x ∈ U and y ∈ R([x)). Then, there exists z ∈ [x) such that (z, y) ∈ R. Since U ∈ C(X ) we have that z ∈ U and since z ∈ R −1 (y), we obtain that R −1 (y) ∩ U = ∅, that is, y ∈ R −1 U . In a similar way, we can prove U ⊆ [≤ ◦R −1 ]RU . Therefore (t3) holds. Next, let us to prove that R −1 [≤ ◦R]U ⊆ U . Let x ∈ R −1 [≤ ◦R]U . Then, R −1 (x) ∩ [≤ ◦R]U = ∅. Hence, there exists z ∈ R −1 (x) such that R([z)) ⊆ U . Since ≤ is reflexive we have that (z, x) ∈ (≤ ◦R), i.e., x ∈ R([z)). Therefore x ∈ U . In a similar way, we can prove that R[≤ ◦R −1 ] ⊆ U . Then (t6) holds. Finally, let us to prove that (t7) holds. Suppose that x ∈ R(U →c V ), x ≤ z and z ∈ [≤ ◦R]U . Let us to prove that z ∈ RV , i.e., R(z) ∩ V = ∅. Since x ∈ R(U →c V ) then there exists y ∈ R(x) ∩ (U →c V ), z ≥ x, (x, y) ∈ R, and so from (K1) we have that (z, v) ∈ R and v ≥ y for some v ∈ X . Since v ∈ R(z) ⊆ (≤ ◦R)(z) ⊆ U , y ≤ v and y ∈ (U →c V ) then v ∈ V . Therefore, R(z) ∩ V = ∅. In a similar way, we can prove R −1 (U →c V ) ⊆ [≤   ◦R −1 ]U →c R −1 V . We now show that the embedding h : A → C(X (A)), defined in Sect. 2, preserves G, H , F and P, i.e., Lemma 9 Let (A, G, H, F, P) be an IKt-algebra. For any a ∈ A, (a) (b) (c) (d)

h(G(a)) = G c (h(a)) = [≤c ◦R c ]h(a), h(H (a)) = H c (h(a)) = [≤c ◦Q c ]h(a), h(F(a)) = F c (h(a)) = R c h(a), h(P(a)) = P c (h(a)) = Q c h(a).

Proof We will only prove (a) and (c). (a): Let G(a) ∈ S and let us to prove that (≤c ◦R c )(S) ⊆ h(a). Suppose that T ∈ (≤c ◦R c )(S). Then there exists W ∈ X (A) such that S ⊆ W and G −1 (W ) ⊆ T ⊆ F −1 (W ). Since a ∈ G −1 (S) and S ⊆ W we have that a ∈ G −1 (W ). Hence, a ∈ T , i.e., T ∈ h(a). On the other hand, we show that, for any a ∈ A, if G(a) ∈ / S then S ∈ / [≤c ◦R c ]h(a). Since ≤ is reflexive, it suffices to show that, if G(a) ∈ / S / S and F(b) ∈ / S. Then then S ∈ / [R c ]h(a). Assume G(a) ∈ / F −1 (S). Consider the ideal ↓ a∩ ↓ b, a∈ / G −1 (S) and b ∈ where ↓ x denotes the ideal generated by the single set {x}. Then, (↓ a∩ ↓ b) ∩ G −1 (S) =↓ a ∩ G −1 (S) = ∅ andG −1 (S) is a filter.

123

A. V. Figallo, G. Pelaitay

Then, by the Birkhoff–Stone theorem there is a prime filter T such that

7 A general construction of tense operators

/ T and b ∈ / T. G −1 (S) ⊆ T and a ∈

In this section, we provide a general construction of tense operators on a complete Heyting algebra, which is a power lattice via the so-called H-frame. Similar constructions were indicated in Chajda (2011), Botur et al. (2011), Chajda and Kolaˇrik (2012) and Chajda and Paseka (2012). Let A = A, ∨, ∧, →, 0, 1 be a Heyting algebra and A X the set of all the functions of X in A. It is easy to see that A X , ∨, ∧, →, 0, 1 is a Heyting algebra, where the operations ∨, ∧, → are defined pointwise and besides 0(x) = 0, 1(x) = 1 for each x ∈ X . Taking into account the above statements, we can formulate the following theorem:

Hence, G(a) ∈ / S implies, for some T ∈ X (A), a ∈ / T and / F −1 (S) then b ∈ / T. T ⊆ F −1 (S) and if b ∈ (c): For any a ∈ A and for any S ∈ X (A), we show that F(a) ∈ S iff there existsT ∈ X (A) such that G −1 (S) ⊆ T ⊆ F −1 (S) and a ∈ T. The right-to-left implication is trivial. Assume F(a) ∈ S and G(b) ∈ S. Then a ∈ F −1 (S) and b ∈ G −1 (S). Consider the filter ↑ a∩ ↑ b, where ↑ x denotes the filter generated by the single set {x}. We have that (↑ a∩ ↑ b) ∩ (A \ F −1 (S)) =↑ a ∩ (A \ F −1 (S)) = ∅ and A \ F −1 (S) is an ideal. Therefore, by the Birkhoff–Stone theorem there is a prime filter T such that T ∩ (A \ F −1 (S)) = ∅ and a ∈ T and b ∈ T. Hence a ∈ F −1 (S) implies, for some T ∈ X (A), T ⊆   F −1 (S) and a ∈ T and if b ∈ G −1 (S) then b ∈ T . We now show that the order-embedding k : X → X (C(X )), defined in Sect. 2, preserves the relation R, i.e., Lemma 10 Let (X, ≤, R, R −1 ) be an IKt-frame and let x, y ∈ X . Then, (x, y) ∈ R if and only if k(x), k(y)) ∈ R c . Proof Assume (x, y) ∈ R. We need to show that (k(x), k(y)) ∈ R c . Note that (k(x), k(y)) ∈ R c iff [≤ ◦R]−1 (k(x)) ⊆ k(y) and k(y) ⊆ R−1 k(x) iff for all U ∈ C(X ), x ∈ [≤ ◦R]U implies y ∈ U and for all U ∈ C(X ), y ∈ U implies x ∈ RU .

Theorem 5 Let A = A, ∨, ∧, →, 0, 1 be a complete Heyting algebra and (X, ≤) a H-frame. Define the operators G, H , F and P on A X as follows:   { p(y)}, H ( p)(x) = { p(y)}, G( p)(x) = y∈[x)



F( p)(x) =

y∈(x]

{ p(y)},

P( p)(x) =

y∈[x)



{ p(y)}.

y∈(x]

Then (A X , G, H, F, P) is an IKt-algebra such that G(0) = 0, H (0) = 0, F(1) = 1 and P(1) = 1. Moreover, the following holds: (a) G( p) ≤ F( p) for all p ∈ A X , (b) H ( p) ≤ P( p) for all p ∈ A X . Proof It is evident to prove axioms (t1) and (t4). Since A is a complete Heyting algebra and the infimum and supremum operations are associative, we obtain (t2) and (t5) immediately. From the definition of G and P we have that: ⎫ ⎧ ⎬  ⎨ { p(z)} . G P( p)(x) = ⎭ ⎩ y∈[x)

z∈(y]

Take any U ∈ C(X ) such that x ∈ [≤ ◦R]U . Then, since (x, y) ∈ R and R ⊆ (≤ ◦R), we have that y ∈ U . Take any U ∈ C(X ) such that y ∈ U . Then, since (x, y) ∈ R we have that x ∈ RU . On the other hand, assume (k(x), k(y)) ∈ R c . Then, [≤]{y} ∈ C(X ). So x ∈ R[≤]{y}. From this last statement and (K1) we can deduce that x ∈ [≤]R{y}. Therefore, by reflexivity of ≤ we have that x ∈ R{y}, i.e., (x, y) ∈ R, as required.  

On the other hand, it is clear that  { p(z)}, for each y ∈ [x). p(x) ≤

Hence, we have a discrete duality between IKt-frames and IKt-algebras.

Thus, p ≤ G P( p). Analogously, it is proved that p ≤ H F( p). Therefore, (t3) is verified. From the definition of P and G, we have that ⎫ ⎧ ⎬  ⎨ { p(z)} . P G( p)(x) = ⎭ ⎩

Theorem 4 (a) Every IKt-algebra is embeddable into the complex algebra of its canonical frame. (b) Every IKt-frame is embeddable into the canonical frame of its complex algebra.

123

(1)

z∈(y]

From 1 and the definition of infimum, we have that ⎫ ⎧ ⎬  ⎨ p(x) ≤ { p(z)} . ⎭ ⎩ y∈[x)

z∈(y]

y∈(x]

z∈[y)

An algebraic axiomatization

In addition, we verify that 

0

a

b

c

d

e

f

g

1

(0,0) (a,0) (0,a) (1,0) (a,a) (0,1) (1,a) (a,1) (1,1)

{ p(z)} ≤ p(x), for each y ∈ (x].

(2)

z∈[y)

From 2 and the definition of supremum, we have that ⎫ ⎧ ⎬  ⎨ { p(z)} ≤ p(x). ⎭ ⎩

Since X = {1, 2}, applying the Theorem 5 we have: x

G(x)

H(x)

F(x)

P(x)

(0,0)

(0,0)

(0,0)

(0,0)

(0,0)

(a,0)

(0,0)

(a,0)

(a,0)

(a,a)

(0,a)

(0,a)

(0,0)

(a,a)

(0,a)

F H ( p) ≤ p.

(1,0)

(0,0)

(1,0)

(1,0)

(1,1)

(a,a)

(a,a)

(a,a)

(a,a)

(a,a)

Therefore, (t6) is verified. Finally, we verify (t7). Let y ∈ (x], then  { p(z)} ∧ ( p(y) → q(y)) ≤ p(y) ∧ ( p(y) → q(y))

(0,1)

(0,1)

(0,0)

(1,1)

(0,1)

(1,a)

(a,a)

(1,a)

(1,a)

(1,1)

(a,1)

(a,1)

(a,a)

(1,1)

(a,1)

(1,1)

(1,1)

(1,1)

(1,1)

(1,1)

y∈(x]

z∈[y)

Hence, P G( p) ≤ p. Analogously, it is proved that

z∈(x]

≤ q(y)  ≤ {q(z)}. z∈(x]

From the latter inequality, we have that   ( p(y) → q(y)) ≤ { p(z)} → {q(z)}, z∈(x]

z∈(x]

for each y ∈ (x]. Hence,    ( p(y) → q(y)) ≤ { p(z)} → {q(z)}, y∈(x]

z∈(x]

z∈(x]

Let us observe that G, H , F and P are the tense operators of the Example 2.

8 Congruences and tense deductive system In order to characterize the IKt-congruences, we introduce the following definition: Definition 7 Let (A, G, H, F, P) be an IKt-algebra. A subset D of A is a tense deductive system, if it satisfies (D1), (D2) and the additional condition

that is, F( p → q) ≤ G( p) → F(q). Similarly, P( p → (D3) G(x), H (x) ∈ D for each x ∈ D. q) ≤ H ( p) → P(q) is proved. Therefore, (A X , G, H, F, P) is an IKt-algebra. Besides, it is obvious that G(0) = 0 = We will prove that the IKt-congruence lattice H (0) and that F(1) = 1 = P(1). On the other hand, by the Con I K t (A) is isomorphic to the lattice of all tense deducreflexivity of the relation ≤, we have that tive systems D I K t (A).   { p(y)} ≤ p(x) ≤ { p(y)} = F( p)(x). G( p)(x) = Lemma 11 Let (A, G, H, F, P) be an IKt-algebra. Then y∈[x)

y∈[x)

Therefore, G( p) ≤ F( p). In a similar way we can prove (b).   The following example is an application of the previous theorem. Example 4 Let (X, ≤) be a H-frame, where X = {1, 2} and ≤ denotes the natural order. Let A be the Heyting algebra three-element chain, i.e., A = {0, a, 1}, where 0 ≤ a ≤ 1. Let us consider the Heyting algebra A X , which has nine elements and whose diagram is visualized in Example 2. Then we can identify the elements as follows:

Con I K t (A) = {R(D) : D ∈ D I K t (A)}, where R(D) is defined as (C1) from the Sect. 2. Proof Let D ∈ D I K t (A), since A is a Heyting algebra and D a deductive system of A, from (C1), we know that R(D) ∈ Con(A). Let us prove that R(D) preserves the tense operators. Let (x, y) ∈ R(D) since D is a tense deductive system, G(x → y), G(y → x) ∈ D. Then by (t2) , we obtain that G(x) → G(y), G(y) → G(x) ∈ D, i.e., (G(x), G(y)) ∈ R(D). On the other hand, since G(x → y), G(y → x) ∈ D, applying (t11), we have that F(x) → F(y), F(y) → F(x) ∈ D; i.e., (F(x), F(y)) ∈ R(D). Similarly, it is proved that R(D) preserves H and P. Conversely,

123

A. V. Figallo, G. Pelaitay

let θ ∈ Con I K t (A), then θ ∈ Con(A). From the obtained results in the Sect. 2, we have that [1]θ is a deductive system of A and R([1]θ ) = θ . Besides, from the hypothesis and (T1) we have that (G(x), 1) ∈ θ and (H (x), 1) ∈ θ whenever (x, 1) ∈ θ , i.e., [1]θ ∈ D I K t (A), which completes the proof.   Taking into account the established results in (C2) and Lemma 11, we obtain: Theorem 6 Let (A, G, H, F, P) be an IKt-algebra. Then, the lattices Con I K t (A) and D I K t (A) are isomorphic. We will define the operator d on an IKt-algebra (A, G, H, F, P). This operator was previously defined in Kowalski (1998) for tense algebras, in Diaconescu and Georgescu (2007) for tense MV-algebras, and in Chiri¸ta˘ (2011) for tense θ -valued Łukasiewicz–Moisil algebras, respectively. We will use the properties of d to characterize the simple and subdirectly irreducible IKt-algebras. Definition 8 Let (A, G, H, F, P) be an IKt-algebra. We define the unary operation d on A by d(x) = G(x)∧x∧H (x), for each x ∈ A. For each n ∈ ω we define d n (x) by : d 0 (x) = x, d n+1 (x) = d(d n (x)). Lemma 12 Let (A, G, H, F, P) be an IKt-algebra. Then for any n ∈ ω, the following holds: (a) (b) (c) (d) (e)

d n (1) = 1 and d n (0) = 0, d n+1 (x) ≤ d n (x), d n (x ∧ y) = d n (x) ∧ d n (y), x ≤ y implies d n (x) ≤ d n (y), D ∈ D I K t (A) iff D is a filter closed under d.

Proof It is easy to prove (a), (b), (c) and (d). Let us prove that (e) is satisfied (⇒). We assume that D is a tense deductive system. Then D is a filter, and D is closed under the operations G and H . Let x ∈ D. Then d(x) = G(x) ∧ x ∧ H (x) and it follows that d(x) ∈ D. (⇐) We assume that D is a filter closed under d. We must prove that D is closed under G and H . Let x ∈ D. Then d(x) ≤ G(x) and d(x) ≤ H (x). It follows that G(x), H (x) ∈ D.   Proposition 3 Let (A, G, H, F, P) be an IKt-algebra. The tense deductive system a of (A, G, H, F, P) generated by {a} has the following form: a = {x ∈ A : d n (a) ≤ x, for some n ∈ ω}. Proof We denote by  the right-hand side of the previous equality. 1 ∈ , since d 0 a = a ≤ 1. Let x ∈  so that x ≤ y. Hence, there exists n ∈ ω such that d n (a) ≤ x. Since x ≤ y, we have that d n (a) ≤ y, i,e., y ∈ . Next, let us prove that x ∧ y ∈ , for x, y ∈ . Let x, y ∈ , there exists n, m ∈ ω such that d n (a) ≤ x and d m (a) ≤ y. If we

123

take k = n +m, from Lemma 12, it is verified that d k (a) ≤ x y d k (a) ≤ y, from which d k (a) ≤ x ∧ y, that is, x ∧ y ∈ . From (b) of Lemma 12, we obtain that  is closed under the operator d. Therefore, from (e) of Lemma 12,  is a tense deductive system. The rest of the proof is obvious.   The following two results are a straightforward consequence of Proposition 3 and Theorem 6 (see Kowalski 1998; Diaconescu and Georgescu 2007, for similar results in the case of tense algebras and tense MV-algebras, respectively). Proposition 4 For any IKt-algebra (A, G, H, F, P) the following are equivalent: (i) (A, G, H, F, P) is a simple IKt-algebra, (ii) (A, G, H, F, P) satisfies the property: (A) For any a ∈ A \ {1} there exists n ∈ ω such that d n (a) = 0. Proposition 5 For any IKt-algebra (A, G, H, F, P) the following are equivalent: (i) (A, G, H, F, P) is a subdirectly irreducible IKt-algebra, (ii) (A, G, H, F, P) satisfies the property: (B) There exists b ∈ A \ {1}, such that for any a ∈ A \ {1} there exists n ∈ ω such that d n (a) ≤ b. Finally, we show a simple example of a subdirectly irreducible IKt-algebra which is not a subdirectly irreducible Heyting algebra. Example 5 Let us consider the IKt-algebra (A, G, H, F, P) of the Example 2. It is plain that A is not a subdirectly irreducible Heyting algebra. On the other hand, taking into account (B) of the Proposition 5, we can check that (A, G, H, F, P) is a subdirectly irreducible IKt-algebra. Acknowledgments We thank the anonymous referee for the very thorough reading and contributions to improve our presentation of the paper.

References Balbes R, Dwinger P (1974) Distributive lattices. University of Missouri Press, Columbia Birkhoff G (1967) Lattice theory, 3rd edn. American Mathematical Society Colloquium Publications, vol XXV. American Mathematical Society, Providence, R.I Botur M, Chajda I, Halaš R, Kolaˇrik M (2011) Tense operators on basic algebras. Int J Theor Phys 50(12):3737–3749 Burges J (1984) Basic tense logic. In: Gabbay DM, Günter F (eds) Handbook of philosophical logic, vol II. Reidel, Dordrecht, pp 89– 139 Chajda I, Halaš R, Kühr J (2007) Semilattice structures, Res. Exp. Math, vol 30. Heldermann, Lemgo.

An algebraic axiomatization Chajda I (2011) Algebraic axiomatization of tense intuitionistic logic. Cent Eur J Math 9(5):1185–1191 Chajda I, Paseka J (2012) Dynamic effect algebras and their representations. Soft Comput 16(10):1733–1741 Chajda I, Kolaˇrik M (2012) Dynamic effect algebras. Math Slovaca 62(3):379–388 Chiri¸ta˘ C (2010) Tense θ-valued Moisil propositional logic. Int J Comput Commun Control 5:642–653 Chiri¸ta˘ C (2011) Tense θ-valued Łukasiewicz-Moisil algebras. J Mult Valued Logic Soft Comput 17(1):1–24 Chiri¸ta˘ C (2012) Polyadic tense θ-valued Łukasiewicz-Moisil algebras. Soft Comput 16(6):979–987 Diaconescu D, Georgescu G (2007) Tense operators on M V -algebras and Łukasiewicz-Moisil algebras. Fundam Inform 81(4):379–408 Ewald WB (1986) Intuitionistic tense and modal logic. J Symbolic Logic 51(1):166–179 Figallo AV, Pelaitay G (2011) Note on tense SHn-algebras. Ann Univ Craiova Ser Math Inform 38(4):24–32 Figallo AV, Pelaitay G, Sanza C (2012) Discrete duality for TSHalgebras. Commun Korean Math Soc 27(1):47–56 Figallo AV, Pelaitay G (2012) Remarks on heyting algebras with tense operators. Bull Sect Logic Univ Lódz 41(1–2):71–74

Figallo AV, Pelaitay G (2014) Tense operators on De Morgan Algebras. Log J IGPL 22(2):255–267 Halmos PR (1956) Algebraic logic. I. Monadic Boolean algebras. Compos Math 12:217–249 Kowalski T (1998) Varieties of tense algebras. Rep Math Logic 32:53– 95 Monteiro A (1980) Sur les algèbres de Heyting symétriques. Portugaliae Math 39:1–237 Orłowska E, Rewitzky I (2007) Discrete duality for Heyting algebras with operators. Fundam Inform 81(1–3):275–295 Orłowska E, Rewitzky I (2007) Discrete duality and its applications to reasoning with incomplete information. In: Kryszkiewicz M, Peters JF, Rybi´nski H, Skowron A (eds) Rough sets and intelligent systems paradigms. Lecture Notes in Artificial Intelligence, vol 4585. Springer-Verlag, Heidelberg, pp 51–56. Rasiowa H, Sikorski R (1968) The mathematics of metamathematics, 2nd edn. PWN-Polish Scientific Publishers, Warsaw

123