An algebraic axiomatization of the Ewald’s intuitionistic tense logic

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 IKt-algebras 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-algebra and to characterize simple and subdirectly irreducible algebras of the IKt variety.

1 Introduction

It is known that propositional logics, both classic or non-classic, 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ţă (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 $(\mathcal {A},G,H)$, where $\mathcal {A}=\langle A,\vee ,\wedge ,-,0,1\rangle$ 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\wedge y)=G(x)\wedge G(y)$ and $H(x\wedge y)=H(x)\wedge H(y)$,

• (B3) $x\le GP(x)$ and $x\le HF(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 Hilbert-style axiomatization of IKt can be found in Ewald (1986) [p. 171]:

• (A1) All axioms of intuitionistic logic (Int).

• (A2) $G(\alpha \rightarrow \beta )\rightarrow (G\alpha \rightarrow G\beta )$,  $H(\alpha \rightarrow \beta )\rightarrow (H\alpha \rightarrow H\beta )$,

• (A3) $G(\alpha \wedge \beta )\leftrightarrow G\alpha \wedge G\beta$,  $H(\alpha \wedge \beta )\leftrightarrow H\alpha \wedge H\beta$,

• (A4) $F(\alpha \vee \beta )\leftrightarrow F\alpha \vee F\beta$,  $P(\alpha \vee \beta )\leftrightarrow P\alpha \vee P\beta$,

• (A5) $G(\alpha \rightarrow \beta )\rightarrow (F\alpha \rightarrow F\beta )$,  $H(\alpha \rightarrow \beta )\rightarrow$ $(P\alpha \rightarrow P\beta )$,

• (A6) $G\alpha \wedge F\beta \rightarrow F(\alpha \wedge \beta )$,  $H\alpha \wedge P\beta \rightarrow P(\alpha \wedge \beta )$,

• (A7) $G\lnot \alpha \rightarrow \lnot F\alpha$,  $H\lnot \alpha \rightarrow \lnot P\alpha$,

• (A8) $FH\alpha \rightarrow \alpha$,  $PG\alpha \rightarrow \alpha$,

• (A9) $\alpha \rightarrow GP\alpha$,  $\alpha \rightarrow HF\alpha$,

• (A10) $(F\alpha \rightarrow G\beta )\rightarrow G(\alpha \rightarrow \beta )$,  $(P\alpha \rightarrow H\beta )\rightarrow H(\alpha \rightarrow \beta )$,

• (A11) $F(\alpha \rightarrow \beta )\rightarrow (G\alpha \rightarrow F\beta )$,  $P(\alpha \rightarrow \beta )\rightarrow (H\alpha \rightarrow P\beta )$.

The rules of inference are modus ponens, and

$$\begin{aligned} (RG)\,\, \displaystyle \frac{\alpha }{G\alpha },\qquad (RH)\,\, \displaystyle \frac{\alpha }{H\alpha }. \end{aligned}$$

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 IKt-algebras, 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 so-called 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 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 $\mathcal {A}=\langle A,\vee ,\wedge ,\rightarrow ,0,1\rangle$ is a Heyting algebra if the following conditions hold:

• (H1)$\langle A,\vee ,\wedge ,0,1\rangle$ is a lattice with $0$, $1$,

• (H2) $x\wedge (x\rightarrow y)=x\wedge y$,

• (H3) $x\wedge (y\rightarrow z)=x\wedge [(x\wedge y)\rightarrow (x\wedge z)]$,

• (H4)$(x\wedge y)\rightarrow 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 $\mathcal {A}=\langle A,\vee ,\wedge ,\rightarrow ,0,1\rangle$ is a deductive system if it satisfies:

• (D1) $1\in D$

• (D2) $x, \, x\rightarrow y \in D$ implies $y\in D$.

In what follows, we denote by $\mathcal {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 $\mathcal {A}=\langle A,\vee ,\wedge ,\rightarrow ,0,1\rangle$ 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\in \mathcal {D}(A)\}$, where $R(D)=\{(x,y)\in A\times A: x\rightarrow y\in D, y\rightarrow x\in D\}$,

• (C2) the lattices $Con(A)$ and $\mathcal {D}(A)$ are isomorphic considering the applications $\theta \mapsto [1]_\theta$ and $D\mapsto R(D)$, which are mutually inverse and where $[x]_\theta$ stands for the equivalence class of $x$ modulo $\theta$.

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\in X: T(x)\subseteq U\}$ and by $\langle T\rangle U$ the set $\{x\in X: T(x)\cap U\not =\emptyset \}$.

Orłowska and Rewitzky (2007) introduced the notion of Heyting frame (or H-frame, for short) as a pair $(X, \le )$ where $X$ is a non-empty set and $\le$ is a quasi-order on $X$. These authors proved that if $\langle A, \vee , \wedge , \rightarrow , 0, 1\rangle$ is a Heyting algebra, then its canonical frame is $({\mathcal X}(A),\le ^{c})$, where ${\mathcal X}(A)$ is the set of all prime filters of $A$ and $\le ^{c}$ is $\subseteq$. It is easy to see that this canonical frame is an H-frame. On the other hand, given an H-frame $(X, \le )$, they show that its complex algebra is $\langle {\mathcal C}(X), \vee ^{c},\wedge ^{c}, \rightarrow ^{c}, 0^{c}, 1^{c}\rangle$, where ${\mathcal C}(X)=\{U\subseteq X: [\le ]U=U\}$, $0^{c}=\emptyset$, $1^{c}=X$, $U\vee ^{c}V=U\cup V$, $U\wedge ^{c}V=U\cap V$ and $U\rightarrow ^{c}V=[\le ]((X{\setminus }U)\cup V)$ for all $U,V\in {\mathcal C}(X)$.

These results allowed them to obtain a discrete duality for Heyting algebras by defining the embeddings as follows:

• $h:A \rightarrow {\mathcal C}({\mathcal X}(A))$, defined by $h(a)=\{M\in {\mathcal X}(A): a\in M\}$,

• $k: X\rightarrow {\mathcal X}({\mathcal C}(X))$, defined by $k(x)=\{U\in {\mathcal C}(X): x\in 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 $\mathcal {A}=\langle A,\vee ,\wedge ,\rightarrow ,0,1\rangle$ be a Heyting algebra. Denote by $\lnot x= x \rightarrow 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\rightarrow y)\le G(x)\rightarrow G(y)$ and $H(x\rightarrow y)\le H(x)\rightarrow H(y)$,

• (ch3) $G(x)\vee G(y)\le G(x\vee y)$ and $H(x)\vee H(y)\le H(x\vee y)$,

• (ch4) $G(x\wedge y)=G(x)\wedge G(y)$ and $H(x\wedge y)=H(x)\wedge H(y)$,

• (ch5) $x\le GP(x)$ and $x\le HF(x)$, where $P(x)=\lnot H(\lnot x)$ and $F(x)=\lnot G(\lnot 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 $\mathcal {A}=\langle A,\vee ,\wedge ,\rightarrow ,0,1\rangle$, satisfying the axiom (ch4). Then, the axioms (ch2) and (ch3) holds.

Proof

First, we will prove that $G$ is increasing. Let $x,y\in A$ such that $x\le y$. From (ch4), we have that $G(x)=G(x\wedge y)=G(x)\wedge G(y)$, i.e., $G(x)\le G(y)$. Taking into account that $G$ is increasing, we obtain that $G(x)\le G(x\vee y)$ and $G(y)\le G(x\vee y)$. Hence, $G(x)\vee G(y)\le G(x\vee y)$. On the other hand, from (H2) and (ch4), we have that $G(x)\wedge G(x\rightarrow y)=G(x\wedge (x\rightarrow y))=G(x\wedge y)\le G(y)$. Therefore, $G(x\rightarrow y)\le G(x)\rightarrow G(y)$. In a similar way, we can prove that $H(x)\vee H(y)\le H(x\vee y)$ and $H(x\rightarrow y)\le H(x)\rightarrow H(y)$, which completes the proof. $\square$

Bearing in mind the Lemma 1, we can reformulate the Definition 1 as follows:

Definition 2

Let $\mathcal {A}=\langle A,\vee ,\wedge ,\rightarrow ,0,1\rangle$ 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\wedge y)=G(x)\wedge G(y)$ and $H(x\wedge y)=H(x)\wedge H(y)$,

• (ch5) $x\le GP(x)$ and $x\le HF(x)$, where $P(x)=\lnot H(\lnot x)$ and $F(x)=\lnot G(\lnot 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.¹ 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:

$$\begin{aligned} F\alpha \leftrightarrow \lnot G\lnot \alpha \quad and \quad P\alpha \leftrightarrow \lnot H\lnot \alpha . \end{aligned}$$

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 $\mathcal {A}=\langle A,\vee ,\wedge ,\rightarrow ,0,1\rangle$ be a Heyting algebra, let $G$, $H$, $F$ and $P$ be unary operations on $A$ satisfying:

• (t1) $G(1)=1$ and $H(1)=1$,

• (t2) $G(x\wedge y)=G(x)\wedge G(y)$ and $H(x\wedge y)=H(x)\wedge H(y)$,

• (t3) $x\le GP(x)$ and $x\le HF(x)$,

• (t4) $F(0)=0$ and $P(0)=0$,

• (t5) $F(x\vee y)= F(x)\vee F(y)$ and $P(x\vee y)= P(x)\vee P(y)$,

• (t6) $PG(x)\le x$ and $FH(x)\le x$,

• (t7) $F(x\rightarrow y)\le G(x)\rightarrow F(y)$ and $P(x\rightarrow y)\le H(x)\rightarrow P(y)$.

Then the algebra $(\mathcal {A},G,H,F,P)$ will be called an IKt-algebra and $G$, $H$, $F$ and $P$ will be called tense operators.

The following are some useful examples.

Example 1

Let $(\mathcal {A},G,H)$ be a tense algebra. If we define $x\rightarrow y=-x\vee y$, for each $x,y\in A$, then $(\mathcal {A},G,H,F$, $P)$ is an IKt-algebra, where $F$ and $P$ are defined as in (B3).

Example 2

Let us consider a Heyting algebra $\mathcal {A}$ visualized in Fig. 1.

Fig. 1

Figure of the Example 2

Define operators $G$, $H$, $F$ and $P$ by the table:

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

Then, it is easy to see that $(\mathcal {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 $(\mathcal {A},G,H,F,P)$ be an IKt-algebra. Then

• (t8) $x\le y$ implies $G(x)\le G(y)$ and $x\le y$ implies $H(x)\le H(y)$,

• (t9) $x\le y$ implies $F(x)\le F(y)$ and $x\le y$ implies $P(x)\le P(y)$,

• (t10) $F(x)\rightarrow G(y)\le G(x\rightarrow y)$ and $P(x)\rightarrow H(y)\le H(x\rightarrow y)$,

• (t11) $G(x\rightarrow y)\le F(x)\rightarrow F(y)$ and $H(x\rightarrow y)\le P(x)\rightarrow P(y)$,

• (t12) $G(x)\wedge F(y)\le F(x\wedge y)$ and $H(x)\wedge P(y)\le P(x\wedge y)$,

• (t13) $x\wedge F(y)\le F(P(x)\wedge y)$ and $x\wedge P(y)\le P(F(x)\wedge y)$,

• (t14) $F(x)\wedge y=0$ if and only if $x\wedge 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)\rightarrow H(y))\le GP(x)\rightarrow FH(y)$. Since $x\le GP(x)$ and $FH(y)\le y$ we can deduce that $GP(x)\rightarrow FH(y)\le x\rightarrow y$. Hence, $F(P(x)\rightarrow H(y))\le x\rightarrow y$. From this last statement and from (t8) it results that $HF(P(x)\rightarrow H(y))\le H(x\rightarrow y)$. Then from (t3), we have that $P(x)\rightarrow H(y)\le H(x\rightarrow y)$. The other inequality is analogous. Let us prove that it verifies (t11). Taking into account axiom (t7), we have that $G(x\rightarrow y)\le F((x\rightarrow y)\rightarrow y)\rightarrow F(y)$. On the other hand, from (H2) it can be deduced that $x\le (x\rightarrow y)\rightarrow y$. Then, from (t9) it results $F(x)\le F((x\rightarrow y)\rightarrow y))$. Then $F((x\rightarrow y)\rightarrow y)\rightarrow F(y)\le F(x)\rightarrow F(y)$. Hence, $G(x\rightarrow y)\le F(x)\rightarrow F(y)$. The other inequality is proved similarly. Next, let us prove (t12). Since $x\le y\rightarrow (x\wedge y)$, from (t8), we obtain $G(x)\le G(y\rightarrow (x\wedge y))$. From this last statement and (t11), it results that $G(x)\le F(y)\rightarrow F(x\wedge y)$, i.e., $G(x)\wedge F(y)\le F(x\wedge y)$. The other inequality is proved similarly. Then, let us prove (t13). From (t3), we have that $x\wedge F(y)\le GP(x)\wedge F(y)$. From this statement and from (t12), we obtain $x\wedge F(y)\le F(P(x)\wedge y)$. The other inequality is analogous. Finally, let us verify (t14). Let us assume that $F(x)\wedge y=0$. From (t13) and (t4), we obtain $x\wedge P(y)\le P(F(x)\wedge y)=P(0)=0$. Hence, $x\wedge P(y)=0$. Similarly, we can prove the other direction. $\square$

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 $(\mathcal {A},G,H,F$, $P)$, defined in the Example 2, then it can be seen:

$$\begin{aligned} \lnot G(\lnot a)=c\not =a=F(a)~\ \hbox {and} ~\ \lnot H(\lnot a)=1\not =d=P(a). \end{aligned}$$

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 $\mathcal {A}=\langle A,\vee ,\wedge ,\rightarrow ,0,1\rangle$ such that $G(1)=1$ and $H(1)=1$. Then the axiom (t2) is equivalent to the following one:

• (t2)$^{\prime }G(x\rightarrow y)\le G(x)\rightarrow G(y)$ and $H(x\rightarrow y)\le H(x)\rightarrow H(y)$.

Proof

We will only prove the equivalence between (t2) and (t2)$^{\prime }$ in the case of $G$. From (t2), (t8) and (H2), we have that $G(x)\wedge G(x\rightarrow y) = G(x\wedge (x\rightarrow y)) = G(x \wedge y) \le G(y)$. Therefore, $G(x\rightarrow y) \le G(x) \rightarrow G(y)$. Conversely, let $x,y\in A$ be such that $x\le y$. Then $x\rightarrow y=1$ and so, from (t2)$^{\prime }$ and the hypothesis, we obtain that $1= G(x \rightarrow y) \le G(x)\rightarrow G(y)$. Hence, $G(x) \le G(y)$ from which we get that $G$ is increasing. From this last assertion and (t2)$^{\prime }$, we infer that $G(x) \le G(y \rightarrow (x \wedge y)) \le G(y) \rightarrow G(x \wedge y)$. Thus, $G(x) \wedge G(y) \le G(x\wedge y)$. From this statement and taking into account that $G$ is increasing, we conclude that $G(x) \wedge G(y) = G(x\wedge y)$. $\square$

Thus, if in Definition 3 we replace the axiom (t2) by (t2)$^{\prime }$, 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 $(\mathcal {A},G,H,F,P)$.

Lemma 4

Let $(\mathcal {A},G,H,F,P)$ be an IKt-algebra. Then

• (t15) $G(0)=0$ if and only if $G(\lnot x)\le \lnot G(x)$,

• (t16) $H(0)=0$ if and only if $H(\lnot x)\le \lnot H(x)$.

• (t17) $G(\lnot x)=\lnot F(x)$ and $H(\lnot x)=\lnot P(x)$,

• (t18) $F(x)\le \lnot G(\lnot x)$ and $P(x)\le \lnot H(\lnot x)$,

• (t19) $F(\lnot x)\le \lnot G(x)$ and $P(\lnot x)\le \lnot H(x)$.

Proof

First, let us prove (t15). Let us assume that $G(0) =0$. Then by (t2)$^{\prime }$, we have that $G(\lnot x)=G(x\rightarrow 0)\le G(x)\rightarrow G(0)=\lnot G(x)$. Conversely, if $G(\lnot x)\le \lnot G(x)$ then $G(0)=G(x\wedge \lnot x)=G(x)\wedge G(\lnot x)\le G(x)\wedge \lnot 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\le G(0)$, we have $F(x)\rightarrow 0\le F(x)\rightarrow G(0)$. Applying (t10), we obtain $\lnot F(x)\le G(\lnot x)$. On the other hand, from (t11) and (t4), we have: $G(\lnot x)=G(x\rightarrow 0)\le F(x)\rightarrow F(0)=\lnot F(x)$. Hence, $G(\lnot x)=\lnot F(x)$. The other equality is proved in a similar way. Let us prove (t18). Since $F(x)\le \lnot \lnot F(x)$, applying (t17), we have that $F(x)\le \lnot G(\lnot x)$. Similarly, $P(x)\le \lnot H(\lnot x)$. Finally, let us verify (t19). From (t4) and (t7), we have that : $F(x\rightarrow 0)\le G(x)\rightarrow F(0)=G(x)\rightarrow 0$, that is, $F(\lnot x)\le \lnot G(x)$. $P(\lnot x)\le \lnot H(x)$ is proved in a similar way. $\square$

5 Algebraic completeness

In this section, we will prove that the IKt-algebras are the algebraic counterpart of the IKt system.

Let $(\mathcal {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\rightarrow 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. $v(\alpha \wedge \beta )=v(\alpha )\wedge v(\beta ),$

• 2. $v(\alpha \vee \beta )=v(\alpha )\vee v(\beta ),$

• 3. $v(\lnot \alpha )=\lnot v(\alpha )$,

• 4. $v(\alpha \rightarrow \beta )=v(\alpha )\rightarrow v(\beta ),$

• 5. $v(G\alpha )=Gv(\alpha ),$

• 6. $v(H\alpha )=Hv(\alpha ),$

• 7. $v(F\alpha )=Fv(\alpha ),$

• 8. $v(P\alpha )=Pv(\alpha ).$

We say that an IKt-formula $\alpha \in For[V]$ is valid if $v(\alpha )=1$ for any valuation $v:For[V]\rightarrow A$ on any IKt-algebra $(\mathcal {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 IKt-algebra $(A,G,H,F,P)$ and suppose that $v(\alpha )=1$. Hence, from (t1) we have that $v(G\alpha )=G(v\alpha )=G(1)=1$. Therefore, $G\alpha$ is valid. In a similar way, we can prove that (RH) preserve validity. $\square$

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 $\equiv$ on the set For[V]:

$$\begin{aligned} \alpha \equiv \beta \Longleftrightarrow \vdash \alpha \rightarrow \beta \quad \hbox {and}\quad \vdash \beta \rightarrow \alpha , \end{aligned}$$

where $\vdash \alpha$ means that $\alpha$ is probable in IKt.

Lemma 5

The equivalence relation $\equiv$ is a congruence on $For[V]$.

Proof

We will only prove that $\equiv$ is compatible with the connective $G$ and $F$. Suppose that $\alpha \equiv \beta$. Then $\vdash \alpha \rightarrow \beta$ and $\vdash \beta \rightarrow \alpha$, which give $\vdash G(\alpha \rightarrow \beta )$ and $\vdash G(\beta \rightarrow \alpha )$. Hence, from the axiom (A2) and modus ponens we have that $\vdash G(\alpha )\rightarrow G(\beta )$ and $\vdash G(\beta )\rightarrow G(\alpha )$, that is, $G(\alpha ) \equiv G(\beta )$. Now, we will prove that $F$ is compatible with $\equiv$. Suppose that $\alpha \equiv \beta$. Then, we can deduce that $\vdash G(\alpha \rightarrow \beta )$ and $\vdash G(\beta \rightarrow \alpha )$. Hence, from (A5) and modus ponens we obtain that $\vdash F\alpha \rightarrow F\beta$ and $\vdash F\beta \rightarrow F\alpha$. Therefore, $F\alpha \equiv F\beta$. $\square$

For an IKt-formula $\alpha \in For[V]$, we denote by $[\alpha ]_\equiv$ the equivalence class of $\alpha$, that is,

$$\begin{aligned}{}[\alpha ]_\equiv =\{\beta \in For[V]: \alpha \equiv \beta \}. \end{aligned}$$

The set of all IKt-classes is denoted by $For[V]/\equiv$.

Since the equivalence $\equiv$ 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]/\equiv$. For $\alpha ,\beta \in For[V]$, we set:

• 1. $[\alpha ]_\equiv \vee [ \beta ]_\equiv =[\alpha \vee \beta ]_\equiv ,$

• 2. $[\alpha ]_\equiv \wedge [\beta ]_\equiv =[\alpha \wedge \beta ]_\equiv ,$

• 3. $[\alpha ]_\equiv \rightarrow [\beta ]_\equiv =[\alpha \rightarrow \beta ]_\equiv ,$

• 4. $\lnot [\alpha ]_\equiv =[\lnot \alpha ]_\equiv ,$

• 5. $G[\alpha ]_\equiv =[G\alpha ]_\equiv ,$

• 6. $H[\alpha ]_\equiv =[H\alpha ]_\equiv ,$

• 7. $F[\alpha ]_\equiv =[F\alpha ]_\equiv ,$

• 8. $P[\alpha ]_\equiv =[P\alpha ]_\equiv ,$

• 9. $0=[\bot ]_\equiv ,$

• 10. $1=[\top ]_\equiv .$

where $\top$ is the constant true defined by

$$\begin{aligned} \top :=p\rightarrow p \end{aligned}$$

for some fixed propositional variable $p\in V$ and $\bot$ is the constant false defined by

$$\begin{aligned} \bot :=\lnot \top . \end{aligned}$$

Since the class of IKt-algebras is equational and the relation $\equiv$ is a congruence, the quotient algebra is an IKt-algebra as stated in the following proposition.

Proposition 1

The quotient algebra

$$\begin{aligned} \langle For[V]/\equiv ,\vee ,\wedge ,\rightarrow ,G,H,F,P,\mathbf{0},\mathbf{1}\rangle \end{aligned}$$

is an IKt-algebra.

The IKt-algebra

$$\begin{aligned} \langle For[V]/\equiv ,\vee ,\wedge ,\rightarrow ,G,H,F,P,\mathbf{0},\mathbf{1}\rangle \end{aligned}$$

is referred to the Lindenbaum–Tarski IKt-algebra. We may now define a valuation $v^{*}: V\rightarrow For[V]/\equiv$ by setting

$$\begin{aligned} v^{*}(p)=[p]_\equiv \end{aligned}$$

It can be easily verified by a straightforward formula induction that we have

$$\begin{aligned} v^{*}(\alpha )=[\alpha ]_\equiv \end{aligned}$$

for all IKt-formula $\alpha \in For[V].$

The following lemma will be useful to prove the algebraic completeness of IKt.

Lemma 6

For any IKt-formula $\alpha \in For[V]$,

$$\begin{aligned} \vdash \alpha \Longleftrightarrow v^{*}(\alpha )=\mathbf{1}. \end{aligned}$$

Proof

If $\vdash \alpha$, then $\vdash \top \rightarrow \alpha$. The inverse, $\vdash \alpha \rightarrow \top$, always holds. Thus, $\alpha \equiv \top$ and $v^{*}(\alpha )=[\alpha ]_\equiv =[\top ]_\equiv =\mathbf{1}.$ Conversely, if $v^{*}(\alpha )=[\alpha ]_\equiv =\mathbf{1}$, then $\vdash \top \rightarrow \alpha$. Hence, $\vdash \alpha$. $\square$

The next theorem shows the algebraic completeness of IKt

Theorem 2

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

Proof

Suppose that $\alpha$ is valid. Then, $v(\alpha )=1$ for every valuation $v$ on any IKt-algebra $(\mathcal {A},G,H,F,P)$. In particular, we have $v^{*}(\alpha )=\mathbf{1}$ in the Lindenbaum–Tarski IKt-algebra. From Lemma 6, we obtain that $\alpha$ must be probable. The other direction is already proved in Theorem 1. $\square$

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 $\alpha \in For[V]^{*}$, $\vdash _{ Int }\alpha$ denotes that $\alpha$ is probable in Int. This means that there is a proof of $\alpha$ 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 $\alpha \in For[V]^{*}$,

$$\begin{aligned} \vdash \alpha \Longleftrightarrow \, \vdash _\mathrm{Int}\alpha . \end{aligned}$$

Proof

Let $\alpha \in For[V]^*$ and suppose that $\not \vdash _\mathrm{Int}\alpha$. Since intuitionistic logic Int is known to be complete with respect to Heyting algebras semantics, there exists a Heyting algebra $\mathcal {A}=\langle A,\vee ,\wedge ,\rightarrow ,0,1\rangle$ and a valuation $v^{*}: For[V]^{*}\rightarrow A$ such that $v^{*}(\alpha )\not =1$. By setting $G(x)=x$, $H(x)=x$, $F(x)=x$ and $P(x)=x$ for any $x\in A$, we may expand this Heyting algebra into an IKt-álgebra $(\mathcal {A},G,H,F,P)$. Also the valuation $v^{*}$ can be extended to a valuation $v:For[V]\rightarrow A$ by setting $v(Gp)=v^{*}(p)$, $v(Hp)=v^{*}(p)$, $v(Fp)=v^{*}(p)$ and $v(Pp)=v^{*}(p)$ for all $p\in V$. Then we have that $v(\alpha )\not =1$, which means that $\not \vdash \alpha$ by Theorem 2. The converse is trivial. $\square$

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,\le ,R,R^{-1})$ is an IKt-frame if $(X,\le )$ is a H-frame, $R$ is a binary on $X$, and $R^{-1}$ is the converse of $R$ such that:

• (K1) $(\ge \circ R)\subseteq (R\circ \ge ),$

• (K2) $(\ge \circ R^{-1})\subseteq (R^{-1}\circ \ge ).$

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

Definition 5

A canonical frame of an IKt-algebra

$(\mathcal {A},G,H,F,P)$ is a structure $(\mathcal {X}(A),\le ^{c},R^{c},Q^{c})$, where:

• (a) $(\mathcal {X}(A),\le ^{c})$ is the canonical frame associated with $\mathcal {A}=\langle A,\vee ,\wedge ,\rightarrow ,0,1\rangle$,

• (b) $R^{c}$ and $Q^{c}$ are two binary relations on $\mathcal {X}(A)$,

• (c) $R^{c}=(Q^{c})^{-1}$,

• (d) $(S,T)\in R^{c}\Longleftrightarrow G^{-1}(S)\subseteq T\subseteq F^{-1}(S)$.

Lemma 7

The canonical frame of an IKt-algebra is an IKt-frame.

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)\in (\ge ^{c} \circ R^{c})$. Then there exists $U\in \mathcal {X}(A)$ such that $S\supseteq U$ and $G^{-1}(U)\subseteq T\subseteq F^{-1}(U)$. Consider the filter K generated by $T\cup G^{-1}(S)$. We will show that $K\subseteq F^{-1}(S)$. Assume $x\in K$. Then, there is $y\in T$ and $z\in G^{-1}(S)$ such that $y\wedge z\le x$. Hence, $y\le z\rightarrow x$ so $F(y)\le F(z\rightarrow x)$, and thus by (t7), we obtain that $F(y)\le G(z)\rightarrow F(x)$. Since $y\in T$ and $T\subseteq F^{-1}(S)$, we have that $G(z)\rightarrow F(x)\in S$. From this last statement and the fact that $S$ is a deductive system we have that $F(x)\in S$, i.e., $x\in F^{-1}(S)$. Therefore, $K\cap (A\setminus F^{-1}(S))=\emptyset$. Then by the Birkhoff–Stone theorem there is a prime filter $W\in \mathcal {X}(A)$ such that $W\subseteq F^{-1}(S)$, $G^{-1}(S)\subseteq T$ and $W\supseteq T$, i.e., $(S,T)\in (R^{c}\circ \ge ^{c})$. We can prove (K2) similarly to (K1).

$\square$

Definition 6

The complex algebra of an IKt-frame $(X,\le , R,R^{-1})$ is

$$\begin{aligned} \langle \mathcal {C}(X),G^{c},H^{c},F^{c},P^{c}\rangle , \end{aligned}$$

where $\mathcal {C}(X)$ is the complex algebra of the H-frame $(X,\le )$, $G^{c}(U)=[\le \circ R]U$, $H^{c}(U)=[\le \circ R^{-1}]U$, $F^{c}(U)$ $=\langle R\rangle U$ and $P^{c}(U)=\langle R^{-1}\rangle U$ for all $U\in \mathcal {C}(X).$

The following result is necessary to the proof of Theorem 3.

Lemma 8

$\mathcal {C}(X)$ is closed under the operations $G^{c}$, $H^{c}$, $F^{c}$ and $P^{c}$.

Proof

We will only prove that $\mathcal {C}(X)$ is closed under the operations $G^{c}$ and $F^{c}$, i.e., for any $U\in \mathcal {C}(X)$, $[\le ][\le \circ R]U=[\le \circ R]U$ and $[\le ]\langle R\rangle U=\langle R\rangle U$. In both cases, the inclusion $\subseteq$ follows from reflexivity of $\le$. First, we will prove that $[\le \circ R]U\subseteq [\le ][\le \circ R]U$. Let $x,y\in X$ such that $R([x))\subseteq U$ and $x\le y$. Let us prove that $R([y))\subseteq U$. Now assume $z\in R([y))$. Then, there is $w\in [y)$ such that $(w,z)\in R$. By the transitivity of the relation $\le$ we obtain that $x\le w$. Since $(w,z)\in R$ we can deduce that $z\in R([x))$ therefore $z\in U$. Next, we will prove that $\langle R\rangle U\subseteq [\le ]\langle R\rangle U$. Let $x\in \langle R\rangle U$ such that $x\le y$. Then, $R(x)\cap U\not =\emptyset$, i.e., there exists $w\in U$ such that $(x,w)\in R$. Therefore, from (K1) we can deduce that $(y,w)\in (R\circ \ge )$. From this last assertion there exists $z\in X$ such that $(y,z)\in R$ and $w\le z$. Since $U\in \mathcal {C}(X)$ we have that $z\in R(y)\cap U$. Therefore $y\in \langle R\rangle U$.

Theorem 3

The complex algebra of an IKt-frame is an IKt-algebra.

Proof

From the results established in Orłowska and Rewitzky (2007), $\mathcal {C}(X)$ is a Heyting algebra. Besides from Lemma 8, $\mathcal {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\subseteq [\le \circ R]\langle R^{-1}\rangle U$. Let $x,y\in X$ such that $x\in U$ and $y\in R([x))$. Then, there exists $z\in [x)$ such that $(z,y)\in R$. Since $U\in \mathcal {C}(X)$ we have that $z\in U$ and since $z\in R^{-1}(y)$, we obtain that $R^{-1}(y)\cap U\not =\emptyset$, that is, $y\in \langle R^{-1}\rangle U$. In a similar way, we can prove $U\subseteq [\le \circ R^{-1}]\langle R\rangle U$. Therefore (t3) holds.

Next, let us to prove that $\langle R^{-1}\rangle [\le \circ R]U\subseteq U$. Let $x\in \langle R^{-1}\rangle [\le \circ R]U$. Then, $R^{-1}(x)\cap [\le \circ R]U\not =\emptyset$. Hence, there exists $z\in R^{-1}(x)$ such that $R([z))\subseteq U$. Since $\le$ is reflexive we have that $(z,x)\in (\le \circ R)$, i.e., $x\in R([z))$. Therefore $x\in U$. In a similar way, we can prove that $\langle R\rangle [\le \circ R^{-1}]\subseteq U$. Then (t6) holds.

Finally, let us to prove that (t7) holds. Suppose that $x\in \langle R\rangle (U\rightarrow ^{c}V)$, $x\le z$ and $z\in [\le \circ R]U$. Let us to prove that $z\in \langle R\rangle V$, i.e., $R(z)\cap V\not =\emptyset$. Since $x\in \langle R\rangle (U\rightarrow ^{c}V)$ then there exists $y \in R(x)\cap (U\rightarrow ^{c}V)$, $z\ge x$, $(x,y)\in R$, and so from (K1) we have that $(z,v)\in R$ and $v\ge y$ for some $v\in X$. Since $v\in R(z)\subseteq (\le \circ R)(z)\subseteq U$, $y\le v$ and $y\in (U\rightarrow ^{c}V)$ then $v\in V$. Therefore, $R(z)\cap V\not =\emptyset$. In a similar way, we can prove $\langle R^{-1}\rangle (U\rightarrow ^{c}V)\subseteq [\le \circ R^{-1}]U\rightarrow ^{c}\langle R^{-1}\rangle V$. $\square$

We now show that the embedding $h:A\rightarrow \mathcal {C}(\mathcal {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\in A$,

• (a) $h(G(a))=G^{c}(h(a))=[\le ^{c}\circ R^{c}]h(a)$,

• (b) $h(H(a))=H^{c}(h(a))=[\le ^{c}\circ Q^{c}]h(a)$,

• (c) $h(F(a))=F^{c}(h(a))=\langle R^{c}\rangle h(a)$,

• (d) $h(P(a))=P^{c}(h(a))=\langle Q^{c}\rangle h(a)$.

Proof

We will only prove (a) and (c).

(a): Let $G(a)\in S$ and let us to prove that $(\le ^{c}\circ R^{c})(S)\subseteq h(a)$. Suppose that $T\in (\le ^{c}\circ R^{c})(S)$. Then there exists $W\in \mathcal {X}(A)$ such that $S\subseteq W$ and $G^{-1}(W)\subseteq T\subseteq F^{-1}(W)$. Since $a\in G^{-1}(S)$ and $S\subseteq W$ we have that $a\in G^{-1}(W)$. Hence, $a\in T$, i.e., $T\in h(a)$. On the other hand, we show that, for any $a\in A$, if $G(a)\notin S$ then $S\notin [\le ^{c}\circ R^{c}]h(a)$. Since $\le$ is reflexive, it suffices to show that, if $G(a)\notin S$ then $S\notin [R^{c}]h(a)$. Assume $G(a)\notin S$ and $F(b)\notin S$. Then $a\notin G^{-1}(S)$ and $b\notin F^{-1}(S)$. Consider the ideal $\downarrow a\cap \downarrow b$, where $\downarrow x$ denotes the ideal generated by the single set $\{x\}$. Then,

$$\begin{aligned}&\!\!\!(\downarrow a\cap \downarrow b)\cap G^{-1}(S)=\downarrow a\cap G^{-1}(S)\\&\quad =\emptyset \hbox { and} G^{-1}(S) \hbox { is a filter}. \end{aligned}$$

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

$$\begin{aligned} G^{-1}(S)\subseteq T\quad \hbox {and}\quad a\notin T\quad \hbox {and}\quad b\notin T. \end{aligned}$$

Hence, $G(a)\notin S$ implies, for some $T\in \mathcal {X}(A)$, $a\notin T$ and $T\subseteq F^{-1}(S)$ and if $b\notin F^{-1}(S)$ then $b\notin T$.

(c): For any $a\in A$ and for any $S\in \mathcal {X}(A)$, we show that

$$\begin{aligned}&\!\!\!\!F(a)\in S \hbox { iff there exists} T\in \mathcal {X}(A) \hbox { such that} \\&\quad G^{-1}(S)\subseteq T\subseteq F^{-1}(S)\quad \hbox {and}\quad a\in T. \end{aligned}$$

The right-to-left implication is trivial. Assume $F(a)\in S$ and $G(b)\in S$. Then $a\in F^{-1}(S)$ and $b\in G^{-1}(S)$. Consider the filter $\uparrow a\cap \uparrow b$, where $\uparrow x$ denotes the filter generated by the single set $\{x\}$. We have that

$$\begin{aligned}&\!\!\!(\uparrow a\cap \uparrow b)\cap (A\setminus F^{-1}(S))=\uparrow a\cap (A\setminus F^{-1}(S))\\&\quad =\emptyset \quad \hbox {and}\quad A\setminus F^{-1}(S) \hbox { is an ideal}. \end{aligned}$$

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

$$\begin{aligned} T\cap (A\setminus F^{-1}(S))=\emptyset \quad \hbox {and}\quad a\in T\quad \hbox {and}\quad b\in T. \end{aligned}$$

Hence $a\in F^{-1}(S)$ implies, for some $T\in \mathcal {X}(A)$, $T\subseteq F^{-1}(S)$ and $a\in T$ and if $b\in G^{-1}(S)$ then $b\in T$. $\square$

We now show that the order-embedding $k:X\rightarrow X(\mathcal {C}(X))$, defined in Sect. 2, preserves the relation $R$, i.e.,

Lemma 10

Let $(X,\le ,R,R^{-1})$ be an IKt-frame and let $x,y\in X$. Then,

$$\begin{aligned} (x,y)\in R \hbox { if and only if } k(x),k(y))\in R^{c}. \end{aligned}$$

Proof

Assume $(x,y)\in R$. We need to show that

$$\begin{aligned} (k(x),k(y))\in R^{c}. \end{aligned}$$

Note that

• $(k(x),k(y))\in R^{c}$ iff $[\le \circ R]^{-1}(k(x))\subseteq k(y)$ and

• $k(y)\subseteq \langle R\rangle ^{-1}k(x)$

• iff for all $U\in \mathcal {C}(X)$, $x\in [\le \circ R]U$ implies $y\in U$ and for all $U\in \mathcal {C}(X)$, $y\in U$ implies $x\in \langle R\rangle U$.

Take any $U\in \mathcal {C}(X)$ such that $x\in [\le \circ R]U$. Then, since $(x,y)\in R$ and $R\subseteq (\le \circ R)$, we have that $y\in U$. Take any $U\in \mathcal {C}(X)$ such that $y\in U$. Then, since $(x,y)\in R$ we have that $x\in \langle R\rangle U$. On the other hand, assume $(k(x),k(y))\in R^{c}$. Then, $[\le ]\{y\}\in \mathcal {C}(X)$. So $x\in \langle R\rangle [\le ]\{y\}$. From this last statement and (K1) we can deduce that $x\in [\le ]\langle R\rangle \{y\}$. Therefore, by reflexivity of $\le$ we have that $x\in \langle R\rangle \{y\}$, i.e., $(x,y)\in R$, as required. $\square$

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

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.

7 A general construction of tense operators

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řik (2012) and Chajda and Paseka (2012). Let $\mathcal {A}=\langle A,\vee ,\wedge ,\rightarrow ,0,1\rangle$ be a Heyting algebra and $A^X$ the set of all the functions of $X$ in $A$. It is easy to see that $\langle A^{X},\vee ,\wedge ,\rightarrow ,0,1\rangle$ is a Heyting algebra, where the operations $\vee ,\wedge ,\rightarrow$ are defined pointwise and besides $0(x)=0$, $1(x)=1$ for each $x\in X$.

Taking into account the above statements, we can formulate the following theorem:

Theorem 5

Let $\mathcal {A}=\langle A,\vee ,\wedge ,\rightarrow ,0,1\rangle$ be a complete Heyting algebra and $(X,\le )$ a H-frame. Define the operators $G$, $H$, $F$ and $P$ on $A^{X}$ as follows:

$$\begin{aligned} G(p)(x)=\bigwedge \limits _{y\in [x)} \{p(y)\},\,\,\,\,\,H(p)(x)=\bigwedge \limits _{y\in (x]} \{p(y)\}, \end{aligned}$$

$$\begin{aligned} F(p)(x)=\bigvee \limits _{y\in [x)} \{p(y)\},\,\,\,\,\,P(p)(x)=\bigvee \limits _{y\in (x]} \{p(y)\}. \end{aligned}$$

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)\le F(p)$ for all $p\in A^{X}$,

• (b) $H(p)\le P(p)$ for all $p\in A^{X}$.

Proof

It is evident to prove axioms (t1) and (t4). Since $\mathcal {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:

$$\begin{aligned} GP(p)(x)=\bigwedge \limits _{y\in [x)}\left\{ \bigvee \limits _{z\in (y]}\{p(z)\}\right\} . \end{aligned}$$

On the other hand, it is clear that

$$\begin{aligned} p(x)\le \bigvee \limits _{z\in (y]}\{p(z)\},\,\, \hbox {for each}\,\, y\in [x). \end{aligned}$$

(1)

From 1 and the definition of infimum, we have that

$$\begin{aligned} p(x)\le \bigwedge \limits _{y\in [x)}\left\{ \bigvee \limits _{z\in (y]}\{p(z)\}\right\} \!. \end{aligned}$$

Thus, $p\le GP(p)$. Analogously, it is proved that $p\le HF(p)$. Therefore, (t3) is verified.

From the definition of $P$ and $G$, we have that

$$\begin{aligned} PG(p)(x)=\bigvee \limits _{y\in (x]}\left\{ \bigwedge \limits _{z\in [y)}\{p(z)\}\right\} \!. \end{aligned}$$

In addition, we verify that

$$\begin{aligned} \bigwedge \limits _{z\in [y)}\{p(z)\}\le p(x),\,\, for each \,\, y\in (x]. \end{aligned}$$

(2)

From 2 and the definition of supremum, we have that

$$\begin{aligned} \bigvee \limits _{y\in (x]}\left\{ \bigwedge \limits _{z\in [y)}\{p(z)\}\right\} \le p(x). \end{aligned}$$

Hence, $PG(p)\le p$. Analogously, it is proved that

$$\begin{aligned} FH(p)\le p. \end{aligned}$$

Therefore, (t6) is verified. Finally, we verify (t7). Let $y\in (x]$, then

$$\begin{aligned} \bigwedge \limits _{z\in (x]}\{p(z)\}\wedge (p(y)\rightarrow q(y))&\le p(y)\wedge (p(y)\rightarrow q(y))\\&\le q(y)\\&\le \bigvee \limits _{z\in (x]}\{q(z)\}. \end{aligned}$$

From the latter inequality, we have that

$$\begin{aligned} (p(y)\rightarrow q(y))\le \bigwedge \limits _{z\in (x]}\{p(z)\}\rightarrow \bigvee \limits _{z\in (x]}\{q(z)\}, \end{aligned}$$

for each $y\in (x].$

Hence,

$$\begin{aligned} \bigvee \limits _{y\in (x]} (p(y)\rightarrow q(y))\le \bigwedge \limits _{z\in (x]}\{p(z)\}\rightarrow \bigvee \limits _{z\in (x]}\{q(z)\}, \end{aligned}$$

that is, $F(p\rightarrow q)\le G(p)\rightarrow F(q)$. Similarly, $P(p\rightarrow q)\le H(p)\rightarrow P(q)$ is proved. Therefore, $(A^{X},G,H,F,P)$ is an IKt-algebra. Besides, it is obvious that $G(0)=0=H(0)$ and that $F(1)=1=P(1)$. On the other hand, by the reflexivity of the relation $\le$, we have that

$$\begin{aligned} G(p)(x)=\bigwedge \limits _{y\in [x)}\{p(y)\}\le p(x)\le \bigvee \limits _{y\in [x)}\{p(y)\}=F(p)(x). \end{aligned}$$

Therefore, $G(p)\le F(p)$. In a similar way we can prove (b). $\square$

The following example is an application of the previous theorem.

Example 4

Let $(X,\le )$ be a H-frame, where $X=\{1,2\}$ and $\le$ denotes the natural order. Let $A$ be the Heyting algebra three-element chain, i.e., $A=\{0,a,1\}$, where $0\le a\le 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:

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)

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)
(1,0)	(0,0)	(1,0)	(1,0)	(1,1)
(a,a)	(a,a)	(a,a)	(a,a)	(a,a)
(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)

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 $(\mathcal {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

• (D3) $G(x),H(x)\in D$ for each $x\in D$.

We will prove that the IKt-congruence lattice

$Con_{IKt}(A)$ is isomorphic to the lattice of all tense deductive systems $\mathcal {D}_{IKt}(A)$.

Lemma 11

Let $(\mathcal {A},G,H,F,P)$ be an IKt-algebra. Then

$$\begin{aligned} Con_{IKt}(A)=\{R(D):D\in \mathcal {D}_{IKt}(A)\}, \end{aligned}$$

where $R(D)$ is defined as (C1) from the Sect. 2.

Proof

Let $D\in \mathcal {D}_{IKt}(A)$, since $A$ is a Heyting algebra and $D$ a deductive system of $A$, from (C1), we know that $R(D)\in Con(A)$. Let us prove that $R(D)$ preserves the tense operators. Let $(x,y)\in R(D)$ since $D$ is a tense deductive system, $G(x\rightarrow y), G(y\rightarrow x)\in D$. Then by (t2)$^{\prime }$, we obtain that $G(x)\rightarrow G(y), G(y)\rightarrow G(x)\in D$, i.e., $(G(x),G(y))\in R(D)$. On the other hand, since $G(x\rightarrow y), G(y\rightarrow x)\in D$, applying (t11), we have that $F(x)\rightarrow F(y), F(y)\rightarrow F(x)\in D$; i.e., $(F(x),F(y))\in R(D)$. Similarly, it is proved that $R(D)$ preserves $H$ and $P$. Conversely, let $\theta \in Con_{IKt}(A)$, then $\theta \in Con(A)$. From the obtained results in the Sect. 2, we have that $[1]_\theta$ is a deductive system of $A$ and $R([1]_\theta )=\theta$. Besides, from the hypothesis and (T1) we have that $(G(x),1)\in \theta$ and $(H(x),1)\in \theta$ whenever $(x,1)\in \theta$, i.e., $[1]_\theta \in \mathcal {D}_{IKt}(A)$, which completes the proof. $\square$

Taking into account the established results in (C2) and Lemma 11, we obtain:

Theorem 6

Let $(\mathcal {A},G,H,F,P)$ be an IKt-algebra. Then, the lattices $Con_{IKt}(A)$ and $\mathcal {D}_{IKt}(A)$ are isomorphic.

We will define the operator $d$ on an IKt-algebra $(\mathcal {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ţă (2011) for tense $\theta$-valued Łukasiewicz–Moisil algebras, respectively. We will use the properties of $d$ to characterize the simple and subdirectly irreducible IKt-algebras.

Definition 8

Let $(\mathcal {A},G,H,F,P)$ be an IKt-algebra. We define the unary operation $d$ on $A$ by $d(x)=G(x)\wedge x\wedge H(x)$, for each $x\in A$. For each $n\in \omega$ we define $d^{n}(x)$ by : $d^{0}(x)=x$, $d^{n+1}(x)=d(d^{n}(x)).$

Lemma 12

Let $(\mathcal {A},G,H,F,P)$ be an IKt-algebra. Then for any $n\in \omega$, the following holds:

• (a) $d^{n}(1)=1$ and $d^{n}(0)=0$,

• (b) $d^{n+1}(x)\le d^{n}(x)$,

• (c) $d^{n}(x\wedge y)=d^{n}(x)\wedge d^{n}(y)$,

• (d) $x\le y$ implies $d^{n}(x)\le d^{n}(y)$,

• (e) $D\in \mathcal {D}_{IKt}(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 ($\Rightarrow$). 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\in D$. Then $d(x)=G(x)\wedge x\wedge H(x)$ and it follows that $d(x)\in D$. ($\Leftarrow$) We assume that $D$ is a filter closed under $d$. We must prove that $D$ is closed under $G$ and $H$. Let $x\in D$. Then $d(x)\le G(x)$ and $d(x)\le H(x)$. It follows that $G(x),H(x)\in D$. $\square$

Proposition 3

Let $(\mathcal {A},G,H,F,P)$ be an IKt-algebra. The tense deductive system $\langle a\rangle$ of $(\mathcal {A},G,H,F,P)$ generated by $\{a\}$ has the following form:

$$\begin{aligned} \langle a\rangle =\{x\in A: d^{n}(a)\le x,\,\, \hbox {for some}\,\, n\in \omega \}. \end{aligned}$$

Proof

We denote by $\Sigma$ the right-hand side of the previous equality. $1\in \Sigma$, since $d^{0}a=a\le 1$. Let $x\in \Sigma$ so that $x\le y$. Hence, there exists $n\in \omega$ such that $d^{n}(a)\le x$. Since $x\le y$, we have that $d^{n}(a)\le y$, i,e., $y\in \Sigma$. Next, let us prove that $x\wedge y\in \Sigma$, for $x,y\in \Sigma$. Let $x,y\in \Sigma$, there exists $n,m\in \omega$ such that $d^{n}(a)\le x$ and $d^{m}(a)\le y$. If we take $k=n+m$, from Lemma 12, it is verified that $d^{k}(a)\le x$ y $d^{k}(a)\le y$, from which $d^{k}(a)\le x\wedge y$, that is, $x\wedge y\in \Sigma$. From $\mathrm{(b)}$ of Lemma 12, we obtain that $\Sigma$ is closed under the operator $d$. Therefore, from $\mathrm{(e)}$ of Lemma 12, $\Sigma$ is a tense deductive system. The rest of the proof is obvious. $\square$

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 $(\mathcal {A},G,H,F,P)$ the following are equivalent:

• (i) $(\mathcal {A},G,H,F,P)$ is a simple IKt-algebra,

• (ii) $(\mathcal {A},G,H,F,P)$ satisfies the property:

(A) For any $a\in A\setminus \{1\}$ there exists $n\in \omega$ such that $d^{n}(a)=0$.

Proposition 5

For any IKt-algebra $(\mathcal {A},G,H,F,P)$ the following are equivalent:

• (i) $(\mathcal {A},G,H,F,P)$ is a subdirectly irreducible IKt-algebra,

• (ii) $(\mathcal {A},G,H,F,P)$ satisfies the property: (B) There exists $b\in A\setminus \{1\}$, such that for any $a\in A\setminus \{1\}$ there exists $n\in \omega$ such that $d^{n}(a)\le 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 $(\mathcal {A},G,H,F ,P)$ of the Example 2. It is plain that $\mathcal {A}$ is not a subdirectly irreducible Heyting algebra. On the other hand, taking into account (B) of the Proposition 5, we can check that $(\mathcal {A},G,H,F,P)$ is a subdirectly irreducible IKt-algebra.