On the Decidability of Intuitionistic Tense Logic without Disjunction

1 Introduction

Intuitionistic logic [Dalen, 1986] and its modal expansions [Servi, 1984; Simpson, 1994; Wolter and Zakharyaschev, 1999] have been widely studied and applied to the area of computer science and artificial intelligence [Boudou et al., 2019], where they are regarded as a natural framework to reason about dynamic processes [Pearce, 1996; Leone et al., 2006; Balbiani and Di´eguez, 2016]. In particular, [Pearce, 1996] showed that the stable model semantics [Gelfond and Lifschitz, 1988] for normal and disjunctive logic program can be characterized by a two points Kripke model for intuitionistic modal logic, and that DLV system for knowledge representation and reasoning [Leone et al., 2006] is one of the known solvers for the stable model semantics. Besides, intuitionistic temporal (tense) logics have also been applied to reactive systems [Maier, 2004], topological dynamics [Fern´andez-Duque, 2016], etc.

Implicative semi-lattices (also known as Brouwerian semilattices), introduced by William C. Nemitz [Nemitz, 1965] in the context of an algebraic approach to non-classical logics, are algebraic reducts of Heyting algebras, and their logical and algebraic theory has been widely investigated [Nemitz and Whaley, 1971; Nemitz and Whaley, 1973; Wronski, 1973; K¨ohler, 1981]. The interest in implicative semi-lattices stems from the fact that, in certain respects, they display a better behaviour than Heyting algebras, as witnessed by results such as [Diego, 1966], which employ algebraic methods to establish logically relevant properties. Specifically, [Diego, 1966] showed that the variety of implicative semi-lattices is locally finite. Based on this result, C. McKay [Mckay, 1968] proved that all intermediate logics which are axiomatic extensions of the logic of implicative semi-lattices have the finite model property (FMP), which implies that these logics are decidable.

∗ Contact Author

In this paper, we consider the natural algebraic semantics of the disjunction-free fragment of intuitionistic tense logic (in the sense of W. B. Ewald [Ewald, 1986] and [Figallo and Pelaitay, 2014]). The algebras of this class, which we refer to as tense implicative semi-lattices (or ISt-algebras), are obtained by expanding implicative semi-lattices with two pairs of adjoint tense operators ♦, ■ (or F, H) and ♦, □ (P, G). The decidability and the FMP of intuitionistic tense logic and its fragments are long term open questions.

The main contribution of the present paper is to show that the disjunction-free fragment of intuitionistic tense logic has the FMP, using methods from algebraic proof theory ([Ciabattoni et al., 2012]). Having the FMP and the finite axiomatizability imply that the disjunction-free fragment of intuitionistic tense logic is decidable. In fact, the disjunction-free fragment of intuitionistic tense logic gives a general logical base for different intuitionisitic tense logics, for example the logic used in [Pearce, 1996]. The Gentzen-style sequent calculus and the method of constructing finite models proposed in this paper can be useful to provide some ideas for constructing automated deductions for different intuitionistic tense logics, and to give more efficient ways of implementing related dynamic processes in artificial intelligence.

The paper is organized as follows. In Section 2, we collect relevant preliminaries. In Section 3, we introduce sequent calculi for intuitionistic tense logic and the logic of IStalgebras both of which enjoy cut elimination and subformula property, and show that intuitionistic tense logic is a conservative extension of the logic of ISt-algebras in a proof theoretic way. In Section 4, we show that the logic of ISt-algebras has the FMP and the decidability. Finally, we mention some prospects for future work in Section 5.

2 Preliminaries

In this section, we recall some algebraic definitions and results which will be used in the rest of the paper.

Definition 1. ([Figallo and Pelaitay, 2014]) An intuitionistic tense algebra (or IKt-algebra) is a structure A = (A, ∧, ∨, → , ♦,□, ♦,■, 0, 1), where A = (A, ∧, ∨,→, 0, 1) is a Heyting algebra, and ♦, □, ♦, ■ are unary operators (called tense operators) on A satisfying the following conditions: for all a, b ∈ A,

It is not difficult to show that: (1) if ♦(♦a ∧ b) ≤ c, then a ∧ ♦b ≤ c and (2) if ♦(♦a ∧ b) ≤ c, then a ∧ ♦b ≤ c hold in IKt-algebras.

Definition 2. ([Nemitz, 1965]) An implicative semi-lattice is a structure S = (L, ≤, ∧,→) in which L is a nonempty set, ≤ is a partial order on L, ∧ is the greatest lower bound with respect to ≤, and → is a binary operator in L such that for any elements a, b and c ∈ L,

An implicative semi-lattice is bounded if it has the least element 0.

Finite implicative semi-lattices (are complete lattices, and hence) are always bounded.

Proposition 3. ([Nemitz and Whaley, 1973, Theorem 2.1]) The variety of implicative semi-lattices is locally finite.

The following definition identifies the main algebraic environment of the present paper.

Definition 4. A tense implicative semi-lattice (ISt) is a bounded implicative semi-lattice endowed with unary operators ♦, □, ♦, ■ satisfying all conditions (t1)-(t7) except (t5) in Definition 1.

In what follows, we use ISt and IKt to denote the variety of IKt-algebras and the class of tense implicative semi-lattices repectively, and IKt and ISt to denote the logic of IKt and the logic of ISt respectively.

3 Sequent Calculi for IKt and ISt

In this section, we introduce sequent calculi for the logic of IKt and the logic of ISt. Both calculi enjoy cut elimination and subformula property. We show that the logic of IKt is a conservative extension of the logic of ISt.

Definition 5. Fix a denumerable set Var of propositional variables. The set of formulae (terms) F is defined recursively as follows:

where p ∈ Var.

Definition 6. Let (, ) ◦ and · be structure operations for ∧, ♦ and ♦ respectively. The set of structures FS is defined inductively as follows:

A structure is an element in FS. In what follows, we use Γ, ∆ with or without subscripts to denote structures. A sequent is an expression of the form Γ ⇒ α where Γ is a structure and α is a formula. A context is a structure Γ[-] with a designated position [-] which can be filled with a structure. In particular, a single position [-] is a context. Let Γ[∆] be structure obtained from Γ[-] by substituting ∆ for [-]. By f(Γ) we denote the formula obtained from Γ by replacing all structure operations by their corresponding formula connectives.

Definition 7. The Gentzen sequent calculus GIKt for IKt consists of the following axiom and rules:

1. Axiom and Constant rules:

The Gentzen sequent calculus GISt for ISt is obtained from GIKt by removing (∨L) and (∨R).

This style of sequent calculi is first introduced by M. Moorgart [Moortgat, 1996] and the rules (Wk◦) and (Wk·) are obtained by modifying S5 rule in modal Lambek calculus in [Lin and Liu, 2012].

A sequent Γ ⇒ β is provable in G where G ∈ {GISt, GIKt}, notation ⊢G Γ ⇒ β, if there is a derivation of Γ ⇒ β in G. We write ⊢G α ⇔ β if ⊢G α ⇒ β and ⊢G β ⇒ α.

Lemma 8. The following sequents are derivable in GIKt (and in GISt except (5)). For any α, β ∈ F,

1. □⊤⇔⊤ and ■⊤⇔⊤;
2. □(α∧ β) ⇔□α∧□β and ■(α∧ β) ⇔■α∧■β;
3. α⇒■♦α and α⇒□♦α;
4. ♦⊥⇔⊥ and ♦⊥⇔⊥;
5. ♦(α∨ β) ⇔♦α∨♦β and ♦(α∨ β) ⇔♦α∨♦β;
6. ♦■α⇒α and ♦□α⇒α;
7. ♦(α→ β) ⇒□α→♦β and ♦(α→ β) ⇒■α→♦β.

Proof. Due to space limitations, we only provide the proof for the first inequality of (7). Others can be checked easily and we omit the proofs here.

Theorem 9. GISt and GIKt are sound and complete with respect to ISt and IKt respectively.

Proof. The soundness can be proved by the standard way and Lemma 8. We only prove the completeness part here. Let |α| = {β| ⊢GISt α ⇔ β} and A := {|α| | α ∈ F}. Let us define ∧, →, ♦, □, ♦, ■ on A as follows:

It is clear that A = (A, ∧,→, ♦,□, ♦,■, |⊤|, |⊥|) is an ISt by Lemma 8. The order is defined as the lattice order, that is, |α1| ≤ |α2| iff |α1| ∧ |α2| = |α1|. Thus |α1| ≤ |α2| iff ⊢GISt α1 → α2. Define an assignment σ : Var → A such that σ(p) = |p|. By induction on the complexity of formula, one shows that σ(γ) = |γ| for any formula γ. Hence ̸⊢GISt α ⇒ β implies ̸|=A,σ σ(α) ≤ σ(β). Consequently ̸⊢GISt α ⇒ β implies ̸|=ISt α ⇒ β, This completes the proof. The proof of the completeness of GISt is similar, and hence is omitted.

The following Lemma can be shown by a straightforward induction on the complexity of ∆ and on the height of the derivation tree for Γ[∆, ∆] ⇒ β.

Lemma 10. If ⊢G Γ[∆,∆] ⇒ β is derivable without any application of (Cut) where G ∈ {GISt, GIKt}, then ⊢G Γ[∆] ⇒ β is derivable without any application of (Cut).

Theorem 11 (Cut elimination). If ⊢G Γ ⇒ β where G ∈ {GISt, GIKt}, then ⊢G Γ ⇒ β without any application of (Cut).

Proof. Assume that there is a subderivation of Γ ⇒ β ended with an application of (Cut) as follows:

It suffices to show that if ∆ ⇒ α and Σ[α] ⇒ θ are both provable in G without any applications of (Cut), then Σ[∆] ⇒ θ is provable in G without any applications of (Cut). We proceed by induction on (I) the complexity of (Cut) formula α. In each case we proceed by induction on (II) the left Cut rank i.e. the height of the proof of the left premise of (Cut) and (III) the right Cut rank i.e. the height of the proof of the right premise of (Cut). Assume that ∆ ⇒ α is obtained by the application of a rule which is denoted by (Rl) and Σ[α] ⇒ θ is obtained by the application of a rule which is denoted by (Rr). It is easy to prove the claim holds if α is not introduced by (Rl), or not introduced by (Rr) and (Rr) is not (Conf), or α are introduced both by (Rl) and (Rr), we refer the details to the standard cut elimination proofs. We only consider the following relevant cases. Without loss of generality, we omit the application of (Ex), (As1) and (As2), and assume that (, ) is associative and commutative.

α is introduced by (Rl). Assume that Σ[α] ⇒ θ is obtained from Σ[αn ] ⇒ θ by n-1 times of (Conf) such that Σ[αn ] is not obtained from a Conf rule. Suppose that Σ[αn ] is obtained by rule (R). Obviously if n = 1 then Rr = R. Let the derivation ends with

We consider the following subcases according to (R). (1) (R) is (Con◦) or (Con·). We consider the following two subcases. (i) Suppose the derivation ends with

Let h(Σ′ [◦(Σ1[αn ]), ◦Σ2] ⇒ θ) = l. Then right Cut rank is l + n. The derivation can be transformed into

Thus the new right Cut rank is l+n-1. Thus by induction hypothesis (III) the claim holds. (ii) Suppose the derivation ends with

such that 0 ≤ n1 + n2 ≤ n. Then the derivation can be transformed into its equivalent derivation as follows

Hence, in the new derivation, each cut can be eliminated by the analogous argument used in (i).

(2) (R) is (WK◦) or (WK·). We consider the following two subcases. First suppose the derivation ends with

This case is similar to 1(i). Second suppose the derivation ends with

This case is similar to 1(ii).

(3) There are three subcases. (i) If (R) is a structural rule which is not considered in (1) and (2), or a constant rule, then the proof is quite similar to 1(i). (ii) If (R) is a connective rule which is not for α, then one may first apply (Conf) to the premise(s) of (R), and then applying (Cut) to ∆ ⇒ α and the conclusion of (Conf), finally applying (R) to the conclusion of (Cut). Clearly the right Cut rank is smaller than the original one. (iii) If (R) is a connective rule for α, then one may first apply (Conf) to the premise(s) of (R), and then applying (Cut) to ∆ ⇒ α and the conclusion of (Conf), clearly the right Cut rank is smaller than the original one. Finally, applying (Cut) to the premise(s) of (Rl) and the conclusion of the previous (Cut). Clearly the complexity of this cut formula is smaller. Therefore, the claim holds by induction hypothesis (III) and (I).

Corollary 12. If ⊢G Γ ⇒ β where G ∈ {GISt, GIKt}, then there is a derivation of Γ ⇒ β such that all formulae appearing in the derivation are subformulae of formulae in Γ ⇒ β.

Notice that combining Theorem 11 with Corollary 12 doesn't imply decidability since there is the rule (Conf) in both GISt and GIKt. However, it straightforwardly follows that:

Proposition 13 (Conservativity). Let Γ ⇒ β be a IStsequent, then ⊢GISt Γ⇒ β iff ⊢GIKt Γ⇒ β.

4 The Decidability of ISt

In this section we prove that the finite model property (FMP) holds for ISt, that is, we will show that if ̸⊢GISt α ⇒ β, then there exits a finite tense implicative semi-lattice M s.t. M ̸|= α ⇒ β. As is well known [Harrop, 1956], the FMP and the finite axiomatizability of ISt imply that ISt is decidable. The fact that ISt is finitely axiomatizable follows from the finite axiomatizability of IKt [Ewald, 1986]. The proof strategy is analogous to the one used in [Greco et al., 2018], and is illustrated by the following diagram.

where α ⇒ β is an ISt-sequent, Q is a finite IKt-algebra, and A is a ∨-reduct of Q. The vertical equivalence on the right-hand side of the diagram holds by Proposition 13. The horizontal implication follows from Theorem 26 and Theorem 9. The proof is complete by appealing to Theorem 29.

Let T be a set of ∨-free formulae closed under subformulae, ∧ and →. Define T ∗ be the ∨-closure of T, then for any α ∈ T ∗ , α = ∨ αi where αi ∈ T. Define α ∧∗ β := ∨(αi ∧ βj). Notice that α ∧∗ β ∈ T ∗ for any α, β ∈ T ∗ . Using (Cut), the following lemma straightforwardly follows:

Lemma 14. If ⊢GIKt Γ[α1 ∨α2] ⇒ β, then ⊢GIKt Γ[α1] ⇒ β and ⊢GIKt Γ[α2] ⇒ β.

Lemma 15. If ⊢GIKt α, β ⇒ θ where α, β ∈ T ∗ , then ⊢GIKt α ∧∗ β ⇒ θ.

Proof. Let α = α1 ∨ . . . ∨ αn and β = β1 ∨ . . . ∨ βm where αi, βj ∈ T for all 1 ≤ i ≤ n and 1 ≤ j ≤ m. By Lemma 14 and assumption, one obtains ⊢GIKt αi, βj ⇒ θ for any 1 ≤ i ≤ n and 1 ≤ j ≤ m. Thus by (∧L) and (∨L), one obtains ⊢GIKt ∨ij (αi ∧ βj) ⇒ θ, whence ⊢GIKt α ∧∗ β ⇒ θ.

In what follows, let T- or T ∗ -sequent be the sequent in which all formulae occurring are from T or T ∗ respectively and let sf(T) or sf(T ∗ ) be the set of structures which is constructed from T or T ∗ formulae.

Lemma 16. For any T ∗ -sequent Γ ⇒ β, if ⊢GIKt Γ ⇒ β and Γ ∈ sf(T), then there is a γ ∈ T such that ⊢GIKt Γ ⇒ γ and ⊢GIKt γ ⇒ β.

Proof. We proceed by induction on the length of the cut free proof of Γ ⇒ β. By Corollary 12, we assume that this cut free derivation of Γ ⇒ β is a T ∗ -derivation. Suppose that Γ ⇒ β is obtained by rule (R). If (R) is a right rule except (∨R), then β ∈ T is a required interpolant. Let (R) be (∨R). Assume that the premise is Γ ⇒ β1 and β = β1 ∨ β2. Then by induction hypothesis, there is a γ ∈ T such that ⊢GIKt Γ ⇒ γ and ⊢GIKt γ ⇒ β1. Hence by (∨R), one obtains ⊢GIKt γ ⇒ β1 ∨ β2. Let (R) be a left rule. Since Γ ∈ sf(T), (R) can not be (∨L). Therefore one obtains the required interpolant by induction hypothesis and rule (R). For instance let (R) be (→ L) (Other cases can be treated similarly). Assume that the premise are ∆ ⇒ α1 and Γ′ [α2] ⇒ β where Γ = Γ′ [∆, α1 → α2]. Obviously Γ′ [α2] ∈ sf(T). By induction hypothesis, one obtains ⊢GIKt Γ′ [α2] ⇒ γ and ⊢GIKt γ ⇒ β for some γ ∈ T. Hence by (→ L), one obtains ⊢GIKt Γ′ [∆, α1 → α2] ⇒ γ, hence γ is the required formula.

Definition 17 (Order on sf(T ∗ )). Define ≤ on sf(T ∗ ) as follows: ∆1 ≤ ∆2 iff for any α ∈ T ∗ , if ⊢GIKt ∆2 ⇒ α, then ⊢GIKt ∆1 ⇒ α.

Proposition 18. Let ∆1 ∼ ∆2 be ∆1 ≤ ∆2 and ∆2 ∼ ∆1, then ∼ is an equivalent relation.

Let JαK := {∆ ∈ sf(T ∗ )|α ∼ ∆} for any α ∈ T ∗ .

Lemma 19. Let F be a finite set and T be the subformula, ∧,→ closure of F. Define |T| = {JαK : α ∈ T} and |T ∗ | = {JαK : α ∈ T ∗ }, then both |T| and |T ∗ | are finite.

Proof. Since F is finite, |F| = {JαK : α ∈ |F|} is finite. Proposition 3 implies that the implicative semi-lattice K generated by |F| is finite. Because the domain of K is |T| = {JαK : α ∈ T}, hence |T| is finite. Therefore, |T ∗ | is finite by construction.

We let E(T) = {α | JαK ∈ |T |} and E(T ∗ ) = {α | JαK ∈ |T ∗ |}, then by Lemma 19, E(T) and E(T ∗ ) are both finite. For the rest of the paper, we let T and T ∗ are constructed from a finite formula set.

Lemma 20. For any α ∈ T, there is β ∈ T s.t. ⋆α ∼ β where ⋆ ∈ {◦, ·}.

Proof. Given a formula θ ∈ T ∗ . Suppose that ⊢GIKt ⋆α ⇒ θ. Then by Lemma 16, there is a γ ∈ E(T) such that ⊢GIKt ⋆α ⇒ γ and ⊢GIKt γ ⇒ θ. Since E(T) is finite, let {γ1, . . . , γn} be the set of all interpolants for all θ ∈ T ∗ such that ⊢GIKt ⋆α ⇒ θ. Let β = γ1 ∧ . . . ∧ γn. Then β ∈ T. Clearly by (∧R) and (∧L), one obtains (1) ⊢GIKt ⋆α ⇒ β and (2) ⊢GIKt β ⇒ θ. From (2) one obtains β ≤ ⋆α. Suppose that ⊢GIKt β ⇒ π for any π ∈ T ∗ . Applying (Cut) to (1) and the assumption, one obtains ⊢GIKt ⋆α ⇒ π. Hence ⋆α ≤ β.

Lemma 21. For any α ∈ T ∗ , there is β ∈ T ∗ s.t. ⋆α ∼ β where ⋆ ∈ {◦, ·}.

Proof. If α ∈ T, then the claim holds by Lemma 20. Let θ ∈ T ∗ such that ⊢GIKt ⋆α ⇒ θ. Let α ∈ T ∗ \ T. Then α = α1 ∨. . .∨αn. By Lemma 14 one obtains ⊢GIKt ⋆αi ⇒ θ for all 1 ≤ i ≤ n. Since αi ∈ T, by Lemma 20 there is a βi ∈ T such that βi ∼ ⋆αi. Thus one obtains ⊢GIKt βi ⇒ θ for all 1 ≤ i ≤ n. Let β = β1∨. . .∨βn. By (∨L), one obtains ⊢GIKt β ⇒ θ. Hence β ≤ ⋆α. Conversely let ⊢GIKt β ⇒ δ for some δ ∈ T ∗ . Then by Lemma 14, one obtains ⊢GIKt βi ⇒ δ for all 1 ≤ i ≤ n. Then one gets ⊢GIKt ⋆αi ⇒ δ. Thus by (∨L), one obtains ⊢GIKt ⋆α ⇒ δ. Therefore ⋆α ≤ β. Hence ⋆α ∼ β.

Lemma 22. Let α ∈ T ∗ , β ∈ T ∗ and γ ∈ T ∗ . If ⊢GIKt ⋆α, β ⇒ θ and ⋆α ∼ γ, then ⊢GIKt γ, β ⇒ θ.

Proof. Let α = α1 ∨ . . . ∨ αn and β = β1 ∨ . . . ∨ βm where αi, βj ∈ T for all 1 ≤ i ≤ n and 1 ≤ j ≤ m. Suppose that ⋆αi ∼ γi and γ ′ = γ1 ∨ . . . ∨ γn. Then ⋆α ∼ γ ′ whence γ ′ ∼ γ.

By Lemma 14, one obtains ⊢GIKt ⋆αi, βj ⇒ θ for all 1 ≤ i ≤ n and 1 ≤ j ≤ m. By Lemma 16 there is a δij ∈ T such that ⊢GIKt ⋆αi, βj ⇒ δij and ⊢GIKt δij ⇒ θ. Since βj → δij ∈ T, by (→ L), one obtains ⊢GIKt ⋆αi ⇒ βj → δij . By Definition 17, one gets ⊢GIKt γi ⇒ βj → δij . Hence ⊢GIKt γi, βj ⇒ δij, whence ⊢GIKt γi, βj ⇒ θ. Then by (∨L), one obtains ⊢GIKt γ ′ , β ⇒ θ. For any γ ∼ γ ′ , we have ⊢IKt γ ⇒ γ ′ and hence ⊢GIKt γ, β ⇒ θ by (Cut).

We construct the quotient algebra from T ∗ as follows:

Definition 23 (Quotient algebra). The quotient algebra of T ∗ is a structure Q = (|T ∗ |, ∧∗ , ∨, →, ♦, ♦, □, ■, 0, 1), where: for any JαK, JβK ∈ |T ∗ |,

1. JαK ∧∗ JβK = Jα ∧∗ βK;
2. JαK ∨ JβK = Jα∨ βK;
3. 0 = J⊥K;
4. JαK → JβK = Jγ1∨. . .∨γnK where γi ∈ T ∗ s.t. JαK∧∗ JγiK ≤ JβK for any i ∈ {1, . . . n};
5. 1 = J⊤K;
6. ♦JαK = JγK where γ ∈ T ∗ s.t. γ ∼ ·α;
7. ♦JαK = JγK where γ ∈ T ∗ s.t. γ ∼ ◦α;
8. □JαK = Jγ1 ∨ . . . ∨ γnK where γi ∈ T ∗ s.t. ♦JγiK ≤ JαK for any i ∈ {1, . . . n};
9. ■JαK = Jγ1 ∨ . . . ∨ γnK where γi ∈ T ∗ s.t. ♦JγiK ≤ JαK for any i ∈ {1, . . . n}.

One can easily check that Q is well-defined. For instance, assume that JαK = JβK, it can be proved that ♦JαK = ♦JβK as follows. Let ♦JαK = Jγ1K and ♦JβK = Jγ2K. Let ⊢GIKt γ2 ⇒ θ for any θ ∈ T ∗ . Then ⊢GIKt ◦β ⇒ θ. Since JαK = JβK, one gets ⊢GIKt α ⇒ β. Hence by (Cut), one obtains ⊢GIKt ◦α ⇒ θ. Thus ⊢GIKt γ1 ⇒ θ. Hence Jγ1K ≤ Jγ2K. Similarly one proves Jγ2K ≤ Jγ1K. The order of Q is defined by ∧∗ as: JαK ≤ JβK iff JαK ∧∗ JβK = JαK.

Lemma 24. ⊢GIKt α ⇒ β iff JαK ≤ JβK where α, β ∈ T ∗ .

Proof. Assume that ⊢GIKt α ⇒ β. Then ⊢GIKt α ⇔ α ∧∗ β. Thus JαK ≤ JβK. Conversely let JαK ≤ JβK. Then α ∧∗ β ∼ α. Clearly ⊢GIKt α ∧∗ β ⇒ β. Hence ⊢GIKt α ⇒ β.

Lemma 25. The following conditions hold for Q: for any JαK, JβK and JγK ∈ |T ∗ |,

1. JαK ∨ JβK ≤ JγK iff JαK ≤ JγK and JβK ≤ JγK;
2. JγK ≤ JαK ∧∗ JβK iff JγK ≤ JαK and JγK ≤ JβK;
3. JαK ∧∗ (JβK ∨ JγK) = (JαK ∧∗ JβK) ∨ (JαK ∧∗ JγK);
4. 0 ≤ JαK and JαK ≤ 1;
5. JαK ∧∗ JβK ≤ JγK iff JαK ≤ JβK → JγK;
6. ♦(JαK ∨ JβK) = ♦JαK ∨ ♦JβK and ♦(JαK ∨ JβK) = ♦JαK ∨ ♦JβK;
7. ♦0 = 0 and ♦0 = 0;
8. ♦JαK ≤ JβK iff JαK ≤■JβK;
9. ♦JαK ≤ JβK iff JαK ≤□JβK;
10. ♦JαK ∧ JβK ≤ ♦(JαK ∧ ♦JβK) and ♦JαK ∧ JβK ≤ ♦(JαK ∧ ♦JβK).

Proof. (2) and (3) follows from Definition 23. (5) and (7) can be check easily. (8) and (9) are analogous to (4). Thus we only provide the proofs for (1),(4), (6) and (10).

(1) From left to right direction, assume that JγK ≤ Jα ∧∗ βK. Let α = ∨i αi and β = ∨j βj s.t. αi, βj ∈ T for any i ∈ {1, . . . , n} and j ∈ {1, . . . ,m}. By Definition 23 JαK ∧∗ JβK = Jα ∧∗ βK = J∨ij (αi ∧ βj)K. Clearly ⊢GIKt αi ∧ βj ⇒ αi. So by (∨R) ⊢GIKt αi ∧ βj ⇒ α. Hence by (∨L), one obtains ⊢GIKt ∨ij (αi ∧ βj) ⇒ α. Similarly, one obtains ⊢GIKt ∨ij (αi ∧ βj) ⇒ β. Hence, by assumption and (Cut), ⊢GIKt γ ⇒ α and ⊢GIKt γ ⇒ β. Therefore, by Lemma 24, JγK ≤ JαK and JγK ≤ JβK.

Conversely, assume that JγK ≤ JαK and JγK ≤ JβK. Let ⊢GIKt ∨ij (αi ∧ βj) ⇒ θ for some θ ∈ T ∗ . Thus by Lemma

14, one obtains ⊢GIKt αi ∧ βj ⇒ θ. Since ⊢GIKt αi, βj ⇒ αi ∧ βj, by (Cut), ⊢GIKt αi, βj ⇒ θ. By (∨L), one obtains ⊢GIKt α, β ⇒ θ. The assumption and Lemma 24 imply that ⊢GIKt γ ⇒ α and ⊢GIKt γ ⇒ β. By (Cut), one obtains ⊢GIKt γ, γ ⇒ θ. Finally, by (Conf), ⊢GIKt γ ⇒ θ. Therefore, γ ≤ α ∧∗ β by Definition 17, and hence JγK ≤ Jα ∧∗ βK = JαK ∧∗ JβK.

1. Assume that JαK ∧∗ JβK ≤ JγK. Then by Definition 23, Jβ → γK = Jδ1 ∨ . . . ∨ δn ∨ αK where δ1, . . . , δn ∈ T ∗ . Clearly ⊢GIKt α ⇒ δ1 ∨ . . . ∨ δn ∨ α. Thus JαK ≤ Jδ1 ∨ . . . ∨ δn ∨αK, whenceJαK ≤ Jβ → γK. Conversely let JαK ≤ JβK → JγK and JβK → JγK = Jδ1 ∨ . . . ∨ δnK where JβK ∧∗ JδiK ≤ JγK for all 1 ≤ i ≤ n. Then ⊢GIKt β ∧∗ δi ⇒ γ. Clearly ⊢GIKt β, δi ⇒ β ∧∗ δi Then by (Cut), ⊢GIKt β, δi ⇒ γ for all 1 ≤ i ≤ n. By (∨L), one obtains ⊢GIKt β, δ ⇒ γ. Clearly ⊢GIKt α ⇒ δ. Thus by (Cut), one obtains ⊢GIKt β, α ⇒ γ. Hence by Lemma 15 ⊢GIKt β ∧∗ α ⇒ γ.

(6) Let ♦JαK = Jγ1K, ♦JβK = Jγ2K and ♦Jα∨ βK = Jγ3K where γ1, γ2, γ3 ∈ T ∗ . Let ⊢GIKt γ3 ⇒ θ. Then ⊢GIKt ◦(α ∨ β) ⇒ θ. By Lemma 14, ⊢GIKt ◦α ⇒ θ and ⊢GIKt ◦β ⇒ θ. Hence ⊢GIKt γ1 ⇒ θ and ⊢GIKt γ2 ⇒ θ. Thus by (∨L), one obtains ⊢GIKt γ1 ∨ γ2 ⇒ θ. Hence by Lemma 24, Jγ3K ≤ Jγ1 ∨ γ2K, whence ♦Jα∨ βK ≤ ♦JαK ∨ ♦JβK. Similarly ♦JαK ∨ ♦JβK ≤ ♦Jα ∨ βK. The proof for the second equality is analogous and hence is omitted.

(10) Let ♦JβK = γ, ♦JαK = δ and ♦Jα∧∗ γK = π where γ, δ, π ∈ T ∗ . It suffice to show Jδ ∧ βK ≤ JπK. Let ⊢GIKt π ⇒ θ for any θ ∈ T ∗ . Then ⊢GIKt ◦(α ∧∗ γ) ⇒ θ. Clearly ⊢GIKt α, γ ⇒ α ∧∗ γ. Hence by (Cut) ⊢GIKt ◦(α, γ) ⇒ θ. Clearly ⊢GIKt ·β ⇒ γ. By (Cut), one obtains ⊢GIKt ◦(α, ·β) ⇒ θ. Then by (WK◦), one obtains ⊢GIKt ◦α, β ⇒ θ. Thus by Lemma 22 ⊢GIKt δ, β ⇒ θ. By Lemma 15 ⊢GIKt δ ∧∗ β ⇒ θ. Hence Jδ ∧ βK ≤ JπK. The proof for the second inequality is analogous and hence is omitted.

Lemma 19 and Lemma 25 imply that:

Theorem 26. Q is a finite IKt.

Lemma 27. Let α∧β, α→ β, ♦α, ♦α, □α, ■α, ⊥, ⊤ ∈ T, then the following equations hold:

1. Jα∧ βK = JαK ∧∗ JβK;
2. J⊥K = 0 and J⊤K = 1;
3. Jα→ βK = JαK → JβK;
4. J♦αK = ♦JαK and J♦αK = ♦JαK;
5. J□αK =□JαK and J■αK =■JαK.

Proof. (1), (3) and (4) follow from Definition 23. We only provide proofs for (2) and (5) as follows.

(2) It is clear that ⊢GIKt α ∧∗ (α → β) ⇒ β. Hence, JαK ∧∗ Jα→ βK ≤ JβK. By Lemma 25.4, Jα→ βK ≤ JαK → JβK. Conversely let γ1, . . . , γn ∈ T ∗ and Jα → βK = Jγ1 ∨ . . . ∨ γnK such that JαK ∧∗ JγiK ≤ JβK. Thus ⊢GIKt α ∧ γi ⇒ β for all 1 ≤ i ≤ n. Hence ⊢GIKt α, γi ⇒ β by (Cut), then by (→ R), ⊢GIKt γi ⇒ α → β. Hence by (∨L), one obtains that ⊢GIKt γ1 ∨ . . . ∨ γn ⇒ α → β. Therefore, since α → β ∈ T ⊆ T ∗ , JαK → JβK ≤ Jα → βK by Lemma 24.

(5) It is easy to show that ⊢GIKt ◦■α ⇒ α. Hence, ♦J■αK ≤ JαK. Thus J■αK ≤ ■JαK by Lemma 25.8. Conversely let γ1, . . . , γn ∈ T ∗ and ■JαK = Jγ1 ∨ . . . ∨ γnK where ♦JγiK ≤ α. Then ⊢GIKt ◦γi ⇒ α for all 1 ≤ i ≤ n. Hence by (■R) and (∨L), one gets ⊢GIKt γ1∨. . .∨γn ⇒ ■α. Therefore, ■JαK ≤ J■αK since ■α ∈ T ⊆ T ∗ .

Lemma 28. For any ISt-sequent α ⇒ β, if ̸⊢GIKt α ⇒ β, then there exits a finite IKt-algebra Q, such that ̸|=Q α ⇒ β.

Proof. Let F be the set of all subformulae of α and β. Let T be the ∧,→-closure of F. Obviously T is closed under subformulae. Define T ∗ as above. Let σ : T ∗ → |T ∗ | be defined as σ(p) = JpK for all p ∈ Var ∩ T . By induction on the complexity of formula, Lemma 27 implies that σ(γ) = JγK for any γ ∈ T . Let Q be constructed as above and hence Q is a finite IKt by Theorem 26 . We show the contraposition of the claim. Assume that |=Q α ⇒ β which implies that |=Q σ(α) ≤ σ(β). The completeness of GIKt implies that ⊢GIKt α⇒ β.

Let A be the ∨-free reduct of Q. Obviously A is a finite ISt-algebra.

Proof. Assume that ̸⊢GISt α ⇒ β. By Proposition 13, ̸⊢GIKt α ⇒ β. By Lemma 28, ̸|=Q α ⇒ β. Hence ̸|=A α ⇒ β.

Theorem 30. ISt has the finite model property.

Corollary 31 (Decidability). ISt is decidable.

5 Conclusion

In this paper we have proved the finite model property for ISt and hence its decidability. These results also partially address the open question of the finite model property and decidability of IKt. However, the results of the present paper cannot be straightforwardly extended to IKt since Lemma 16 and Lemma 19 do not hold if there are ∨-formulae in T (see the paragraph above Lemma 14). The FMP of IKt will be our next work. The computational complexity of IKt is PSPACEhard while the same problem for ISt is unknown. Up to our knowledge, there are no results on the computational complexity of the logic of implicative semi-lattices. Our sequent system and the proof of the finite model property might provide some help for finding a refined upper bound for the complexity of ISt. Using our methods to obtain some temporal extensions of logic programing algorithms and to solve the decidability problems of the intuitionistic modal logics which are used to model dynamic processes in theoretical computer science and artificial intelligence are also interesting topics for our future work.

Acknowledgements

The first author is supported by "International Scientific Cooperation Seed Fund of Shandong University" (11090089395416) and "Young Scholars Program of Shandong University"(11090089964225). The second author is supported by "The National Social Science Fund of China" (17CZX048). Both of the two authors are grateful to five anonymous reviewers for their comments to revise the paper.