Paper deep dive

Applications of Intuitionistic Temporal Logic to Temporal Answer Set Programming

Pedro Cabalar, Martín Diéguez, David Fernández-Duque, François Laferrière, Torsten Schaub, Igor Stéphan

Year: 2026Venue: arXiv preprintArea: cs.LOType: PreprintEmbeddings: 154

Intelligence

Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 94%

Last extracted: 3/22/2026, 5:13:21 AM

Summary

This paper investigates the logical foundations of Temporal Answer Set Programming (TASP) by extending Pearce's equilibrium logic and Osorio's safe beliefs to the temporal domain. It establishes a formal correspondence between temporal intuitionistic logic and temporal logic programming, utilizing Temporal Here-and-There (THT) logic and semantic bisimulations to overcome challenges in axiomatic systems for intuitionistic temporal logics.

Entities (6)

Osorio · researcher · 99%Pearce · researcher · 99%Temporal Answer Set Programming · field-of-study · 98%Intuitionistic Logic · logic · 95%Temporal Equilibrium Logic · formalism · 95%Temporal Here-and-There logic · logic · 95%

Relation Signals (4)

Temporal Equilibrium Logic → combines → Equilibrium Logic

confidence 95% · a formalism combining equilibrium logic with linear-time temporal operators

Pearce → developed → Equilibrium Logic

confidence 95% · prominently featuring Pearce’s equilibrium logic

Osorio → developed → Safe Beliefs

confidence 95% · Osorio's safe beliefs

Temporal Here-and-There logic → characterizes → Temporal Equilibrium Models

confidence 90% · theory completions coincide with temporal equilibrium models when HT is superseded by Temporal Here-and-There logic

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:The relationship between intuitionistic or intermediate logics and logic programming has been extensively studied, prominently featuring Pearce's equilibrium logic and Osorio's safe beliefs. Equilibrium logic admits a fixpoint characterization based on the logic of here-and-there, akin to theory completion in default and autoepistemic logics. Safe beliefs are similarly defined via a fixpoint operator, albeit under the semantics of intuitionistic or other intermediate logics. In this paper, we investigate the logical foundations of Temporal Answer Set Programming through the lens of Temporal Equilibrium Logic, a formalism combining equilibrium logic with linear-time temporal operators. We lift the seminal approaches of Pearce and Osorio to the temporal setting, establishing a formal correspondence between temporal intuitionistic logic and temporal logic programming. Our results deepen the theoretical underpinnings of Temporal Answer Set Programming and provide new avenues for research in temporal reasoning.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

153,864 characters extracted from source content.

Expand or collapse full text

Applications of Intuitionistic Temporal Logic to Temporal Answer Set Programming111This paper is an extended version of (Cabalar et al. 2024), presented at the 17th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2024). PEDRO CABALAR MARTÍN DIÉGUEZ DAVID FERNÁNDEZ-DUQUE FRANÇOIS LAFERRIÈRE TORSTEN SCHAUB IGOR STÉPHAN Abstract The relationship between intuitionistic or intermediate logics and logic programming has been extensively studied, prominently featuring Pearce’s equilibrium logic and Osorio’s safe beliefs. Equilibrium logic admits a fixpoint characterization based on the logic of here-and-there, akin to theory completion in default and autoepistemic logics. Safe beliefs are similarly defined via a fixpoint operator, albeit under the semantics of intuitionistic or other intermediate logics. In this paper, we investigate the logical foundations of Temporal Answer Set Programming through the lens of Temporal Equilibrium Logic, a formalism combining equilibrium logic with linear-time temporal operators. We lift the seminal approaches of Pearce and Osorio to the temporal setting, establishing a formal correspondence between temporal intuitionistic logic and temporal logic programming. Our results deepen the theoretical underpinnings of Temporal Answer Set Programming and provide new avenues for research in temporal reasoning. Under consideration in Theory and Practice of Logic Programming (TPLP). keywords: Temporal answer set programming, Temporal equilibrium logic, Fixpoint characterization 1 Introduction Temporal logic programming, introduced in the late 1980s (Abadi and Manna 1989), augments logic programming with temporal modal operators, primarily those from linear-time temporal logic (LTL; Pnueli 1977). Although this field experienced substantial research activity throughout the 1980s and 1990s, its momentum eventually waned. More recently, the advent of answer set programming (ASP; Lifschitz 2019), and particularly its demonstrated efficacy in modeling and resolving temporal scenarios, has sparked renewed interest in these foundational approaches to temporal logic programming. Early approaches to time representation in ASP (Gelfond and Lifschitz 1993) relied on variables ranging over finite subsets of the natural numbers. Although straightforward, this methodology lacked the dedicated language constructs and specialized inference mechanisms characteristic of LTL. Consequently, it remains infeasible to represent or reason about properties of reactive systems over infinite traces, such as safety (e.g., “Is a specific state reachable?”) or liveness (e.g., “Does a condition hold infinitely often?”). Furthermore, establishing the unsolvability of planning problems becomes substantially more difficult. To overcome these limitations, several extensions of ASP with temporal operators have been investigated. For instance, Eiter and Šimkus (2009) extended logic programs with function symbols to model both past and future temporal references. Other modal-inspired approaches typically adopt a temporal or dynamic modal logic (Pnueli 1977; Harel et al. 2000) as a monotonic basis, subsequently introducing nonmonotonicity via an established ASP semantics (Lifschitz 2010). As an example, Giordano et al. (2013) generalized the traditional reduct-based semantics (Gelfond and Lifschitz 1988) to a logic programming fragment equipped with dynamic logic operators (Harel et al. 2000). Similarly, Aguado et al. (2013) integrated LTL with equilibrium logic (EL; Pearce 2006), the predominant logical characterization of stable models and answer sets. This latter framework was subsequently adapted to finite traces in (Aguado et al. 2023). Equilibrium logic builds upon here-and-there logic (HT; Heyting 1930) by imposing a minimal model selection criterion to capture answer sets. In his seminal work, Pearce (2006) provided an alternative formulation of equilibrium logic based on fixpoints. Analogous to the treatment of default and autoepistemic logics (Marek and Truszczyński 1993), this characterization relies on theory extensions, or completions, rather than direct semantic minimization. A related fixpoint characterization, termed safe beliefs, was introduced by Osorio et al. (2005a). Instead of HT, their approach employs intuitionistic logic (INT; Mints 2000) as its monotonic foundation. Crucially, they demonstrated that INT can be substituted with any (intermediate) logic X satisfying INT⊆X⊆HT INT X HT without altering the resulting safe beliefs. Consequently, safe beliefs provide a robust framework for investigating properties of (temporal) logic programs from a broader logical standpoint, facilitating novel and insightful program transformations. In this paper, we extend both Pearce’s and Osorio’s fixpoint-based characterizations to the temporal domain. Regarding Pearce’s approach, we demonstrate that theory completions coincide with temporal equilibrium models when HT is superseded by Temporal Here-and-There logic (THT; (Balbiani and Diéguez 2016)). Extending Osorio’s approach to the temporal setting presents several notable challenges. First, Osorio’s work heavily relies on fundamental properties of propositional intuitionistic and intermediate logics (Gabbay 1981). One pivotal property is that satisfiability (or consistency) in intuitionistic logic is preserved across all intermediate logics. Furthermore, if a formula is satisfiable, it is guaranteed to hold in a finite model. Unfortunately, these properties generally fail in the temporal case. To circumvent this, we identify an intuitionistic temporal logic that preserves these characteristics, serving as the “weakest” intuitionistic base logic in our framework. Second, Osorio’s approach depends on a syntactic consequence relation and Hilbert-style axiomatic systems for intuitionistic logic. However, to the best of our knowledge, no sound and complete axiomatic system currently exists for an intuitionistic version of LTL.222In (Boudou et al. 2019), four axiomatic systems for intuitionistic temporal logics are studied. It is shown that each generates a different logic, inducing distinct confluence properties. However, their completeness remains unaddressed. A sound and complete axiomatic system for the □ -free fragment of ITLeITL^e is presented in (Diéguez and Fernández-Duque 2018). Alternative attempts introduce the co-implication connective (Rauszer 1974) into the language (Fernández-Duque et al. 2024; Aguilera et al. 2025; 2022). Additionally, Osorio’s method employs syntactic transformations to eliminate propositional variables. These transformations cannot be directly lifted to the temporal setting, as the truth values of propositional variables vary dynamically over time. In light of these challenges, we adopt a strictly semantic approach. We reformulate Osorio’s fundamental results using a semantic entailment relation, which we subsequently generalize to the temporal case. A critical component of this strategy is the application of bisimulations for both intuitionistic (Patterson 1997) and intuitionistic temporal logics (Balbiani et al. 2020). Beyond reformulating Osorio’s results semantically, we formally define the notion of an X-temporal safe belief set, where X is any intermediate temporal logic. We establish two primary results: first, that THT-temporal safe belief sets exactly correspond to temporal equilibrium models; and second, that substituting THT with any weaker intermediate temporal logic yields the identical set of safe beliefs. The remainder of this paper is organized as follows. Section 2 provides the background on propositional intuitionistic and equilibrium logics. Section 3 introduces Pearce’s theory completions alongside our semantic reformulation of Osorio’s safe beliefs. Section 4 reviews intuitionistic and intermediate temporal logics, detailing the specific technical results employed in our framework. Section 5 presents our primary contribution: lifting Pearce’s theory completions and Osorio’s safe beliefs to the temporal domain. Finally, we conclude the paper with a brief discussion and directions for future research. 2 Intuitionistic and Intermediate Logics Given a countable, possibly infinite set ℙP of atoms, also called alphabet, our basic language ℒpL_p consists of formulas generated by the following grammar: φ::=p∈ℙ∣⊥∣φ∧φ∣φ∨φ∣φ→φ ::=p → The negation connective is defined in terms of implication as ¬φ:=φ→⊥ := → . A (propositional) theory is a possibly infinite set of propositional formulas. Formulas of ℒpL_p are interpreted over partially ordered sets. An intuitionistic frame is a tuple =(W,≼) F=(W, ), where W is a non-empty set of (Kripke) worlds and ≼⊆W×W W× W is a partial order. Given a frame =(W,≼) F=(W, ), a world w∈Ww∈ W is ≼ -maximal if there is no v∈Wv∈ W such that w≠vw =v and w≼vw v. Because maximality is exclusively associated with the relation ≼ throughout this work, we simply use the term maximal. Given a frame =(W,≼) F=(W, ), we say that a subset U⊆WU W is an upset of F if for every w,v∈Ww,v∈ W we have that if both w∈Uw∈ U and w≼vw v then v∈Uv∈ U. Moreover, a frame ′=(U,≼′) F =(U, ) is called a generated subframe of F if U⊆WU W is an upset of F and ≼′ is the restriction of ≼ to U, that is, ≼′=≼∩(U×U) = ∩(U× U). Finally, given w∈Ww∈ W, we define the subframe generated by w as the generated subframe ′=(u∈W∣w≼u,≼′) F =(\u∈ W w u\, ). We say that an intuitionistic frame =(W,≼) F=(W, ) is of depth n, 0pt=n0pt F=n in symbols, if there is a chain of n worlds in F and no chain of more than n worlds. Whenever F contains an n-world chain for every n<ωn<ω, we say that F is of infinite depth ∞. Given a frame =(W,≼) F=(W, ) and w∈Ww∈ W, we denote the depth of the subframe generated by w as 0pt(,w)0pt( F,w). An intuitionistic model, or simply model, is a tuple =⟨(W,≼),V⟩ M= (W, ),V consisting of a frame (W,≼)(W, ) equipped with a monotone valuation function V:W→2ℙV:W→ 2^P. That is, if w≼vw v, then V(w)⊆V(v)V(w) V(v) for all w,v∈Ww,v∈ W. The satisfaction relation (denoted by ⊧ ) of a formula φ at w∈Ww∈ W is defined inductively by: 1. ,w⊧p M,w p iff p∈V(w)p∈ V(w) 2. ,w⊧̸⊥ M,w 3. ,w⊧φ∧ψ M,w ψ iff ,w⊧φ M,w and ,w⊧ψ M,w ψ 4. ,w⊧φ∨ψ M,w ψ iff ,w⊧φ M,w or ,w⊧ψ M,w ψ 5. ,w⊧φ→ψ M,w →ψ iff for all v≽wv w, if ,v⊧φ M,v , then ,v⊧ψ M,v ψ A formula φ is satisfied in an intuitionistic model =⟨,V⟩ M= F,V , in symbols ⊧φ M , if ,w⊧φ M,w for some w∈w∈ F. A formula φ is satisfied on an intuitionistic frame F, if there exists a model =⟨,V⟩ M= F,V such that ⊧φ M . A formula φ is valid on an intuitionistic frame F, in symbols ⊧φ F , if for all models =⟨,V⟩ M= F,V , we have ⊧φ M . In the case of a theory Γ , we say that ,w⊧Γ M,w if ,w⊧φ M,w for all φ∈Γ ∈ . Similarly, Γ is said to be consistent, if there is a model M and a world w such that ,w⊧Γ M,w . Finally we define the intuitionistic logic as INT:=φ∈ℒp∣⊧φ, INT:=\ _p F \, where F is an intuitionistic frame. 2.1 Intermediate Logics An intermediate logic333Chagrov and Zakharyaschev (1997) made a distinction between super-intuitionistic and intermediate logics but they also mention that in the propositional case, these two notions are practically identical. in the language ℒpL_p is any set of formulas X satisfying the following conditions: 1) INT⊆X⊆CL INT X CL, where CL stands for classical logic, 2) X is closed under modus ponens, i.e., φ,φ→ψ∈X , →ψ∈ X implies ψ∈Xψ∈ X, 3) X is closed under uniform substitution, i.e., φ∈X ∈ X implies φ∈X ∈ X for any φ∈ℒp _p and substitution s.444A substitution s is a mapping :ℙ→ℒps:P _p and φ is defined by induction on the construction of φ : φ=(p) =s(p), ⊥=⊥ = and (φ⊙ψ)=φ⊙ψ( ψ)s= for ⊙∈∧,∨,→ ∈\ , ,→\. A proper intermediate logic is an intermediate logic different from CL. Broadly speaking, intermediate logics are obtained by adding formulas (that are classically valid) to INT as axiom schemas (Gabbay 1981, Chapter 2). In this way, they impose restrictions on ≼ . Therefore, given an intermediate logic X, we define the class of X-frames as the set of all intuitionistic frames (W,≼)(W, ) where ≼ satisfies the restriction induced by the schemas used to generate X. As in the intuitionistic case, an intermediate logic X can be defined as X:=φ∈ℒp∣⊧φ, X:=\ _p F \, where F is an X-frame. To give an example, the logic of the weak exclude middle (Jankov 1968; Gabbay 1981) (KC) is obtained by adding the axiom ¬p∨¬p p p to INT and it is characterized by intuitionistic frames (W,≼)(W, ) satisfying the following frame condition: there exists u∈Wu∈ W such that v≼uv u for all v∈Wv∈ W.555In the literature, this frame condition is usually called topwidth 1 (Gabbay 1981). Another family of intermediate logics, denoted by BDnBD_n, are obtained by adding an instance of the axiom schema bd_n to INT. For a given n≥1n≥ 1, such a family of axioms is recursively defined as follows: bd_1 := := p1∨¬p1 p_1 p_1 + bd_n+1 := := pn+1∨(pn+1→). p_n+1 (p_n+1→ bd_n ). The axiom bd_n induces the following property on intuitionistic frames. Theorem 1 (Chagrov and Zakharyaschev 1997) An intuitionistic frame =(W,≼) F=(W, ) validates bd_n iff 0pt≤n0pt F≤ n, i.e, iff F satisfies the following condition ∀w0,⋯,∀wn((⋀i=0n−1wi≼wi+1)→⋁i≠j(wi=wj)).∀ w_0,·s,∀ w_n ( ( _i=0^n-1w_i w_i+1 )→ _i =j (w_i=w_j ) ). (1) The strongest proper intermediate logic is the logic of here-and-there (HT), which has been studied in the literature by different authors (Heyting 1930; Gödel 1932; Smetanich 1960). This logic is obtained by adding the axiom schema (Hosoi 1966) p∨(p→q)∨¬qp (p→ q ) q (2) to INT and it is characterized by frames of the form (0,1,≼)(\0,1\, ) where ≼=(0,0),(1,1),(0,1) =\(0,0),(1,1),(0,1)\. Broadly speaking, the world 0 (resp. 11) refers to the world “here” (resp. “there”). We write ⊧X _ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ to specify the satisfaction relation in a concrete intermediate logic X. When the underlying logic is clear from the context, we omit X from the satisfaction relation. The notions of satisfiability, validity and consistency are defined in an analogous way as with INT. However, we prefix them with the logic when necessary. For instance, when Γ is consistent in the logic X, we say that Γ is X-consistent. Consistency in any intermediate logic X is equivalent to consistency in classical logic. This is because, if a theory Γ is classically satisfiable, it is trivially satisfiable in a one-world model; conversely, if Γ is X-consistent, there exists a finite model satisfying all formulas in Γ at a world x. Hence, a maximal world of the submodel generated by x is a classical world that, in addition, satisfies Γ . Lemma 1 (Osorio et al. 2005a; van Dalen 1989) Let X and Y be two intermediate logics, and let Γ be a theory. Then Γ is X-consistent iff Γ is Y-consistent. Definition 1 (Local semantic consequence) Let X be any intermediate logic and let Γ and ψ be a propositional theory and a propositional formula, respectively. We define ψ as a local semantic consequence of Γ , written Γ⊧Xψ _ 0.0pt 3.83148pt3.0pt 0.0pt$ X$ 0.0pt 3.83148pt3.0pt 0.0pt$ X$ 0.0pt 3.2634pt3.0pt 0.0pt$ X$ 0.0pt 3.26338pt3.0pt 0.0pt$ X$ψ, if, for each X-model =⟨,V⟩ M= F,V and for each world w∈w∈ F, (,w⊧φ for all φ∈Γ) implies ,w⊧ψ. ( M,w for all ∈ ) implies M,w ψ. When ψ is replaced by a theory Δ , we say that Δ is local semantic consequence of Γ , written Γ⊧XΔ _ 0.0pt 3.83148pt3.0pt 0.0pt$ X$ 0.0pt 3.83148pt3.0pt 0.0pt$ X$ 0.0pt 3.2634pt3.0pt 0.0pt$ X$ 0.0pt 3.26338pt3.0pt 0.0pt$ X$ , if for each model X-model =⟨,V⟩ M= F,V and for each world w∈w∈ F, (,w⊧φ for all φ∈Γ) implies (,w⊧ψ, for all ψ∈Δ). ( M,w for all ∈ ) implies ( M,w ψ, for all ψ∈ ). Proposition 1 Let X⊆Y X Y be two intermediate logics. For all theories Γ and all formulas φ , Γ⊧Xφ _ 0.0pt 3.83148pt3.0pt 0.0pt$ X$ 0.0pt 3.83148pt3.0pt 0.0pt$ X$ 0.0pt 3.2634pt3.0pt 0.0pt$ X$ 0.0pt 3.26338pt3.0pt 0.0pt$ X$ implies Γ⊧Yφ _ 0.0pt 3.83148pt3.0pt 0.0pt$ Y$ 0.0pt 3.83148pt3.0pt 0.0pt$ Y$ 0.0pt 3.2634pt3.0pt 0.0pt$ Y$ 0.0pt 3.26338pt3.0pt 0.0pt$ Y$ . We denote by CnX(Γ):=φ∈ℒp∣Γ⊧XφCn_ X( ):=\ _p _ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ \ the set of consequences obtained from Γ within the intermediate logic X. 2.2 Bisimulations for Intuitionistic Logic In intuitionistic and modal logic, a world w in a model M cannot see the entire Kripke model, it can only explore it locally, step by step, by means of the different accessibility relations (≼ in the case of INT). The concept of bisimulation states that, if two worlds w and w′w are bisimilar, it does not matter how one can try to explore from w and w′w using modal formulas, since they are behaviorally indistinguishable with respect to their logical properties. Bisimulation in intuitionistic propositional logic was studied by Patterson (1997). Formally, given two models 1=⟨(W1,≼1),V1⟩ M_1= (W_1, _1),V_1 and 2=⟨(W2,≼2),V2⟩ M_2= (W_2, _2),V_2 , a bisimulation Z is a relation on W1×W2W_1× W_2 that satisfies the following properties: C1 if w1w2w_1Zw_2 then V1(w1)=V2(w2)V_1(w_1)=V_2(w_2) C2 if w1w2w_1Zw_2 then for all v1∈W1v_1∈ W_1, if w1≼1v1w_1 _1v_1, then there exists v2∈W2v_2∈ W_2 such that w2≼2v2w_2 _2v_2 and v1v2v_1Zv_2 C3 if w1w2w_1Zw_2 then for all v2∈W2v_2∈ W_2, if w2≼2v2w_2 _2v_2, then there exists v1∈W1v_1∈ W_1 such that w1≼1v1w_1 _1v_1 and v1v2v_1Zv_2 Condition C1 ensures that two bisimilar worlds satisfy the same atoms. Condition C2 expresses that if we move forward from w1w_1 to a new world v1v_1, we can find a matching move from w2w_2 to a world v2v_2 that is (logically) indistinguishable from v1v_1. In other words, the second model can imitate the movements of the first. Condition C3 is the mirror image of C2: now the second model makes a move and the first one must be able to imitate it. Given two models 1=⟨(W1,≼1),V1⟩ M_1= (W_1, _1),V_1 and 2=⟨(W2,≼2),V2⟩ M_2= (W_2, _2),V_2 with w1∈W1w_1∈ W_1 and w2∈W2w_2∈ W_2, we say that 1 M_1 and 2 M_2 are bisimilar, if there exists a bisimulation Z between W1W_1 and W2W_2 such that w1w2w_1Zw_2. The following lemma states that two bisimilar Kripke worlds satisfy the same formulas. Lemma 2 (Patterson 1997) Given two models 1=⟨(W1,≼1),V1⟩ M_1= (W_1, _1),V_1 and 2=⟨(W2,≼2),V2⟩ M_2= (W_2, _2),V_2 and a bisimulation Z on W1×W2W_1× W_2, then for all w1∈W1w_1∈ W_1 and for all w2∈W2w_2∈ W_2, if w1w2w_1Zw_2 then for all φ∈ℒp _p, 1,w1⊧φ M_1,w_1 iff 2,w2⊧φ M_2,w_2 . The proof of the lemma is done by structural induction and it uses C1 to prove the case of the propositional variables while conditions C2 and C3 are used to prove the case of implication. Osorio et al. (2005b) show that the notion of X-safe beliefs is independent of the intermediate logic X; replacing X with any proper intermediate logic leaves the set of safe beliefs unchanged. Their approach, however, relies on a syntactic entailment relation and a Hilbert-style axiomatization of INT. Here, we establish the same result semantically via bisimulations. Our first lemma demonstrates that if a world w in an intuitionistic model M satisfies all instances of the axiom ¬p∨¬p p p, then all maximal worlds in the subframe generated by w can be merged into a single world. Proposition 2 Let =⟨(W,≼),V⟩ M= (W, ),V be an intuitionistic model and let w∈Ww∈ W be such that ,w⊧¬p∨¬p∣p∈ℙ M,w \ p p p \. It follows that all maximal ≼ -worlds in the subframe generated by x satisfy the same propositional variables. Lemma 3 Let =⟨(W,≼),V⟩ M= (W, ),V an intuitionistic model and let w∈Ww∈ W be such that ,w⊧¬p∨¬p∣p∈ℙ M,w \ p p p \. There exists a model ′=⟨(W′,≼′),V′⟩ M = (W , ),V , w′∈W′w ∈ W and a bisimulation ⊆W×W′Z W× W such that ww′wZw and the subframe generated by w′w has a unique maximal world with respect to ≼′ . Proof 2.2. From ,w⊧¬p∨¬p∣p∈ℙ M,w \ p p p \ and Proposition 2, all maximal worlds in the subframe generated by w satisfy the same propositional variables. Let us define now the model ′:=⟨(W′,≼′),V′⟩ M := (W , ),V as follows: • W′=v∈W,u∣w≼v and v is not ≼-maximal W =\v∈ W,u w v and v is not -maximal \, where u∉Wu ∈ W is a fresh world. • v≼′v′v v if v,v′∈Wv,v ∈ W and v≼v′v v or v′=uv =u; u≼′u u. • V′(u):=V(x)V (u):=V(x), where x∈Wx∈ W, w≼xw x and x is ≼ -maximal; V′(v):=V(v)V (v):=V(v), for all v∈W′v∈ W with v≠uv =u. wwv1v_1u1u_1≼ 2u_2≼ ≼ 2v_2u3u_3≼ ≼ 3v_3u4u_4≼ 5u_5≼ ≼ 1v_1≼′ v2v_2u≼′ v3v_3≼′ ≼′ M′ M Figure 1: A bisimulation relation, represented in red dashed lines, among two intuitionistic models M (on the left) and ′ M (with a unique maximal world, on the right). We assume that, ,w⊧¬p∨¬p∣p∈ℙ M,w \ p p p \ and we define V′V as V′(w):=V(w)V (w):=V(w), V′(vi):=V(vi)V (v_i):=V(v_i) for all i∈1,2,3i∈\1,2,3\ and V′(u)V (u) can be set (for instance) to V(u1)V(u_1). Reflexivity and transitivity of ≼ and ≼′ is not represented for the sake of readability. It can be checked that ′ M is an intuitionistic model and, moreover, that there exists a relation ⊆W×W′Z W× W , displayed in red dashed lines in Figure 1. In general, we map maximal worlds in W to u∈W′u∈ W while the remaining worlds v∈Wv∈ W that belong to the subframe generated by w are mapped to themselves in W′W (where they also belong by construction). The reader can easily check that Z is a bisimulation. The notion of bisimulation can also be used to contract intuitionistic models to HT models. In the following lemma, we identify the condition under which such contraction is possible. Before presenting our result, we introduce the following notation. Definition 2.3. Let =⟨(W,≼),V⟩ M= (W, ),V be an intuitionistic model and let w∈Ww∈ W. We define the sets ≼(w) (w) :=v∈W∣w≼v :=\v∈ W w v\ ≺(w) (w) :=v∈W∣w≼v and v≠w. :=\v∈ W w v and v =w\. Clearly, w∈≼(w)w∈ (w) while w∉≺(w)w∉ (w). Lemma 2.4 (Contraction lemma). Let =⟨(W,≼),V⟩ M= (W, ),V be an intuitionistic model, let T⊆ℙT and let w∈Ww∈ W satisfying the following conditions: 1. ≼(w) (w) has a unique maximal world, denoted by u, and 2. V(v)=TV(v)=T, for all v∈≺(w)v∈ (w). Then, there exists a HT model ′=⟨(0,1,≼′),V′⟩ M = (\0,1\, ),V and a bisimulation ⊆W×0,1Z W×\0,1\ such that w0wZ0 Proof 2.5. Let us define ′=⟨(0,1,≼′),V′⟩ M = (\0,1\, ),V as V′(0):=V(w)V (0):=V(w) and V′(1):=V(u)V (1):=V(u). Let us define the relation ⊆W×0,1Z W×\0,1\ as :=((w,0),(v,1))∣v∈≺(w)Z:=\((w,0),(v,1)) v∈ (w)\. It can be checked that Z is a bisimulation among M and ′ M . Figure 2 shows both M and ′ M together with Z (in red dashed lines). wwv1v_1≼ 2v_2u≼ ≼ 3v_3≼ ≼ ≼ 011≼′ M′ M Figure 2: An intuitionistic model M, a HT model ′ M and a bisimulations Z (in red dashed lines) among them. As preconditions, V(v)=TV(v)=T for all v∈Wv∈ W with v≠wv =w, V′(0)=V(w)V (0)=V(w) and V′(1)=V(u)V (1)=V(u). Reflexivity and transitivity of ≼ and ≼′ are not represented for the sake of readability. 2.3 Equilibrium Logic The logic of here-and-there (HT; Heyting 1930) is fundamental in logic programming, since it serves as the basis for equilibrium logic (EL; Pearce 1997; 2006), the most prominent logical characterization of stable models and answer sets (Gelfond and Lifschitz 1988). EL extends HT via a model selection criterion that induces nonmonotonicity. For any two HT models 1=(,V1) M_1=( F,V_1) and 2=(,V2) M_2=( F,V_2), we define a partial order 1≤2 M_1≤ M_2 holding when V1(1)=V2(1)V_1(1)=V_2(1) and V1(0)⊆V2(0)V_1(0) V_2(0). Strict inequality 1<2 M_1< M_2 holds if 1≤2 M_1≤ M_2 and V1≠V2V_1≠ V_2. A model =(,V) M=( F,V) is called total if V(0)=V(1)V(0)=V(1). Equilibrium models are then defined as follows. Definition 2.6 (Pearce 2006). A total HT model =⟨,V⟩ M= F,V is an equilibrium model of a formula φ if 1. ,0⊧HTφ M,0 _ 0.0pt 7.54004pt3.0pt 0.0pt$ HT$ 0.0pt 7.54004pt3.0pt 0.0pt$ HT$ 0.0pt 6.40483pt3.0pt 0.0pt$ HT$ 0.0pt 6.40483pt3.0pt 0.0pt$ HT$ , and 2. M is ≤-minimal, i.e., there is no ′< M < M such that ′,0⊧HTφ M ,0 _ 0.0pt 7.54004pt3.0pt 0.0pt$ HT$ 0.0pt 7.54004pt3.0pt 0.0pt$ HT$ 0.0pt 6.40483pt3.0pt 0.0pt$ HT$ 0.0pt 6.40483pt3.0pt 0.0pt$ HT$ . ∎ 3 Two Fixpoint Characterisations of Propositional Equilibrium Logic This section presents two characterizations of equilibrium models (and, consequently, answer sets) that we extend to the temporal setting in Section 5. The first characterization, originally defined by Pearce (2006), is based on the concept of theory completions, which has also been used in autoepistemic and default logic (Marek and Truszczyński 1993; Besnard 1989). 3.1 Pearce’s fixpoint characterization Definition 3.7 (Pearce 2006). Let Γ be a theory. A set E of formulas extending Γ is said to be a completion of Γ iff E E =CnHT(Γ∪¬ψ∣ψ∉E). =Cn_ HT( ∪\ ψ ψ ∈ E\). ∎ Equilibrium models correspond precisely to completions in the propositional case. For any model M, we define ℎ():=ψ∣,0⊧HTψ.Th( M):=\ψ M,0 _ 0.0pt 7.28226pt3.0pt 0.0pt$ HT$ 0.0pt 7.28226pt3.0pt 0.0pt$ HT$ 0.0pt 6.46344pt3.0pt 0.0pt$ HT$ 0.0pt 6.46342pt3.0pt 0.0pt$ HT$ψ\. The relation between equilibrium models and theory completions is made precise next. Proposition 3.8 (Pearce 1999b). For any theory Γ , there is a one-to-one correspondence between the equilibrium models of Γ and the completions of Γ . In particular, E=ℎ()E=Th( M) for some equilibrium model M of Γ . Similarly, any total HT model =⟨,V⟩ M= F,V is an equilibrium model of Γ iff V(0)=V(1)=E∩ℙV(0)=V(1)=E for some completion E of Γ . 3.2 INT-safe beliefs A slightly different fixpoint characterization of equilibrium logic can be given in terms of INT-safe beliefs (Osorio et al. 2005a), which are typically defined in terms of entailment in intuitionistic and intermediate logics. In this section, we provide a semantic reformulation of INT-safe beliefs, offering a different perspective that is useful for our subsequent development of temporal safe beliefs. Definition 3.9. A set T of atoms is said to be an INT-safe belief set of a theory Γ if • Γ∪¬p∣p∈T∪¬p∣p∉T ∪\ p p∈ T\∪\ p p ∈ T\ is INT-consistent and • Γ∪¬p∣p∈T∪¬p∣p∉T⊧INTT ∪\ p p∈ T\∪\ p p ∈ T\ _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$T. Analogous definitions can be reproduced for intermediate logics by replacing INT by any intermediate logic X. In fact, HT-safe beliefs correspond to equilibrium models, as stated in the following lemma. Lemma 3.10 (Osorio et al. 2005a; Pearce 2006). There is a one-to-one correspondence between both the HT-safe beliefs sets of a theory Γ and its equilibrium models. That is, for each HT-safe belief set T, we can construct an equilibrium model =⟨,V⟩ M= F,V where V(0)=V(1)=TV(0)=V(1)=T. Conversely, given M, we can extract the HT-safe belief set T=V(0)T=V(0). Osorio et al. (2005a) show that safe beliefs are independent of the chosen intermediate logic, as stated in lemmas 3.11 (below) and 3.12. Lemma 3.11 (Osorio et al. 2005a). Let T be a set of atoms and let X and Y be two proper intermediate logics such that X⊆Y X Y. For any propositional theory Γ , if T is a X-safe belief set of Γ , then T is a Y-safe belief set of Γ . In (Osorio et al. 2005a), Lemma 3.12 is proved by using arguments from proof theory. We provide a model-theoretic proof based on Lemma 2.4, which is easier to extend to temporal equilibrium logic. Lemma 3.12. Let T be a set of atoms and let X and Y be two proper intermediate logics satisfying X⊆Y X Y. For any propositional theory Γ , if T is a Y-safe belief set of Γ then T is a X-safe belief set of Γ . Proof 3.13. Let us assume that T is a Y-safe belief of Γ . It holds that (a) Γ∪¬p∣p∈T∪¬p∣p∉T ∪\ p p∈ T\∪\ p p ∈ T\ is Y-consistent and (b) Γ∪¬p∣p∈T∪¬p∣p∉T⊧YT ∪\ p p∈ T\∪\ p p ∈ T\ _ 0.0pt 3.83148pt3.0pt 0.0pt$ Y$ 0.0pt 3.83148pt3.0pt 0.0pt$ Y$ 0.0pt 3.2634pt3.0pt 0.0pt$ Y$ 0.0pt 3.26338pt3.0pt 0.0pt$ Y$T. From Γ∪¬p∣p∈T∪¬p∣p∉T ∪\ p p∈ T\∪\ p p ∈ T\ (3) being Y-consistent and Lemma 1, it follows that (3) is both X-consistent and INT-consistent. From the second item, the fact that Y⊆HT Y HT and Proposition 1 it follows Γ∪¬p∣p∈T∪¬p∣p∉T⊧HTT. ∪\ p p∈ T\∪\ p p ∈ T\ _ 0.0pt 7.54004pt3.0pt 0.0pt$ HT$ 0.0pt 7.54004pt3.0pt 0.0pt$ HT$ 0.0pt 6.40483pt3.0pt 0.0pt$ HT$ 0.0pt 6.40483pt3.0pt 0.0pt$ HT$T. (4) Let =⟨(W,≼),V⟩ M= (W, ),V be any intuitionistic model and w∈Ww∈ W satisfying (c) ,w⊧INTΓ M,w _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$ , (d) ,w⊧INT¬p∣p∈T M,w _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$\ p p∈ T\ and (e) ,w⊧INT¬p∣p∉T M,w _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$\ p p ∈ T\. Items (d) and (e) imply that ,w⊧INT¬p∨¬p∣p∈ℙ M,w _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$\ p p p \. By Lemma 3 there exists an intuitionistic ′=⟨(W′,≼′),V′⟩ M = (W , ),V , w′∈W′w ∈ W and a bisimulation ⊆W×W′Z W× W such that ww′wZw and the subframe generated by w′w has an unique maximal world. By Lemma 2, ′,w′⊧INTΓ M ,w _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$ , ′,w′⊧INT¬p∣p∈T M ,w _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$\ p p∈ T\ and ′,w′⊧INT¬p∣p∉T M ,w _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$\ p p ∈ T\. Let us denote by u′∈W′u ∈ W the (unique) maximal world in the subframe generated by w′w . By the monotonicity property of intuitionistic logic, ′,u′⊧INT¬p∣p∈T M ,u _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$\ p p∈ T\ and ′,u′⊧INT¬p∣p∉T M ,u _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$\ p p ∈ T\. Since u′u is maximal V′(u′)=TV (u )=T. In addition, we prove by induction on 0pt((W′,≼′),v′)0pt((W , ),v ), that for all v′∈≼′(w′)v ∈ (w ) (which includes the case w′w as well), ′,v′⊧INTT M ,v _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$T. 1. If depth((W′,v′))=1depth((W ,v ))=1 then v′v is maximal so v′=u′v =u (and we reason as in the base case). 2. For the inductive step, let us assume that 0pt((W′,≼′),v′)=n+10pt((W , ),v )=n+1 and the claim holds for every x∈≺′(v′)x∈ (v ), that is, 0pt((W′,≼′),x)≤n0pt((W , ),x)≤ n. (a) If ≺′(v′)=∅ (v )= , v′v is maximal so V′(v′)=V′(u′)=TV (v )=V (u )=T. (b) If ≺′(v′)≠∅ (v ) = then, by induction hypothesis, ′,x⊧T M ,x T for all x∈≺′(v′)x∈ (v ). From ′,w′⊧INT¬p∣p∉T M ,w _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$\ p p ∈ T\ and w′≼′v′w v , ′,x⊧̸p M ,x p for all x∈≺′(v′)x∈ (v ) and all p∈ℙ∖Tp T. Therefore, V′(x)=TV (x)=T for all for all x∈≺′(v′)x∈ (v ). By Lemma 2.4, there exists a HT model ′=⟨(0,1,≼′),V′⟩ M = (\0,1\, ),V and a bisimulation ′⊆W′×0,1Z W ×\0,1\ such that v′′0v Z 0. By Lemma 2, ′,0⊧HTΓ M ,0 _ 0.0pt 7.54004pt3.0pt 0.0pt$ HT$ 0.0pt 7.54004pt3.0pt 0.0pt$ HT$ 0.0pt 6.40483pt3.0pt 0.0pt$ HT$ 0.0pt 6.40483pt3.0pt 0.0pt$ HT$ , ′,0⊧HT¬p∣p∈T M ,0 _ 0.0pt 7.54004pt3.0pt 0.0pt$ HT$ 0.0pt 7.54004pt3.0pt 0.0pt$ HT$ 0.0pt 6.40483pt3.0pt 0.0pt$ HT$ 0.0pt 6.40483pt3.0pt 0.0pt$ HT$\ p p∈ T\ and ′,0⊧HT¬p∣p∉T M ,0 _ 0.0pt 7.54004pt3.0pt 0.0pt$ HT$ 0.0pt 7.54004pt3.0pt 0.0pt$ HT$ 0.0pt 6.40483pt3.0pt 0.0pt$ HT$ 0.0pt 6.40483pt3.0pt 0.0pt$ HT$\ p p ∈ T\. Thank to (4) it follows ′,0⊧HTT M ,0 _ 0.0pt 7.54004pt3.0pt 0.0pt$ HT$ 0.0pt 7.54004pt3.0pt 0.0pt$ HT$ 0.0pt 6.40483pt3.0pt 0.0pt$ HT$ 0.0pt 6.40483pt3.0pt 0.0pt$ HT$T. From v′′0v Z 0 and Lemma 2, ′,v′⊧INTT M ,v _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$T. Therefore, ′,w′⊧INTT M ,w _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$T. Since ww′wZw , ,w⊧INTT M,w _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$T. Since M was chosen arbitrarily, it follows that Γ∪¬p∣p∈T∪¬p∣p∉T⊧INTT ∪\ p p∈ T\∪\ p p ∈ T\ _ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 9.55234pt3.0pt 0.0pt$ INT$ 0.0pt 8.0975pt3.0pt 0.0pt$ INT$ 0.0pt 8.09749pt3.0pt 0.0pt$ INT$T. By Proposition 1, Γ∪¬p∣p∈T∪¬p∣p∉T⊧XT ∪\ p p∈ T\∪\ p p ∈ T\ _ 0.0pt 3.83148pt3.0pt 0.0pt$ X$ 0.0pt 3.83148pt3.0pt 0.0pt$ X$ 0.0pt 3.2634pt3.0pt 0.0pt$ X$ 0.0pt 3.26338pt3.0pt 0.0pt$ X$T. Therefore, T is a X-safe belief of Γ . Note that the combination of lemmas 3.11 and 3.12 allows us to replace HT by any proper intermediate logic without altering the set of equilibrium models. 4 Temporal Intuitionistic and Intermediate Logics Given a countable, possibly infinite set ℙP of atoms, also called alphabet, our temporal language ℒtL_t consists of formulas generated by the following grammar: φ::=p∈ℙ∣⊥∣φ∧φ∣φ∨φ∣φ→φ∣◦φ∣φ∣φ ::=p → -0.5pt This extends our basic language with temporal modal operators ◦, , and . The intended meaning of these operators is the following: ◦φ -0.5pt means that φ is true at the next time point. φψ ψ means that φ is true until ψ is true. For φψ ψ the meaning is not as direct as for the previous operators. That is, φψ ψ means that ψ is true until both φ and ψ become true simultaneously or ψ is true forever. We also define several common derived operators like the Boolean connectives ⊤⁣:=⁣¬⁣⊥ := , ¬φ:=φ→⊥ := → , φ↔ψ:=(φ→ψ)∧(ψ→φ) ψ:=( →ψ) (ψ→ ), and the unary temporal operators □φ:=⊥φ := (always afterwards) and ◇φ:=⊤φ := (eventually afterwards). A (temporal) theory is a possibly infinite set of temporal formulas. Formulas of ℒtL_t are interpreted over intuitionistic temporal frames. An intuitionistic temporal frame is a tuple =(W,≼,S) D=(W, ,S), where W is a non-empty set of (Kripke) worlds, ≼ is a partial order, and S is a function from W to W satisfying the forward confluence condition: If w≼vw v then S(w)≼S(v)S(w) S(v) for all w,v∈Ww,v∈ W. Conversely, the backward confluence condition stipulates that if S(w)=vS(w)=v and v≼uv u, then there exists t∈Wt∈ W such that w≼tw t and S(t)=uS(t)=u for all w,v,u∈Ww,v,u∈ W. If D satisfies both confluence conditions, we call D a persistent intuitionistic temporal frame. Figure 3(a) (resp. Figure 3(b)) shows a graphical version of the forward (resp. backward) confluence condition. wwS(w)S(w)vvS(v)S(v)S≼ ≼ (a) Forward confluence wwvvttuuSS≼ ≼ (b) Backward confluence Figure 3: Diagrams associated to forward and backward confluence. The above diagrams can always be completed if S is forward or backward confluent (represented by means of dashed arrows). An intuitionistic temporal model, or simply model, is a tuple =⟨,V⟩ M= D,V consisting of an intuitionistic temporal frame =(W,≼,S) D=(W, ,S) equipped with a valuation function V:W→2ℙV:W→ 2^P that is monotone in the sense that if w≼vw v then V(w)⊆V(v)V(w) V(v) for all w,v∈Ww,v∈ W. In the standard way, we define S0(w):=wS^0(w):=w and Sk+1(w):=S(Sk(w))S^k+1(w):=S (S^k(w) ) for k≥0k≥ 0. Regarding the satisfaction relation, the propositional connectives are satisfied as in INT (see Section 2). The satisfaction of the temporal connectives is presented below. 6. ,w⊧◦φ M,w -0.5pt iff ,S(w)⊧φ M,S(w) 7. ,w⊧φψ M,w ψ iff there exists k≥0k≥ 0 such that ,Sk(w)⊧ψ M,S^k(w) ψ and ,Si(w)⊧φ M,S^i(w) for all i∈[0..k)i∈[0..k) 8. ,w⊧φψ M,w ψ iff for all k≥0k≥ 0, either ,Sk(w)⊧ψ M,S^k(w) ψ or ,Si(w)⊧φ M,S^i(w) for some i∈[0..k)i∈[0..k). Figure 4 illustrates the satisfaction relation ‘⊧ ’ (Balbiani et al. 2020). Note that ,x⊧◦p M,x -0.5pt p but ,x⊧̸p M,x p, while ,y⊧p M,y p but ,y⊧̸◦p M,y -0.5pt p. From this, it follows that ,w⊧̸(◦p→p)∨(p→◦p) M,w ( -0.5pt p→ p) (p→ -0.5pt p). wwV(w):=∅V(w):= (x):=∅V(x):= (y):=pV(y):=\p\≼ ≼ Figure 4: Example of an ITLeITL^e model =((W,≼,S),V) M=((W, ,S),V), where reflexivity and transitivity for ≼ are not represented. We refer to the intuitionistic temporal logic interpreted over the class of intuitionistic temporal frames as intuitionistic temporal logic (ITLeITL^e). Formally, defined as ITLe:=φ∈ℒt∣⊧φ,ITL^e:=\ _t D \, where D is an intuitionistic temporal frame. If in addition D is persistent, we denote by ITLp:=φ∈ℒt∣⊧φITL^p:=\ _t D \ the persistent intuitionistic temporal logic (ITLpITL^p), i.e., the intuitionistic temporal logic interpreted over the class of the intuitionistic persistent frames. The following proposition shows that ITLe≠ITLpITL^e =ITL^p. Proposition 4.14 (Balbiani et al. 2020). The formulas (◦p→◦q)→◦(p→q) ( -0.5pt p→ -0.5pt q )→ -0.5pt (p→ q ) and (◇p→□q)→□(p→q) ( p→ q )→ (p→ q ) are valid over the class of persistent intuitionistic temporal frames. The formulas presented in the proposition above are valid in ITLpITL^p but not in ITLeITL^e. This leads to the following result. Corollary 4.15 (Balbiani et al. 2020). ITLe≠ITLpITL^e =ITL^p. We remark that intuitionistic temporal frames impose minimal conditions on S and ≼ in order to preserve the monotonicity of truth of formulas, in the sense that if ,w⊧ITLeφ M,w _ 0.0pt 8.64653pt3.0pt 0.0pt$ ^e$ 0.0pt 9.48969pt3.0pt 0.0pt$ ^e$ 0.0pt 9.34174pt3.0pt 0.0pt$ ^e$ 0.0pt 10.0784pt3.0pt 0.0pt$ ^e$ and w≼vw v then ,v⊧ITLeφ M,v _ 0.0pt 8.64653pt3.0pt 0.0pt$ ^e$ 0.0pt 9.48969pt3.0pt 0.0pt$ ^e$ 0.0pt 9.34174pt3.0pt 0.0pt$ ^e$ 0.0pt 10.0784pt3.0pt 0.0pt$ ^e$ . In the propositional case, the monotonicity property is guaranteed by the use of a monotone valuation. In the temporal case, we additionally require the forward confluence property, which relates ≼ and S. Forward confluence ensures the satisfaction of temporal formulas is also monotone with respect to ≼ . The backward confluence property, while not required for monotonicity, allows us to show that maximal points are preserved under the temporal successor relation: if w is a ≼ -maximal point, then S(w)S(w) is also maximal (see Proposition 4.18). Proposition 4.16 (monotonicity; Balbiani et al. 2020). Let =⟨(W,≼,S),V⟩ M= (W, ,S),V be an intuitionistic temporal model. For any w,v∈Ww,v∈ W, if w≼vw v then for any temporal formula φ , ,w⊧φ M,w implies ,v⊧φ M,v . Contrary to the non-temporal case (see Section 2), consistency in ITLeITL^e cannot be reduced to consistency in plain LTL. We provide here the counterexample proposed by Balbiani et al. (2020): consider Γ:=¬◦p,¬◦¬p :=\ -0.5pt p, -0.5pt p\. In LTL, this theory is equivalent to ◦¬p,◦p\ -0.5pt p, -0.5pt p\ and it is inconsistent. However, the ITLeITL^e model M shown in Figure 5 satisfies Γ at the world w (in symbols, ,w⊧Γ M,w ). Note that, in this case, S is forward, but not backward, confluent. Hence, the decidability of the satisfiability problem in ITLeITL^e is not a corollary of the LTL case. wwV(w):=∅V(w):= (v):=∅V(v):= (u):=pV(u):=\p\S≼ Figure 5: Example of an ITLeITL^e model satisfying Γ:=¬◦p,¬◦¬p :=\ -0.5pt p, -0.5pt p\. Reflexivity and transitivity of ≼ are omitted for the sake of clarity. When adding the backward confluence property, Γ becomes inconsistent. However, adding such condition (i.e. replacing ITLeITL^e by ITLpITL^p) does not allow us to reduce ITLpITL^p-consistency to LTL-consistency either. To show this, we consider the theory Γ:=□¬p,¬□p :=\ p, p\. In LTL, Γ is equivalent to □p,¬□p\ p, p\ and it is clearly inconsistent. Now, consider the model =⟨(ℕ×ℕ,≼,S),V⟩ M= (N×N, ,S),V shown in Figure 6. In this case, the valuation V is defined as V((i,j)):=pV((i,j)):=\p\ if i<ji<j and ∅ otherwise. In fact, M is a ITLpITL^p model since it possesses both forward and backward confluence properties. Moreover, 1) For every i≥0i≥ 0 there exist j>0j>0 such that ,(i,j)⊧p M,(i,j) p, so ,(i,0)⊧¬p M,(i,0) p, for every i≥0i≥ 0. Consequently, ,(0,0)⊧□¬p M,(0,0) p. 2) For every j≥0j≥ 0 there exist i≥0i≥ 0 such that ,(i,j)⊧̸p M,(i,j) p. Therefore, ,(0,j)⊧̸□p M,(0,j) p, for every j≥0j≥ 0. Consequently, ,(0,0)⊧¬□p M,(0,0) p. As a consequence, ,(0,0)⊧ΓM,(0,0) . We remark that the depth of ≼ is not finite in M. (0,0)(0,0)(1,0)(1,0)(2,0)(2,0)(3,0)(3,0)(4,0)(4,0)(5,0)(5,0)(6,0)(6,0)⋯·s(,)(0,1)(1,1)(1,1)(2,1)(2,1)(3,1)(3,1)(4,1)(4,1)(5,1)(5,1)(6,1)(6,1)⋯·s(,)(0,2)(,)(1,2)(2,2)(2,2)(3,2)(3,2)(4,2)(4,2)(5,2)(5,2)(6,2)(6,2)⋯·s(,)(0,3)(,)(1,3)(,)(2,3)(3,3)(3,3)(4,3)(4,3)(5,3)(5,3)(6,3)(6,3)⋯·s⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ ≼ Figure 6: A ITLpITL^p model M satisfying Γ:=□¬p,¬□p :=\\ p, p\\ at (0,0)(0,0). The proposition p is true in the worlds displayed boldface while false in those that are not. Reflexivity and transitivity of ≼ are not represented for the sake of readability. Such a counterexample leads to the following result. Proposition 4.17. ITLpITL^p-consistency cannot be reduced to LTL-consistency. 4.1 Intermediate Temporal Logics As we have shown in the previous section, intermediate temporal logics defined extending ITLpITL^p with new axioms may not preserve consistency. There is one extra condition that we need to impose on the intuitionistic temporal frames: the intuitionistic depth (≼ -depth, for short) must be finite. Finite depth can be achieved by forcing ITLpITL^p to validate the schema bd_n, for some n≥1n≥ 1, as shown in Lemma 1. We define the family ITLBDnITL BD_n of intuitionistic temporal logics as ITLBDn:=φ∈ℒt∣⊧φ,ITL BD_n:=\ _t D \, where =(W,≼,S) D=(W, ,S) is a ITLpITL^p frame with 0pt(W,≼)≤n0pt(W, )≤ n. Observation 1 ITLBD1ITL BD_1 corresponds to LTL, that is, ITLBD1ITL BD_1 frames =(W,≼,S) D=(W, ,S) such that 0pt(W,≼)=10pt(W, )=1.666Note that the axiom schema bd_1 corresponds to the excluded middle axiom, which is added to INT to get classical logic and to ITLeITL^e to obtain LTL. Proposition 4.18. For all ITLBDnITL BD_n frame =(W,≼,S) D=(W, ,S) and for all w∈Ww∈ W, if w is maximal w.r.t. ≼ then S(w)S(w) is maximal. Note that the proposition above can be proved only if the backward-confluence property holds. In addition, using the result above, we can prove that ITLBDnITL BD_n-consistency can be reduced to LTL-consistency. Lemma 4.19. Any temporal theory Γ is ITLBDnITL BD_n-consistent iff Γ is LTL-consistent. To the best of our knowledge, the family of intermediate temporal logics has not been defined in the literature. We define those logics as extensions of ITLBDnITL BD_n.777In other words, we want ITLBDnITL BD_n to play the same role as INT does in the propositional case. Definition 4.20 (Intermediate temporal logic). An intermediate temporal logic in the language ℒtL_t is any set of formulas X satisfying the following conditions: 1. ITLBDn⊆X⊆LTLITL BD_n X LTL 2. X is closed under modus ponens, i.e., φ,φ→ψ∈X , →ψ∈ X implies ψ∈Xψ∈ X 3. X is closed under necessitation, i.e., ψ∈Xψ∈ X implies ◦ψ∈X -0.5pt ψ∈ X and □ψ∈X ψ∈ X 4. X is closed under uniform substitution, i.e., φ∈X ∈ X implies φ∈X ∈ X for any φ∈ℒt _t and a substitution s As in the propositional case, an intermediate temporal logic is said to be proper if it is different from LTL. Assuming that any intermediate temporal logic extends ITLBDnITL BD_n, the following result directly follows from Lemma 4.19. Corollary 4.21. Let X be any intermediate temporal logic. Any temporal theory Γ is X-consistent iff Γ is LTL-consistent. The following proposition shows that the depth of a generated (intuitionistic) subframe does not increase between two worlds x and S(x)S(x). Proposition 4.22. For any intuitionistic temporal frame =(W,≼,S) D=(W, ,S) and for an w∈Ww∈ W and for any n≥1n≥ 1, if 0pt((W,≼),w)≤n0pt((W, ),w)≤ n then 0pt((W,≼),S(w))≤n0pt((W, ),S(w))≤ n. Similar to the propositional case, intermediate temporal logics defined as extensions of ITLBDnITL BD_n satisfy the following proposition. Proposition 4.23. Let X and Y be two intermediate temporal logics satisfying X⊆Y X Y. A theory Γ is X-consistent iff Γ is Y-consistent. Furthermore, semantic entailment is preserved when strengthening the logic. Proposition 4.24. Let X and Y be two intermediate temporal logics satisfying X⊆Y X Y. For any theories Γ and Δ , Γ⊧XΔ implies Γ⊧YΔ. _ 0.0pt 3.83148pt3.0pt 0.0pt$ X$ 0.0pt 3.83148pt3.0pt 0.0pt$ X$ 0.0pt 3.2634pt3.0pt 0.0pt$ X$ 0.0pt 3.26338pt3.0pt 0.0pt$ X$ implies _ 0.0pt 3.83148pt3.0pt 0.0pt$ Y$ 0.0pt 3.83148pt3.0pt 0.0pt$ Y$ 0.0pt 3.2634pt3.0pt 0.0pt$ Y$ 0.0pt 3.26338pt3.0pt 0.0pt$ Y$ . The strongest proper intermediate temporal logic is the logic of here-and-there (THT; Balbiani and Diéguez 2016). In our setting, this logic is obtained by adding Axiom (2) to ITLBD2ITL BD_2.888It can also be obtained by adding Axiom (2) to ITLpITL^p. However, in this paper, we take ITLBDnITL BD_n as the root of our constructions. THT frames are of the form (W,≼,S)(W, ,S) where W W = = ℕ×0,1, ×\0,1\, ≼ = = ((i,h),(i,t))∣((i,h),(i,t))∈W×W such that h≤t and \((i,h),(i,t)) ((i,h),(i,t))∈ W× W such that h≤ t\ and S S = = ((i,k),(i+1,k))∣((i,k),(i+1,k))∈W×W. \((i,k),(i+1,k)) ((i,k),(i+1,k))∈ W× W\. In the definition above, pairs of the form (i,0)(i,0) (resp. (i,1)(i,1)) represent the “here” (resp. “there”) world at each time point i. 4.2 Bisimulations for Intuitionistic Temporal Logics The notion of intuitionistic temporal bisimulation was introduced in (Balbiani et al. 2020) and we use it in what follows to contract intuitionistic temporal models into THT. Given two intuitionistic temporal models 1=⟨(W1,≼1,S1),V1⟩ M_1= (W_1, _1,S_1),V_1 and 2=⟨(W2,≼2,S2),V2⟩ M_2= (W_2, _2,S_2),V_2 , a relation ⊆W1×W2Z W_1× W_2 is an intuitionistic temporal bisimulation, if it satisfies Conditions C1-C3 together with the following ones: C5 If w1w2w_1Zw_2 then S(w1)S(w2)S(w_1)ZS(w_2); C6 If w1w2w_1Zw_2 then for all k1≥0k_1≥ 0 there exists k2≥0k_2≥ 0 and (v1,v2)∈W1×W2(v_1,v_2)∈ W_1× W_2 such that (a) v2≼Sk2(w2)v_2 S^k_2(w_2), Sk1(w1)≼v1S^k_1(w_1) v_1 and v1v2v_1Zv_2 and (b) for all j2∈[0..k2)j_2∈[0..k_2) there exists j1∈[0..k1)j_1∈[0..k_1) and (u1,u2)∈W1×W2(u_1,u_2)∈ W_1× W_2 such that Sj1(w1)≼u1S^j_1(w_1) u_1, u2≼Sj2(w2)u_2 S^j_2(w_2) and u1u2u_1Zu_2. C7 If w1w2w_1Zw_2 then for all k2≥0k_2≥ 0 there exists k1≥0k_1≥ 0 and (v1,v2)∈W1×W2(v_1,v_2)∈ W_1× W_2 such that (a) v1≼Sk1(w1)v_1 S^k_1(w_1), Sk2(w2)≼v2S^k_2(w_2) v_2 and v1v2v_1Zv_2 and (b) for all j1∈[0..k1)j_1∈[0..k_1) there exists j2∈[0..k2)j_2∈[0..k_2) and (u1,u2)∈W1×W2(u_1,u_2)∈ W_1× W_2 such that Sj2(w2)≼u2S^j_2(w_2) u_2, u1≼Sj1(w1)u_1 S^j_1(w_1) and u1u2u_1Zu_2. C8 If w1w2w_1Zw_2 then for all k2≥0k_2≥ 0 there exists k1≥0k_1≥ 0 and (v1,v2)∈W1×W2(v_1,v_2)∈ W_1× W_2 such that (a) v2≼Sk2(w2)v_2 S^k_2(w_2), Sk1(w1)≼v1S^k_1(w_1) v_1 and v1v2v_1Zv_2 and (b) for all j1∈[0..k1)j_1∈[0..k_1) there exists j2∈[0..k2)j_2∈[0..k_2) and (u1,u2)∈W1×W2(u_1,u_2)∈ W_1× W_2 such that Sj1(w1)≼u1S^j_1(w_1) u_1, u2≼Sj2(w2)u_2 S^j_2(w_2) and u1u2u_1Zu_2. C9 If w1w2w_1Zw_2 then for all k1≥0k_1≥ 0 there exists k2≥0k_2≥ 0 and (v1,v2)∈W1×W2(v_1,v_2)∈ W_1× W_2 such that (a) v1≼Sk1(w1)v_1 S^k_1(w_1), Sk2(w2)≼v2S^k_2(w_2) v_2 and v1v2v_1Zv_2 and (b) for all j2∈[0..k2)j_2∈[0..k_2) there exists j1∈[0..k1)j_1∈[0..k_1) and (u1,u2)∈W1×W2(u_1,u_2)∈ W_1× W_2 such that Sj2(w2)≼u2S^j_2(w_2) u_2, u1≼Sj1(w1)u_1 S^j_1(w_1), and u1u2u_1Zu_2. Conditions C5-C9 play the same role as conditions C2- C3 in the case of INT but they affect the temporal modalities. More precisely, Conditions C6 and C7 (resp. conditions C8 and C9) simulate the behavior of the until (resp. release) operator. Note that, due confluence of both ≼ and S, the forth and back conditions for the binary temporal modalities involve both relations. Condition C5, which is used to simulate the next modality, is not divided into two conditions because the next operator is interpreted in terms of a function. Given two intuitionistic temporal models 1=⟨(W1,≼1,S1),V1⟩ M_1= (W_1, _1,S_1),V_1 and 2=⟨(W2,≼2,S2),V2⟩ M_2= (W_2, _2,S_2),V_2 with w1∈W1w_1∈ W_1 and w2∈W2w_2∈ W_2, we say that 1 M_1 and 2 M_2 are bisimilar, if there exists an intuitionistic temporal bisimulation Z between W1W_1 and W2W_2 such that w1w2w_1Zw_2. The following lemma states that two bisimilar Kripke worlds satisfy the same temporal formulas. Lemma 4.25 (Balbiani et al. 2020). Given two models 1=⟨(W1,≼1,S1),V1⟩ M_1= (W_1, _1,S_1),V_1 and 2=⟨(W2,≼2,S2),V2⟩ M_2= (W_2, _2,S_2),V_2 and a bisimulation Z on W1×W2W_1× W_2, we have for all w1∈W1w_1∈ W_1 and for all w2∈W2w_2∈ W_2, if w1w2w_1Zw_2 then for all φ∈ℒt _t, 1,w1⊧φ M_1,w_1 iff 2,w2⊧φ M_2,w_2 . In the proof of the previous lemma, Condition C1 is used to establish the case of propositional variables. Conditions C3 and C2 are used to handle the case of implication. Conditions C7 and C6 are employed for the operator, while Conditions C9 and C8 are used for the operator. Finally, Condition C5 is used in the proof of the case of the ◦ connective. In (Balbiani et al. 2020), where ITLeITL^e and ITLpITL^p are studied in detail, the authors proved that both satisfiability (resp. validity) on arbitrary ITLeITL^e models is equivalent to satisfiability (resp. validity) on the so-called expanding models, defined in the following theorem. Theorem 4.26 (Balbiani et al. 2020; Boudou et al. 2017). Every ITLeITL^e model M can be unfolded into an expanding model ′=⟨(W′,≼′,S′),V′⟩ M = (W , ,S ),V , which satisfies the following properties: 1. For all i≥0i≥ 0 and w′∈W′w ∈ W , the intuitionistic subframe generated by each S′⁣i(w′)S i(w ) is a tree, 2. the sequence of trees induced by S′⁣i(w′)S i(w ) is a sequence of disjoint trees, and 3. for all v′∈W′v ∈ W and for all i≥0i≥ 0, if S′⁣i(w′)≼v′S i(w ) v then S′⁣i+1(w′)≼S′(v′)S i+1(w ) S (v ), that is, S′(v′)S (v ) falls in the tree generated by S′⁣i+1(w′)S i+1(w ). We refer the reader to (Balbiani et al. 2020) for more details about such unfolding. Since ITLBDnITL BD_n is contained in ITLeITL^e then the construction above can be also applied to models of finite ≼ -depth. From now on, when displaying the ITLBDnITL BD_n models, we consider expanding models. Bisimulations for intuitionistic temporal logics allow us to extend lemmas 3 and 2.4 to the temporal case. Lemma 4.27. Let =⟨(W,≼,S),V⟩ M= (W, ,S),V be an ITLBDnITL BD_n model and let w∈Ww∈ W be such that ,w⊧□(¬p∨¬p)∣p∈ℙ M,w \ ( p p) p \. Then, there exists an ITLBDnITL BD_n model ′=⟨(W′,≼′,S′),V′⟩ M = (W , ,S ),V , w′∈W′w ∈ W and a bisimulation ⊆W×W′Z W× W such that, for all i≥0i≥ 0 both Si(w)S′⁣i(w′)S^i(w)ZS i(w ) and each (intuitionistic) subframe generated by each S′⁣i(w′)S i(w ) has an unique maximal world, uiu_i, w.r.t. ≼′ . Proof 4.28. Since ,w⊧□(¬p∨¬p)∣p∈ℙ M,w \ ( p p) p \ implies ,Si(w)⊧¬p∨¬p∣p∈ℙ M,S^i(w) \ p p p \, for all i≥0i≥ 0. Since M is an ITLBDnITL BD_n model, the intuitionistic depth of (W,≼)(W, ) is finite and, because of Proposition 2, all maximal worlds in ≼(Si(w)) (S^i(w)) satisfy the same propositional variables. Let us define the ITLBDnITL BD_n model ′:=⟨(W′,≼′,S′),V′⟩ M := (W , ,S ),V , where its corresponding frame is defined as: W′ W :=v,ui∣i≥0, v is ≼−maximal in≼(Si(w)) and ui∉W is a fresh world; :=\v,u_i i≥ 0 , v is - maximal in (S^i(w)) and u_i ∈ W is a fresh world\; ≼′ :=(ui,ui),(v,ui)∣i≥0,v,ui∈W′ and Si(w)≼v :=\(u_i,u_i),(v,u_i) i≥ 0,\;v,u_i∈ W and S^i(w) v\ ∪(v,v′)∣v,v′∈W′ and v≼v′; ∪\(v,v ) v,v ∈ W and v v \; S′ S :=(ui,ui+1),(v,ui+1)∣i≥0,Si(w)≼v and S(v)=x, with x≼−maximal :=\(u_i,u_i+1),(v,u_i+1) i≥ 0,\;S^i(w) v and S(v)=x , with x - maximal\ ∪(v,v′)∣(v,v′)∈W′×W′ and vSv′. ∪\(v,v ) (v,v )∈ W × W and vSv \. We verify that it (W′,≼′,S′)(W , ,S ) is an ITLBDnITL BD_n frame. Since ≼ is a partial order relation, by construction, ≼′ is. Since S is a function, it can be verified that S′S is a function as well. Also by construction, (W′,≼′)(W , ) is of finite depth. We readily check that S′S and ≼′ are forward and backward confluent. For the forward confluence let us consider v,v′∈Wv,v ∈ W satisfying v≼′v′v v . In order to prove that S′(v)≼′S′(v′)S (v) S (v ) we need to consider several cases. 1. If v=uiv=u_i, for some i≥0i≥ 0, by construction, v′=uiv =u_i too. Therefore, ui+1=S′(v)≼′S′(v′)=ui+1u_i+1=S (v) S (v )=u_i+1. 2. If v≠uiv =u_i but v′=uiv =u_i then S′(v′)=ui+1S (v )=u_i+1 and v∈Wv∈ W. If S(v)S(v) is maximal then ui+1=S′(v)≼S′(v′)=ui+1u_i+1=S (v) S (v )=u_i+1 by definition. If not, take S′(v):=S(v)∈W′S (v):=S(v)∈ W . By construction, S′(v)≼ui+1S (v) u_i+1. 3. If v≠uiv =u_i and v′≠uiv =u_i it follows that v≼v′v v . Since ≼ and S are forward confluent then S(v)≼S(v′)S(v) S(v ). If either S(v)S(v) or S(v′)S(v ) are maximal w.r.t. ≼ , we follow a similar reasoning as in the previous two items in order to check S′(v)≼′S′(v′)S (v) S (v ). If neither S(v)S(v) nor S(v′)S(v ) are maximal then S′(v)=S(v)S (v)=S(v) and S′(v′)=S(v′)S (v )=S(v ) so S′(v)≼′S′(v′)S (v) S (v ) by construction. In any case we conclude that, if v≼′v′v v then S′(v)≼S′(v′)S (v) S (v ) as requested. For the backward confluence, let us take three arbitrary worlds v,y,z∈W′v,y,z∈ W satisfying S′(v)=y≼′zS (v)=y z. We show that there exists t∈W′t∈ W such v≼′tv t and S′(t)=zS (t)=z. As for the forward case, we proceed by cases. 1. If y=ui+1y=u_i+1 then z=ui+1z=u_i+1 by construction. Since S′(v)=ui+1S (v)=u_i+1 then take t:=uit:=u_i. By definition, v≼′uiv u_i and S′(ui)=ui+1=zS (u_i)=u_i+1=z. 2. If y≠ui+1y =u_i+1 and z=ui+1z=u_i+1 then take t:=uit:=u_i. v≼′tv t by construction and S′(ui)=ui+1=zS (u_i)=u_i+1=z. 3. If y≠ui+1y =u_i+1 and z≠ui+1z =u_i+1 then y,z∈Wy,z∈ W, y≼zy z and z is not maximal w.r.t. ≼ . Since y≠ui+1y =u_i+1 then S′(v)=y≠ui+1S (v)=y =u_i+1. Therefore, v∈Wv∈ W. By construction, S(v)=yS(v)=y. Because of the backward confluence property, there exist x∈Wx∈ W such that v≼xv x and S(x)=zS(x)=z. The world x cannot be maximal, otherwise z would be maximal in view of Proposition 4.18 and it would not belong to W′W . By construction, x∈W′x∈ W and S′(x)=zS (x)=z. Set t:=xt:=x so we would get v≼′xv x and S′(x)=zS (x)=z. As a consequence, (W′,≼′,S)(W , ,S) is an ITLBDnITL BD_n frame. wwv0,0v_0,0u0,0u_0,0≼ 0,1u_0,1≼ ≼ 0,1v_0,1u0,2u_0,2≼ ≼ 1(w)S^1(w)v1,0v_1,0u1,0u_1,0≼ ≼ 1,1v_1,1u1,2u_1,2≼ ≼ 2(w)S^2(w)v2,0v_2,0u2,0u_2,0≼ ≼ 2,1v_2,1u2,1u_2,1≼ ≼ ⋯·s⋯·s⋯·sSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSwwv0,0v_0,0≼′ u0u_0v0,1v_0,1≼′ ≼′ S1(w)S^1(w)v1,0v_1,0≼′ u1u_1v1,1v_1,1≼′ ≼′ S1(w)S^1(w)v2,0v_2,0≼′ u2u_2v2,1v_2,1≼′ ≼′ ⋯·s⋯·s⋯·s M′ M S′S S′S S′S S′S S′S S′S S′S S′S S′S S′S S′S S′S Figure 7: Two ITLBDnITL BD_n models =⟨(W,≼,S),V⟩ M= (W, ,S),V and ′=⟨(W′,≼′,S′),V′⟩ M = (W , ,S ),V . Under the assumption that ,w⊧□(¬p∨¬p)∣p∈ℙ M,w \ ( p p) p \, for all i≥0i≥ 0, all maximal worlds in ≼(Si(w)) (S^i(w)) satisfy the same atoms. By setting V′(v):=V(v)V (v):=V(v) for every world v∈W∩W′v∈ W∩ W and, for all i≥0i≥ 0, V′(ui):=V(x)V (u_i):=V(x), with x a maximal world in ≼(Si(w)) (S^i(w)), it can be verified that the relation Z displayed in terms of red dashed lines is a bisimulation between M and ′ M . The reflexivity and transitivity of ≼ and ≼′ is not represented for the sake of readability. Let us define V′V as V′(v):=V(v)V (v):=V(v) if v≠uiv =u_i and V′(ui):=V(x)V (u_i):=V(x) with x being any maximal world in ≼(Si(w)) (S^i(w))999Note that, since M is a ITLBDnITL BD_n model, such x always exists. Moreover, since by assumption ,Si(w)⊧¬p∨¬p∣p∈ℙ M,S^i(w) \ p p p \, all ≼ -maximal worlds in ≼(Si(w)) (S^i(w)) satisfy the same propositions., for all i≥0i≥ 0. We define the relation ⊆W×W′Z W× W as follows: := := (v,v)∣v∈W and v∈W′ $v,v) v∈ W and v∈ W \ ∪(v,ui)∣v∈W,Si(w)≼v and v is maximal w.r.t.≼. ∪\(v,u_i) v∈ W,S^i(w) v and v is maximal w.r.t. \. It can be checked that Z is a bisimulation. Figure 7 provides an example of an ITLBDnITL BD_n model M and its bisimilar model ′ M owning an unique ≼′ -maximal world uiu_i per time instant. Lemma 4.29 (Contraction lemma for ITLBDnITL BD_n). Let =⟨(W,≼,S),V⟩ M= (W, ,S),V be an ITLBDnITL BD_n model and let w∈Ww∈ W. If for all i≥0i≥ 0 1. there exists an unique maximal world, denoted by uiu_i, in ≼(Si(w)) (S^i(w)) and 2. V(v)=Ti⊆ℙV(v)=T_i for all Si(w)≺vS^i(w) v then there exists a THT model ′=⟨(ℕ×0,1,≼′,S′),V′⟩ M = (N×\0,1\, ,S ),V and a bisimulation ⊆W×(ℕ×0,1)Z W×(N×\0,1$ such that, for all i≥0i≥ 0, Si(w)S′⁣i((0,0))S^i(w)ZS i((0,0)) and Si(u0)S′⁣i((0,1))S^i(u_0)ZS i((0,1)). Proof 4.30. Let us define the THT model ′=⟨(ℕ×0,1,≼′,S′),V′⟩ M = (N×\0,1\, ,S ),V where V′V is defined as V′((i,0)):=V(Si(w))V ((i,0)):=V(S^i(w)) and V′((i,1)):=V(ui)V ((i,1)):=V(u_i), for all i≥0i≥ 0101010All uiu_is exist because of Condition 1.. Let us define now the relation ⊆W×(ℕ×0,1)Z W×(N×\0,1\) as :=(Si(w),(i,0)),(v,(i,1))∣i≥0 and v∈≺(Si(w)).Z:=\(S^i(w),(i,0)),(v,(i,1)) i≥ 0 and v∈ (S^i(w))\. (5) w0w_0v0,0v_0,0≼ 0u_0v0,1v_0,1≼ ≼ ≼ 1w_1v1,0v_1,0≼ 1u_1v1,1v_1,1≼ ≼ ≼ 2w_2v2,0v_2,0≼ 2u_2v2,1v_2,1≼ ≼ ≼ ⋯·s⋯·s⋯·sSSSSSSSSSSSSSSSSSSSSSSSS(0,0)(0,0)(0,1)(0,1)≼′ (1,0)(1,0)(1,1)(1,1)≼′ (2,0)(2,0)(2,1)(2,1)≼′ ⋯·s⋯·s M′ M S′S S′S S′S S′S S′S S′S Figure 8: Example of model contraction. =⟨(W,≼,S),V⟩ M= (W, ,S),V is an ITLBDnITL BD_n model and ′=⟨(ℕ×0,1,≼′,S′),V′⟩ M = (N×\0,1\, ,S ),V is a THT model. Under the assumption that every world v∈≺(Si(w))v∈ (S^i(w)) satisfies exactly the same set of propositional variables, we can set V′((i,0)):=V(wi)V ((i,0)):=V(w_i) and V′((i,1)):=V(ui)V ((i,1)):=V(u_i), for all i≥0i≥ 0. The relation Z, displayed in red dashed lines, is a bisimulation between M and ′ M . The reflexivity and transitivity of ≼′ and ≼ is not represented for the sake of readability. It can be checked that Z is an intuitionistic temporal bisimulation between M and ′ M . The condition for the propositional variables is satisfied because of Condition 2. The other conditions can be easily checked. Figure 8 shows an example of how a bisimulation between an ITLBDnITL BD_n model M and a THT model ′ M , which can be constructed whenever M satisfies the preconditions 1 and 2 stated in this lemma. 4.3 Temporal Equilibrium Logic Given two THT models ′=⟨(W,≼,S),V′⟩ M = (W, ,S),V and =⟨(W,≼,S),V⟩ M= (W, ,S),V , we define ′≤ M ≤ M if V′((i,1))=V((i,1))V ((i,1))=V((i,1)) and V′((i,0))⊆V((i,0))V ((i,0)) V((i,0)) for all i≥0i≥ 0, and ′= M = M if V′((i,x))=V((i,x))V ((i,x))=V((i,x)) for all i≥0i≥ 0 and x∈0,1x∈\0,1\. Strict inequality ′< M < M is defined as ′≤ M ≤ M and ′≠ M ≠ M. Finally, we also say that M is total if V((i,0))=V((i,1))V((i,0))=V((i,1)), for all i≥0i≥ 0. The following result is a corollary of Proposition 4.16. Corollary 4.31 (Satisfaction of negation). For any THT model =⟨(W,≼,S),V⟩ M= (W, ,S),V , for any i≥0i≥ 0 and for all φ∈ℒt _t, ,(i,0)⊧¬φ M,(i,0) iff ,(i,1)⊧̸φ M,(i,1) Definition 4.32. We say that a total THT model =⟨(W,≼,S),V⟩ M= (W, ,S),V is an equilibrium logic of a temporal formula φ if 1. ,(0,0)⊧φ M,(0,0) and 2. there is no THT model ′ M such that ′< M < M and ′,(0,0)⊧φ M ,(0,0) . Temporal Equilibrium Logic (TEL for short) is the nonmonotonic logic induced by the temporal equilibrium models. 5 Two Fixpoint Characterisations of Temporal Equilibrium Logic In this section, we extend the fixpoint characterizations presented in Section 3 to the temporal case. In order to extend Pearce’s characterization to the TEL case, we need to reformulate some of his definitions. In this section, given a THT model M, we redefine ℎ():=φ∣,(0,0)⊧THTφ.Th( M):=\ M,(0,0) _ 0.0pt 10.86241pt3.0pt 0.0pt$ THT$ 0.0pt 10.86241pt3.0pt 0.0pt$ THT$ 0.0pt 9.63417pt3.0pt 0.0pt$ THT$ 0.0pt 9.63414pt3.0pt 0.0pt$ THT$ \. Proposition 5.33. Let =⟨(W,≼,S),V⟩ M= (W, ,S),V be a temporal equilibrium model of Γ . For every THT model ′=⟨(W,≼,S),V′⟩ M = (W, ,S),V , if ′,(0,0)⊧Γ∪¬φ∣φ∉ℎ() M ,(0,0) ∪\ ( M)\, then V((i,1))=V′((i,1))=V′((i,0))V((i,1))=V ((i,1))=V ((i,0)) for all i≥0i≥ 0. Proof 5.34. Assume towards a contradiction that ′,(0,0)⊧Γ∪¬φ∣φ∉ℎ() M ,(0,0) ∪\ ( M)\ but there exists i≥0i≥ 0 such that not V((i,1))=V′((i,1))=V′((i,0))V((i,1))=V ((i,1))=V ((i,0)). We first consider the case where V((i,1))≠V′((i,1))V((i,1)) =V ((i,1)). There are two cases: • If V((i,1))⊈V′((i,1))V((i,1)) V ((i,1)), there exists some p∈V((i,1))p∈ V((i,1)) such that p∉V′((i,1))p ∈ V ((i,1)). Since p∈V((i,1))p∈ V((i,1)), then ,(0,1)⊧◦ip M,(0,1) -0.5pt ^ip. Since M is a total model, it follows that ,(0,0)⊧◦ip M,(0,0) -0.5pt ^ip and ,(0,0)⊧̸¬◦ip M,(0,0) -0.5pt ^ip. Therefore, ¬◦ip∉ℎ() -0.5pt ^ip ( M). Since ′,(0,0)⊧Γ∪¬φ∣φ∉ℎ() M ,(0,0) ∪\ ( M)\, then ′,(0,0)⊧¬◦ip M ,(0,0) -0.5pt ^ip. By Proposition 4.16, ′,(0,1)⊧¬◦ip M ,(0,1) -0.5pt ^ip. Since the world (0,1)(0,1) is a classical world, ′,(0,1)⊧◦ip M ,(0,1) -0.5pt ^ip so p∈V′((i,1))p∈ V ((i,1)): a contradiction. • If V((i,1))⊉V′((i,1))V((i,1)) V ((i,1)), there exists some p∈V′((i,1))p∈ V ((i,1)) such that p∉V((i,1))p ∈ V((i,1)). Since p∉V((i,1))p ∈ V((i,1)), then ,(0,1)⊧̸◦ip M,(0,1) -0.5pt ^ip. By Proposition 4.16, ,(0,0)⊧̸◦ip M,(0,0) -0.5pt ^ip. Therefore, ◦ip∉ℎ() -0.5pt ^ip ( M). Since ′,(0,0)⊧Γ∪¬φ∣φ∉ℎ() M ,(0,0) ∪\ ( M)\ then ′,(0,0)⊧¬◦ip M ,(0,0) -0.5pt ^ip. By the satisfaction relation it follows that ′,(0,1)⊧̸◦ip M ,(0,1) -0.5pt ^ip, so p∉V′((i,1))p ∈ V ((i,1)): a contradiction. Therefore, we can assume that V((i,1))=V′((i,1))V((i,1))=V ((i,1)), for all i≥0i≥ 0. For the case, V′((i,0))≠V′((i,1))V ((i,0)) =V ((i,1)), we can conclude that V′((i,0))⊂V′((i,1))V ((i,0))⊂ V ((i,1)). Therefore, ′< M < M. Since M is a temporal equilibrium model of Γ then, ′,(0,0)⊧̸Γ M ,(0,0) , so ′,(0,0)⊧̸Γ∪¬φ∣φ∉ℎ() M ,(0,0) ∪\ ( M)\: a contradiction. In the temporal case, we can obtain the same result by replacing HT for THT as underlying logic, as stated in the following proposition. Lemma 5.35. For any theory Γ and any total THT model M, the following items are equivalent: 1) M is a temporal equilibrium model of Γ 2) Γ∪¬φ∣φ∉ℎ()⊧THTφ ∪\ ( M)\ _ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ iff φ∈ℎ() ( M) for all φ∈ℒt _t. Proof 5.36. To prove that Item 1) implies Item 2) we assume that Item 1) holds but 2) does not. Then, M is a temporal equilibrium model of Γ but there exists a formula φ∈ℒt _t for which one of the following two cases hold: • Γ∪¬φ∣φ∉ℎ()⊧THTφ ∪\ ( M)\ _ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ but φ∉ℎ() ( M): in this case, since M is a temporal equilibrium model of Γ then M is total and, in addition, ,(0,0)⊧Γ M,(0,0) . We can easily check that ,(0,0)⊧¬φ∣φ∉ℎ() M,(0,0) \ ( M)\. Therefore, ,(0,0)⊧φ M,(0,0) which contradicts φ∉ℎ() ( M). • φ∈ℎ() ( M) but Γ∪¬φ∣φ∉ℎ()⊧̸THTφ ∪\ ( M)\ _ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ : in this case, there exists ′=⟨(W,≼,S),V′⟩ M = (W, ,S),V such that ′,(0,0)⊧Γ∪¬φ∣φ∉ℎ() M ,(0,0) ∪\ ( M)\ but ′,(0,0)⊧̸φ M ,(0,0) . From ′,(0,0)⊧Γ∪¬φ∣φ∉ℎ() M ,(0,0) ∪\ ( M)\ and Proposition 5.33 it follows V′=V =V. Therefore, ,(0,0)⊧̸φ M,(0,0) , which means that φ∉ℎ() ( M): a contradiction. For the converse direction, let us assume towards a contradiction that M is not an equilibrium model of Γ . We assume without loss of generality that M is total but one of the following conditions fails. • ,(0,0)⊧̸Γ M,(0,0) . Assume that Γ≠∅ = so there exists φ∈Γ ∈ such that ,(0,0)⊧̸φ M,(0,0) . This means that φ∉ℎ() ( M). Since item 2) holds, Γ∪¬φ∣φ∉ℎ()⊧̸THTφ ∪\ ( M)\ _ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ . It follows that there exists ′=⟨(W,≼,S),V′⟩ M = (W, ,S),V such that ′,(0,0)⊧Γ∪¬φ∣φ∉ℎ() M ,(0,0) ∪\ ( M)\ but ′,(0,0)⊧̸φ M ,(0,0) . Since ′,(0,0)⊧Γ M ,(0,0) and φ∈Γ ∈ then ′,(0,0)⊧φ M ,(0,0) . Since, φ∉ℎ() ( M) then ′,(0,0)⊧¬φ M ,(0,0) . From the two previous points we conclude that ′,(0,0)⊧⊥ M ,(0,0) : a contradiction. • ,(0,0)⊧Γ M,(0,0) but there exists ′=⟨(W,≼,S),V′⟩ M = (W, ,S),V such that ′< M < M and ′,(0,0)⊧Γ M ,(0,0) . From ′< M < M follows that there exists i≥0i≥ 0 and ◦ip∈ℒt -0.5pt ^ip _t such that ′,(0,0)⊧̸◦ip M ,(0,0) -0.5pt ^ip, but ,(0,0)⊧◦ip M,(0,0) -0.5pt ^ip. Since ◦ip∈ℎ() -0.5pt ^ip ( M) then Γ∪¬φ∣φ∉ℎ()⊧THT◦ip ∪\ ( M)\ _ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ -0.5pt ^ip. It can be checked that ′,(0,0)⊧¬φ∣φ∉ℎ() M ,(0,0) \ ( M)\. Therefore, ′,(0,0)⊧◦ip M ,(0,0) -0.5pt ^ip, a contradiction. 5.1 Temporal safe beliefs For extending Definition 3.9 to the temporal case, we need some extra definitions. Since in the temporal case the truth of an atom may vary along time, we define the so-called set of temporal atoms associated with a signature ℙP (in symbols, ℙ◦P -0.5pt ) as ℙ◦:=◦ip∣p∈ℙ and i≥0.P -0.5pt :=\ -0.5pt ^ip p and i≥ 0\. Clearly, for any p∈ℙp , ◦0p:=p -0.5pt ^0p:=p, so ℙ⊆ℙ◦P -0.5pt . Definition 5.37 (ITLBDnITL BD_n-temporal safe belief). Let Γ be a temporal theory. The set T⊆ℙ◦T -0.5pt is said to be a ITLBDnITL BD_n-temporal safe belief set with respect to Γ if 1. Γ∪◦i¬p∣◦ip∈T∪◦i¬p∣◦ip∉T ∪\ -0.5pt ^i p -0.5pt ^ip∈ T\∪\ -0.5pt ^i p -0.5pt ^ip ∈ T\ is ITLBDnITL BD_n-consistent and 2. Γ∪◦i¬p∣◦ip∈T∪◦i¬p∣◦ip∉T⊧ITLBDnT ∪\ -0.5pt ^i p -0.5pt ^ip∈ T\∪\ -0.5pt ^i p -0.5pt ^ip ∈ T\ _ 0.0pt 10.35521pt3.0pt 0.0pt$ BD_n$ 0.0pt 11.1685pt3.0pt 0.0pt$ BD_n$ 0.0pt 12.67227pt3.0pt 0.0pt$ BD_n$ 0.0pt 10.83186pt3.0pt 0.0pt$ BD_n$T.∎ In the definition above, ITLBDnITL BD_n can be exchanged by any other proper intermediate temporal logic X. In the particular case of THT, we can prove a correspondence between THT-temporal safe beliefs and temporal equilibrium models. Definition 5.38. Given a total THT model =⟨(W,≼,S),V⟩ M= (W, ,S),V we define T:=◦ip∣p∈V((i,0)) and i≥0.T:=\ -0.5pt ^ip p∈ V((i,0)) and i≥ 0\. Clearly, T⊆ℙ◦T -0.5pt . Conversely, given T we retrieve =⟨(W,≼,S),V⟩ M= (W, ,S),V by setting V((i,0)),V((i,1)):=p∣◦ip∈T, for all i≥0.V((i,0)),V((i,1)):=\p -0.5pt ^ip∈ T\, for all i≥ 0. Proposition 5.39. For any temporal theory Γ , any total THT model =⟨(W,≼,S),V⟩ M= (W, ,S),V and set T⊆ℙ◦T -0.5pt related as described in Definition 5.38, the following items are equivalent: 1) M is a temporal equilibrium model of Γ 2) T is a THT-temporal safe belief of Γ Proof 5.40. To prove that 1) implies 2), let us assume that T is not a THT-temporal safe belief of Γ . Let us assume that Γ∪¬◦ip∣◦ip∈T∪¬◦ip∣◦ip∉T ∪\ -0.5pt ^ip -0.5pt ^ip∈ T\∪\ -0.5pt ^ip -0.5pt ^ip ∈ T\ is consistent but Γ∪¬◦ip∣◦ip∈T∪¬◦ip∣◦ip∉T⊧̸THTT. ∪\ -0.5pt ^ip -0.5pt ^ip∈ T\∪\ -0.5pt ^ip -0.5pt ^ip ∈ T\ _ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$T. This means that there exists a THT model ′=⟨(W,≼,S),V′⟩ M = (W, ,S),V such that ′,(0,0)⊧Γ M ,(0,0) , ′,(0,0)⊧¬◦ip∣◦ip∈T M ,(0,0) \ -0.5pt ^ip -0.5pt ^ip∈ T\, ′,(0,0)⊧¬◦ip∣◦ip∉T M ,(0,0) \ -0.5pt ^ip -0.5pt ^ip ∈ T\ but ′,(0,0)⊧̸T M ,(0,0) T. From ′,(0,0)⊧¬◦ip∣◦ip∈T M ,(0,0) \ -0.5pt ^ip -0.5pt ^ip∈ T\ and ′,(0,0)⊧¬◦ip∣◦ip∉T M ,(0,0) \ -0.5pt ^ip -0.5pt ^ip ∈ T\ we can conclude that V((i,1))=V′((i,1))V((i,1))=V ((i,1)), for all i≥0i≥ 0. From ′,(0,0)⊧̸T M ,(0,0) T it follows that ′,(0,0)⊧̸◦ip M ,(0,0) -0.5pt ^ip for some ◦ip∈T -0.5pt ^ip∈ T, with i≥0i≥ 0. This means that ′,(i,0)⊧̸p M ,(i,0) p. From ′,(0,0)⊧¬◦ip∣◦ip∈T M ,(0,0) \ -0.5pt ^ip -0.5pt ^ip∈ T\ we conclude that ′,(0,0)⊧¬◦ip M ,(0,0) -0.5pt ^ip, so ′,(i,1)⊧p M ,(i,1) p. Therefore, ′< M < M. Since ′,(0,0)⊧Γ M ,(0,0) , M is not an equilibrium model of Γ : a contradiction. Conversely, let us assume towards a contradiction that T is a THT-temporal safe belief of Γ but =⟨(W,≼,S),V⟩ M= (W, ,S),V is not a temporal equilibrium model of Γ . Assume, without loss a contradiction that M is total. Since T is a THT-temporal safe belief of Γ then Γ∪¬◦ip∣◦ip∈T∪¬◦ip∣◦ip∉T ∪\ -0.5pt ^ip -0.5pt ^ip∈ T\∪\ -0.5pt ^ip -0.5pt ^ip ∈ T\ is consistent. Let ′=⟨(W,≼,S),V′⟩ M = (W, ,S),V be such that ′,(0,0)⊧Γ∪¬◦ip∣◦ip∈T∪¬◦ip∣◦ip∉T M ,(0,0) ∪\ -0.5pt ^ip -0.5pt ^ip∈ T\∪\ -0.5pt ^ip -0.5pt ^ip ∈ T\. Since ′,(0,0)⊧¬◦ip∣◦ip∈T∪¬◦ip∣◦ip∉T M ,(0,0) \ -0.5pt ^ip -0.5pt ^ip∈ T\∪\ -0.5pt ^ip -0.5pt ^ip ∈ T\ then V′(i,1)=V(i,1)V (i,1)=V(i,1), for all i≥0i≥ 0. Since ′,(0,0)⊧Γ M ,(0,0) then ′,(0,1)⊧Γ M ,(0,1) . Since M is total and V′(i,1)=V(i,1)V (i,1)=V(i,1), for all i≥0i≥ 0 then ,(0,0)⊧Γ M,(0,0) . Since M is not an equilibrium model of Γ , there exists ′=⟨(W,≼,S),V′⟩ M = (W, ,S),V such that ′< M < M and ′,(0,0)⊧Γ M ,(0,0) . However, this contradicts Condition 2 of Definition 5.37. To conclude this section, we show that temporal safe belief sets are preserved when changing the underlying logic. In this case, we extend the results shown in Section 3. Lemma 5.41. Let us consider T⊆ℙ◦T -0.5pt and let X and Y be two proper intermediate temporal logics satisfying X⊆Y X Y. For any temporal theory Γ , if T is a X-temporal safe belief of Γ , then T is a Y-temporal safe belief of Γ . Proof 5.42. If T is a X-temporal safe belief of Γ , it follows that 1. Γ∪◦i¬p∣◦ip∈T∪◦i¬p∣◦ip∉T ∪\ -0.5pt ^i p -0.5pt ^ip∈ T\∪\ -0.5pt ^i p -0.5pt ^ip ∈ T\ is X-consistent and 2. Γ∪◦i¬p∣◦ip∈T∪◦i¬p∣◦ip∉T⊧XT ∪\ -0.5pt ^i p -0.5pt ^ip∈ T\∪\ -0.5pt ^i p -0.5pt ^ip ∈ T\ _ 0.0pt 3.83148pt3.0pt 0.0pt$ X$ 0.0pt 3.83148pt3.0pt 0.0pt$ X$ 0.0pt 3.2634pt3.0pt 0.0pt$ X$ 0.0pt 3.26338pt3.0pt 0.0pt$ X$T From the first item and Proposition 4.23 it follows that Γ∪◦i¬p∣◦ip∈T∪◦i¬p∣◦ip∉T ∪\ -0.5pt ^i p -0.5pt ^ip∈ T\∪\ -0.5pt ^i p -0.5pt ^ip ∈ T\ is Y-consistent. From the second item and Proposition 4.24 we conclude that Γ∪◦i¬p∣◦ip∈T∪◦i¬p∣◦ip∉T⊧YT. ∪\ -0.5pt ^i p -0.5pt ^ip∈ T\∪\ -0.5pt ^i p -0.5pt ^ip ∈ T\ _ 0.0pt 3.83148pt3.0pt 0.0pt$ Y$ 0.0pt 3.83148pt3.0pt 0.0pt$ Y$ 0.0pt 3.2634pt3.0pt 0.0pt$ Y$ 0.0pt 3.26338pt3.0pt 0.0pt$ Y$T. As a consequence, T is a Y-safe belief of Γ . We prove the converse of Lemma 5.41 below. Lemma 5.43. Let us consider T⊆ℙ◦T -0.5pt and let X and Y be two proper intermediate temporal logics satisfying X⊆Y X Y. For any temporal theory Γ , if T is a Y-temporal safe belief set of Γ , then T is a X-temporal safe belief set of Γ . Proof 5.44. Let us assume that T is a Y-temporal safe belief of Γ . It holds that (a) Γ∪◦i¬p∣◦ip∈T∪◦i¬p∣◦ip∉T ∪\ -0.5pt ^i p -0.5pt ^ip∈ T\∪\ -0.5pt ^i p -0.5pt ^ip ∈ T\ is Y-consistent and (b) Γ∪◦i¬p∣◦ip∈T∪◦i¬p∣◦ip∉T⊧YT ∪\ -0.5pt ^i p -0.5pt ^ip∈ T\∪\ -0.5pt ^i p -0.5pt ^ip ∈ T\ _ 0.0pt 3.83148pt3.0pt 0.0pt$ Y$ 0.0pt 3.83148pt3.0pt 0.0pt$ Y$ 0.0pt 3.2634pt3.0pt 0.0pt$ Y$ 0.0pt 3.26338pt3.0pt 0.0pt$ Y$T. From item (a) and Proposition 4.23 it follows that Γ∪◦i¬p∣p∈T∪◦i¬p∣p∉T ∪\ -0.5pt ^i p p∈ T\∪\ -0.5pt ^i p p ∈ T\ is both X-consistent and ITLBDnITL BD_n-consistent. From Y⊆THT Y $ THT$, the second item and Proposition 4.24 Γ∪◦i¬p∣◦ip∈T∪◦i¬p∣◦ip∉T⊧THTT. ∪\ -0.5pt ^i p -0.5pt ^ip∈ T\∪\ -0.5pt ^i p -0.5pt ^ip ∈ T\ _ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$T. (6) Let =⟨(W,≼,S),V⟩ M= (W, ,S),V be an ITLBDnITL BD_n model and w∈Ww∈ W satisfying (c) ,w⊧ITLBDnΓ M,w _ 0.0pt 10.35521pt3.0pt 0.0pt$ BD_n$ 0.0pt 11.1685pt3.0pt 0.0pt$ BD_n$ 0.0pt 12.67227pt3.0pt 0.0pt$ BD_n$ 0.0pt 10.83186pt3.0pt 0.0pt$ BD_n$ , (d) ,w⊧ITLBDn◦i¬p∣◦ip∈T M,w _ 0.0pt 10.35521pt3.0pt 0.0pt$ BD_n$ 0.0pt 11.1685pt3.0pt 0.0pt$ BD_n$ 0.0pt 12.67227pt3.0pt 0.0pt$ BD_n$ 0.0pt 10.83186pt3.0pt 0.0pt$ BD_n$\ -0.5pt ^i p -0.5pt ^ip∈ T\ and (e) ,w⊧ITLBDn◦i¬p∣◦ip∉T M,w _ 0.0pt 10.35521pt3.0pt 0.0pt$ BD_n$ 0.0pt 11.1685pt3.0pt 0.0pt$ BD_n$ 0.0pt 12.67227pt3.0pt 0.0pt$ BD_n$ 0.0pt 10.83186pt3.0pt 0.0pt$ BD_n$\ -0.5pt ^i p -0.5pt ^ip ∈ T\. From items (d) and (e) it follows that ,w⊧□(¬p∨¬p)∣p∈ℙ M,w \ ( p p) p \. In view of Lemma 4.27, there exists an ITLBDnITL BD_n model ′=⟨(W′,≼′,S′),V′⟩ M = (W , ,S ),V , w′∈W′w ∈ W and a bisimulation ⊆W×W′Z W× W such that, ww′wZw and for each i≥0i≥ 0, the intuitionistic subframe generated by S′⁣i(w′)S i(w ) contains an unique maximal point that we name ui′u _i. By Lemma 4.25, ′,w′⊧ITLBDnΓ M ,w _ 0.0pt 10.35521pt3.0pt 0.0pt$ BD_n$ 0.0pt 11.1685pt3.0pt 0.0pt$ BD_n$ 0.0pt 12.67227pt3.0pt 0.0pt$ BD_n$ 0.0pt 10.83186pt3.0pt 0.0pt$ BD_n$ , ′,w′⊧ITLBDn◦i¬p∣◦ip∈T M ,w _ 0.0pt 10.35521pt3.0pt 0.0pt$ BD_n$ 0.0pt 11.1685pt3.0pt 0.0pt$ BD_n$ 0.0pt 12.67227pt3.0pt 0.0pt$ BD_n$ 0.0pt 10.83186pt3.0pt 0.0pt$ BD_n$\ -0.5pt ^i p -0.5pt ^ip∈ T\ and ′,w′⊧ITLBDn◦i¬p∣◦ip∉T M ,w _ 0.0pt 10.35521pt3.0pt 0.0pt$ BD_n$ 0.0pt 11.1685pt3.0pt 0.0pt$ BD_n$ 0.0pt 12.67227pt3.0pt 0.0pt$ BD_n$ 0.0pt 10.83186pt3.0pt 0.0pt$ BD_n$\ -0.5pt ^i p -0.5pt ^ip ∈ T\. We prove the following claim: For all v′∈W′, if w′≼v′ then ′,v′⊧T. For all $v ∈ W $, if $w v $ then M ,v T. (7) The proof is done by induction in 0pt((W′,≼′),v′)0pt((W , ),v ). 1. If 0pt((W′,≼′),v′)=10pt((W , ),v )=1 then v′v is maximal, so v′=u0′v =u _0. By monotonicity, ′,u0′⊧◦i¬p∣◦ip∈T and i≥0∪◦i¬p∣◦ip∉T and i≥0. M ,u _0 \ -0.5pt ^i p -0.5pt ^ip∈ T and i≥ 0\∪\ -0.5pt ^i p -0.5pt ^ip ∈ T and i≥ 0\. Because of Proposition 4.18, Si(u0′)S^i(u _0) is ≼ -maximal, for all i≥0i≥ 0. Therefore, ′,S′⁣i(u0′)⊧p∣◦ip∈T∪¬p∣◦ip∉T, M ,S i(u _0) \p -0.5pt ^ip∈ T\∪\ p -0.5pt ^ip ∈ T\, for all i≥0i≥ 0. Hence, V′(S′⁣i(u0′))=p∣◦ip∈TV (S i(u _0))=\p -0.5pt ^ip∈ T\, for all i≥0i≥ 0 so ′,u0′⊧T M ,u _0 T. 2. For the inductive step, let us assume that 0pt((W,≼′),v′)=n+10pt((W, ),v )=n+1 and the claim holds for every x∈W′x∈ W satisfying v′≼xv x and 0pt((W,≼′),x)≤n0pt((W, ),x)≤ n (so v′≺xv x). By Proposition 4.22, 0pt((W,≼),S′⁣i(v′))≤n+10pt((W, ),S i(v ))≤ n+1, for all i≥0i≥ 0. By induction hypothesis, for all x∈≺′(v′)x∈ (v ), ′,x⊧T M ,x T. Moreover, by monotonicity, for all x∈≼′(v′)x∈ (v ) (including v′v itself), ′,x⊧◦i¬p∣◦ip∉T M ,x \ -0.5pt ^i p -0.5pt ^ip ∈ T\. By the semantics, for all i≥0i≥ 0 and for all y≼′(S′⁣i(v′))y (S i(v )), ′,y⊧¬p∣◦ip∉T M ,y \ p -0.5pt ^ip ∈ T\. By the semantics, for all i≥0i≥ 0 and for all y≺′(S′⁣i(v′))y (S i(v )), ′,y⊧p∣◦ip∈T M ,y \p -0.5pt ^ip∈ T\. From the two previous results, it follows that for all i≥0i≥ 0 and for all y∈≺′(S′⁣i(v′))y∈ (S i(v )), V′(y)=p∣◦ip∈TV (y)=\p -0.5pt ^ip∈ T\. Therefore, every point y∈≺′(S′⁣i(v′))y∈ (S i(v )) satisfies exactly the set p∣◦ip∈T\p -0.5pt ^ip∈ T\. By Lemma 4.29 there exists a THT model ′=⟨(ℕ×0,1,≼′,S′),V′⟩ M = (N×\0,1\, ,S ),V and a bisimulation ′⊆W′×(ℕ×0,1)Z W ×(N×\0,1\) such that v′′(0,0)v Z (0,0). Because of items (c)-(e), the monotonicity property and Lemma 4.25, ′,(0,0)⊧THTΓ∪◦i¬p∣◦ip∈T∪◦i¬p∣◦ip∉T. M ,(0,0) _ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ ∪\ -0.5pt ^i p -0.5pt ^ip∈ T\∪\ -0.5pt ^i p -0.5pt ^ip ∈ T\. Since ′ M is a THT model, ′,(0,0)⊧THTT M ,(0,0) _ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 11.2486pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$ 0.0pt 9.54628pt3.0pt 0.0pt$ THT$T because of (6). From v′′(0,0)v Z (0,0) and Lemma 4.25 it follows ′,v′⊧ITLBDnT M ,v _ 0.0pt 10.35521pt3.0pt 0.0pt$ BD_n$ 0.0pt 11.1685pt3.0pt 0.0pt$ BD_n$ 0.0pt 12.67227pt3.0pt 0.0pt$ BD_n$ 0.0pt 10.83186pt3.0pt 0.0pt$ BD_n$T. As a consequence, ′,w′⊧ITLBDnT M ,w _ 0.0pt 10.35521pt3.0pt 0.0pt$ BD_n$ 0.0pt 11.1685pt3.0pt 0.0pt$ BD_n$ 0.0pt 12.67227pt3.0pt 0.0pt$ BD_n$ 0.0pt 10.83186pt3.0pt 0.0pt$ BD_n$T. From ww′wZw and Lemma 4.25, ,w⊧ITLBDnT M,w _ 0.0pt 10.35521pt3.0pt 0.0pt$ BD_n$ 0.0pt 11.1685pt3.0pt 0.0pt$ BD_n$ 0.0pt 12.67227pt3.0pt 0.0pt$ BD_n$ 0.0pt 10.83186pt3.0pt 0.0pt$ BD_n$T. Since M was chosen arbitrary it follows that Γ∪◦i¬p∣◦ip∈T∪◦i¬p∣◦ip∉T⊧ITLBDnT, ∪\ -0.5pt ^i p -0.5pt ^ip∈ T\∪\ -0.5pt ^i p -0.5pt ^ip ∈ T\ _ 0.0pt 10.35521pt3.0pt 0.0pt$ BD_n$ 0.0pt 11.1685pt3.0pt 0.0pt$ BD_n$ 0.0pt 12.67227pt3.0pt 0.0pt$ BD_n$ 0.0pt 10.83186pt3.0pt 0.0pt$ BD_n$T, so T is a ITLBDnITL BD_n-safe belief of Γ . By Lemma 5.41 and the fact that ITLBDn⊆XITL BD_n X, Γ∪◦i¬p∣◦ip∈T∪◦i¬p∣◦ip∉T⊧XT. ∪\ -0.5pt ^i p -0.5pt ^ip∈ T\∪\ -0.5pt ^i p -0.5pt ^ip ∈ T\ _ 0.0pt 3.83148pt3.0pt 0.0pt$ X$ 0.0pt 3.83148pt3.0pt 0.0pt$ X$ 0.0pt 3.2634pt3.0pt 0.0pt$ X$ 0.0pt 3.26338pt3.0pt 0.0pt$ X$T. Lemmas 5.41 and 5.43 state that THT can be replaced by any proper intermediate temporal logic extending ITLBDnITL BD_n without affecting the resulting safe beliefs. Theorem 5.45. For any intermediate temporal logic X satisfying ITLBDn⊆X⊆THTITL BD_n X THT and for any theory Γ , the set of X-temporal safe beliefs of Γ coincide. 6 Conclusions In this paper, we revisited two well-known fixpoint characterizations of propositional equilibrium logic and answer sets. The first characterization, originally defined by Pearce (2006; 1999b) is based on the concept of theory completions, which has also been used in autoepistemic and default logic (Marek and Truszczyński 1993; Besnard 1989). We extended this characterization to the case of TEL. The second characterization, introduced by Osorio et al. (2005a) and known as safe belief sets, relates the equilibrium logic of arbitrary theories to syntactic entailment in intuitionistic logic.111111Similar results were also obtained by David Pearce for the case of disjunctive logic programs (Pearce 1999a). The authors proved that intuitionistic logic can be replaced by any proper intermediate logic without changing the set of safe beliefs. Their results rely on syntactic transformations that cannot be easily reproduced in the temporal case. Therefore, as a first contribution, we reformulated Osorio et al.’s approach in terms of semantic consequence in intuitionistic logic. We have identified a family of intuitionistic temporal logics, ITLBDnITL BD_n, for which we have defined a temporal extension of safe beliefs. We first show that any proper intermediate temporal logic extending ITLBDnITL BD_n can be used instead, without affecting the resulting set of temporal safe beliefs. Moreover, we show that in the case of THT, temporal safe beliefs correspond to temporal equilibrium models. We believe our results have fostered connections between temporal answer set programming and constructive modal logic, while also enhancing the visibility of THT within the field of constructive temporal logics. In future work, we plan to investigate intermediate logics not covered here, such as ITLeITL^e, ITLpITL^p, and real-valued Gödel temporal logics (Aguilera et al. 2025). Since consistency is not always preserved across these logics, it remains unclear whether the set of safe beliefs is preserved when using one of them as the monotonic basis for temporal equilibrium logic. Competing interests declaration. The authors declare none. References Abadi and Manna (1989) Martín Abadi and Zohar Manna. Temporal logic programming. Journal of Symbolic Computation, 8(3):277–295, 1989. ISSN 0747-7171. Aguado et al. (2013) F. Aguado, P. Cabalar, M. Diéguez, G. Pérez, and C. Vidal. Temporal equilibrium logic: a survey. Journal of Applied Non-Classical Logics, 23(1-2):2–24, 2013. 10.1080/11663081.2013.798985. Aguado et al. (2023) F. Aguado, P. Cabalar, M. Diéguez, G. Pérez, T. Schaub, A. Schuhmann, and C. Vidal. Linear-time temporal answer set programming. Theory and Practice of Logic Programming, 23(1):2–56, 2023. 10.1017/S1471068421000557. Aguilera et al. (2022) Juan P. Aguilera, Martín Diéguez, David Fernández-Duque, and Brett McLean. A gödel calculus for linear temporal logic. In Gabriele Kern-Isberner, Gerhard Lakemeyer, and Thomas Meyer, editors, Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning, KR 2022, Haifa, Israel, July 31 - August 5, 2022, 2022. Aguilera et al. (2025) Juan P. Aguilera, Martín Diéguez, David Fernández-Duque, and Brett McLean. Gödel-dummett linear temporal logic. Artif. Intell., 338:104236, 2025. Balbiani and Diéguez (2016) P. Balbiani and M. Diéguez. Temporal here and there. In L. Michael and A. Kakas, editors, Proceedings of the Fifteenth European Conference on Logics in Artificial Intelligence (JELIA’16), volume 10021 of Lecture Notes in Artificial Intelligence, pages 81–96. Springer-Verlag, 2016. Balbiani et al. (2020) Philippe Balbiani, Joseph Boudou, Martín Diéguez, and David Fernández-Duque. Intuitionistic linear temporal logics. ACM Transactions on Computational Logic, 21(2):14:1–14:32, 2020. Besnard (1989) P. Besnard. An Introduction to Default Logic. Symbolic Computation — Artifical Intelligence. Springer-Verlag, 1989. Boudou et al. (2017) Joseph Boudou, Martín Diéguez, and David Fernández-Duque. A decidable intuitionistic temporal logic. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden, volume 82 of LIPIcs, pages 14:1–14:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. 10.4230/LIPICS.CSL.2017.14. Boudou et al. (2019) Joseph Boudou, Martín Diéguez, David Fernández-Duque, and Fabián Romero. Axiomatic systems and topological semantics for intuitionistic temporal logic. In F. Calimeri, N. Leone, and M. Manna, editors, Proceedings of the Sixteenth European Conference on Logics in Artificial Intelligence (JELIA’19), volume 11468 of Lecture Notes in Computer Science, pages 763–777. Springer-Verlag, 2019. Cabalar et al. (2024) Pedro Cabalar, Martín Diéguez, François Laferrière, Torsten Schaub, and Igor Stéphan. A fixpoint characterisation of temporal equilibrium logic. In Carmine Dodaro, Gopal Gupta, and Maria Vanina Martinez, editors, Logic Programming and Nonmonotonic Reasoning - 17th International Conference, LPNMR 2024, Dallas, TX, USA, October 11-14, 2024, Proceedings, volume 15245 of Lecture Notes in Computer Science, pages 304–316. Springer, 2024. 10.1007/978-3-031-74209-5_23. Chagrov and Zakharyaschev (1997) Alexander V. Chagrov and Michael Zakharyaschev. Modal Logic, volume 35 of Oxford logic guides. Oxford University Press, 1997. ISBN 978-0-19-853779-3. Diéguez and Fernández-Duque (2018) Martín Diéguez and David Fernández-Duque. An intuitionistic axiomatization of ’eventually’. In Guram Bezhanishvili, Giovanna D’Agostino, George Metcalfe, and Thomas Studer, editors, Advances in Modal Logic 12, proceedings of the 12th conference on ”Advances in Modal Logic,” held in Bern, Switzerland, August 27-31, 2018, pages 199–218. College Publications, 2018. Eiter and Šimkus (2009) T. Eiter and M. Šimkus. Bidirectional answer set programs with function symbols. In C. Boutilier, editor, Proceedings of the Twenty-first International Joint Conference on Artificial Intelligence (IJCAI’09), pages 765–771. AAAI/MIT Press, 2009. Fernández-Duque et al. (2024) David Fernández-Duque, Brett McLean, and Lukas Zenger. A sound and complete axiomatisation for intuitionistic linear temporal logic. In P. Marquis, M. Ortiz, and M. Pagnucco, editors, Proceedings of the Twenty-first International Conference on Principles of Knowledge Representation and Reasoning (KR’24), pages 350–360, 2024. 10.24963/KR.2024. Gabbay (1981) Dov M. Gabbay. Semantical Investigations in Heyting’s Intuitionistic Logic. Reidel, Dordrecht, Netherland, 1981. Gelfond and Lifschitz (1988) M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In R. Kowalski and K. Bowen, editors, Proceedings of the Fifth International Conference and Symposium of Logic Programming (ICLP’88), pages 1070–1080. MIT Press, 1988. 10.1201/b10397-6. Gelfond and Lifschitz (1993) M. Gelfond and V. Lifschitz. Representing action and change by logic programs. Journal of Logic Programming, 17(2-4):301–321, 1993. Giordano et al. (2013) L. Giordano, A. Martelli, and D. Theseider Dupré. Reasoning about actions with temporal answer sets. Theory and Practice of Logic Programming, 13(2):201–225, 2013. Gödel (1932) K. Gödel. Zum intuitionistischen Aussagenkalkül. Anzeiger der Akademie der Wissenschaften in Wien, pages 65–66, 1932. Harel et al. (2000) D. Harel, J. Tiuryn, and D. Kozen. Dynamic Logic. MIT Press, 2000. 10.1145/568438.568456. Heyting (1930) A. Heyting. Die formalen Regeln der intuitionistischen Logik. In Sitzungsberichte der Preussischen Akademie der Wissenschaften, pages 42–56. Deutsche Akademie der Wissenschaften zu Berlin, 1930. Hosoi (1966) T. Hosoi. The Axiomatization of the Intermediate Propositional Systems S2S_2 of Gödel. Journal of the Faculty of Science of the University of Tokyo, 13(2):183–187, 1966. Jankov (1968) V A Jankov. The calculus of the weak ”law of excluded middle”. Mathematics of the USSR-Izvestiya, 2(5):997, oct 1968. 10.1070/IM1968v002n05ABEH000690. Lifschitz (2010) V. Lifschitz. Thirteen definitions of a stable model. In A. Blass, N. Dershowitz, and W. Reisig, editors, Fields of Logic and Computation, Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, volume 6300 of Lecture Notes in Computer Science, pages 488–503. Springer-Verlag, 2010. 10.1007/978-3-642-15025-8_24. Lifschitz (2019) V. Lifschitz. Answer Set Programming. Springer-Verlag, 2019. 10.1007/978-3-030-24658-7. Marek and Truszczyński (1993) V. Marek and M. Truszczyński. Nonmonotonic logic: context-dependent reasoning. Artifical Intelligence. Springer-Verlag, 1993. Mints (2000) G. Mints. A Short Introduction to Intuitionistic Logic. Kluwer Academic / Plenum Publishers, 2000. Osorio et al. (2005a) M. Osorio, J. Navarro Pérez, and J. Arrazola. Safe beliefs for propositional theories. Annals of Pure and Applied Logic, 134(1):63–82, 2005a. 10.1016/J.APAL.2004.06.012. Osorio et al. (2005b) Mauricio Osorio, Juan Antonio Navarro Pérez, and José Arrazola. Safe beliefs for propositional theories. Annals of Pure and Applied Logic, 134(1):63–82, 2005b. Patterson (1997) A. Patterson. Bisimulation and propositional intuitionistic logic. In A. Mazurkiewicz and J. Winkowski, editors, Proceedings of the Eighth International Conference on Concurrency Theory (CONCUR’97), volume 1243 of Lecture Notes in Computer Science, pages 347–360. Springer-Verlag, 1997. Pearce (1997) D. Pearce. A new logical characterisation of stable models and answer sets. In J. Dix, L. Pereira, and T. Przymusinski, editors, Proceedings of the Sixth International Workshop on Non-Monotonic Extensions of Logic Programming (NMELP’96), volume 1216 of Lecture Notes in Computer Science, pages 57–70. Springer-Verlag, 1997. 10.1007/BFb0023801. Pearce (1999a) D. Pearce. Stable inference as intuitionistic validity. Journal of Logic Programming, 38(1):79–91, 1999a. Pearce (1999b) D. Pearce. From here to there: stable negation in logic programming. In D. Gabbay and H. Wansing, editors, What is negation?, pages 161–181. Kluwer Academic Publishers, 1999b. Pearce (2006) D. Pearce. Equilibrium logic. Annals of Mathematics and Artificial Intelligence, 47(1-2):3–41, 2006. 10.1007/s10472-006-9028-z. Pnueli (1977) A. Pnueli. The temporal logic of programs. In Proceedings of the Eight-teenth Symposium on Foundations of Computer Science (FOCS’77), pages 46–57. IEEE Computer Society Press, 1977. 10.1109/SFCS.1977.32. Rauszer (1974) Cecylia Rauszer. A formalization of the propositional calculus of h-b logic. Studia Logica, 33(1):23–34, 1974. 10.1007/bf02120864. Smetanich (1960) Ya. S. Smetanich. On the completeness of the propositional calculus with additional operations in one argument. Trudy Moskovskogo Matematicheskogo Obshchestva, 9:357–371, 1960. (in russian). van Dalen (1989) Dirk van Dalen. Logic and structure (2. ed.). Universitext. Springer, 1989. Appendix A Proofs Proof of Proposition 1. Assume towards a contradiction that Γ⊧̸X′φ _ 0.0pt 4.05066pt3.0pt 0.0pt$ X $ 0.0pt 4.05066pt3.0pt 0.0pt$ X $ 0.0pt 4.60304pt3.0pt 0.0pt$ X $ 0.0pt 5.12718pt3.0pt 0.0pt$ X $ . This means that there exists a model =⟨(W,≼),V⟩ M= (W, ),V and w∈Ww∈ W such that ,w⊧X′Γ M,w _ 0.0pt 4.05066pt3.0pt 0.0pt$ X $ 0.0pt 4.05066pt3.0pt 0.0pt$ X $ 0.0pt 4.60304pt3.0pt 0.0pt$ X $ 0.0pt 5.12718pt3.0pt 0.0pt$ X $ and ,w⊧̸X′φ M,w _ 0.0pt 4.05066pt3.0pt 0.0pt$ X $ 0.0pt 4.05066pt3.0pt 0.0pt$ X $ 0.0pt 4.60304pt3.0pt 0.0pt$ X $ 0.0pt 5.12718pt3.0pt 0.0pt$ X $ . Since X⊆X′ X X , M can be reconsidered within the logic X, meaning that ,w⊧XΓ M,w _ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ and ,w⊧̸Xφ M,w _ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ : a contradiction. Proof of Proposition 2. Let =⟨(W,≼),V⟩ M= (W, ),V be an intuitionistic model and let w∈Ww∈ W be such that ,w⊧¬p∨¬p∣p∈ℙ M,w \ p p p \. It follows that all maximal ≼ -worlds in the subframe generated by x satisfy the same propositional variables. Let us assume towards a contradiction that ,w⊧¬p∨¬p∣p∈ℙ M,w \ p p p \ but there exist two maximal worlds u and u′u in W such that w≼uw u, w≼u′w u but V(u)≠V(u′)V(u) =V(u ). Let us assume, without loss of generality, that V(u)⊈V(u′)V(u) V(u ). Therefore, there exists p∈ℙp such that p∈V(u)p∈ V(u) but p∉V(u′)p ∈ V(u ). Since u is a maximal world, it is classical, so ,u⊧p∨¬p M,u p p, so ,u⊧̸¬p M,u p. By monotonicity, ,w⊧̸¬p M,w p. Since ,w⊧¬p∨¬p M,w p p, ,w⊧¬p M,w p. By monotonicity, ,u′⊧¬p M,u p. Since u′u is also classical, it follows that ,u′⊧p M,u p: a contradiction. Proof of Lemma 3.11. If T is a X-safe belief of Γ , it follows that 1. Γ∪¬p∣p∈T∪¬p∣p∉T ∪\ p p∈ T\∪\ p p ∈ T\ is X-consistent and 2. Γ∪¬p∣p∈T∪¬p∣p∉T⊧XT ∪\ p p∈ T\∪\ p p ∈ T\ _ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$T From the first item and Proposition 1, it follows that Γ∪¬p∣p∈T∪¬p∣p∉T ∪\ p p∈ T\∪\ p p ∈ T\ is Y-consistent. From the second item and Proposition 1, we conclude that Γ∪¬p∣p∈T∪¬p∣p∉T⊧YT. ∪\ p p∈ T\∪\ p p ∈ T\ _ 0.0pt 3.7021pt3.0pt 0.0pt$ Y$ 0.0pt 3.7021pt3.0pt 0.0pt$ Y$ 0.0pt 3.2927pt3.0pt 0.0pt$ Y$ 0.0pt 3.2927pt3.0pt 0.0pt$ Y$T. Proof of Proposition 4.18. Assume towards a contradiction that S(w)S(w) is not maximal w.r.t. ≼ . Therefore there exists v∈Wv∈ W such that S(w)≺vS(w) v. By the backward confluence property there exists u∈Wu∈ W such that w≼uw u and S(u)=vS(u)=v. Since w is maximal w.r.t. ≼ then w=uw=u. this would imply that S is not a function: a contradiction. Proof of Lemma 4.19. From right to left, in view of Observation 1, LTL models are an specific case of ITLBDnITL BD_n models so if Γ is LTL-consistent then it is ITLBDnITL BD_n-consistent. From left to right, if Γ is ITLBDnITL BD_n consistent then there exists ITLBDnITL BD_n model =⟨(W,≼,S),V⟩ M= (W, ,S),V and w∈Ww∈ W such that ,w⊧ΓM,w . Since M is of finite depth, then there exists a maximal Kripke world v∈Wv∈ W such that w≼vw v and ,v⊧ΓM,v . Since w≼vw v then S(w)≼S(v)S(w) S(v) because of the forward confluence property. Moreover, in view of Proposition 4.18, S(v)S(v) is also a maximal point. Let us define ′=⟨(W′,≼′,S′),V′⟩ M = (W , ,S ),V where W′=Sn(v)∣n≥0W =\S^n(v) n≥ 0\, ≼′=(x,x)∣x∈W′ =\(x,x) x∈ W \ and S′(x)=S(x)S (x)=S(x), for all x∈W′x∈ W . Clearly, ′ M is an LTL satisfying Γ at v∈W′v∈ W . Proof of Lemma 4.21. The right to left direction follows Observation 1 as in the proof of Lemma 4.19. For the left to right direction, note that, since X is an intermediate logic,, any model in the logic X is also a ITLBDnITL BD_n model. By Lemma 4.19, if Γ X-consistent then Γ is ITLBDnITL BD_n-consistent and, because of Lemma 4.19, Γ is LTL-consistent. Proof of Proposition 4.22. Assume towards a contradiction that 0pt((W,≼),S(w))>n0pt((W, ),S(w))>n. Assume without loss of generality that 0pt((W,≼),S(w))=n+10pt((W, ),S(w))=n+1. By definition, there exists w0′,w1′,⋯,wn+1′w _0,w _1,·s,w _n+1 such that S(w)=w0′S(w)=w _0 and wi′≺wi+1′w _i w _i+1121212We consider ≺ because all those wi′w _i must be different., for all i∈[0..n)i∈[0..n). From S(w)=w0′≺w1′S(w)=w _0 w _1 and the backward confluence property it follows that there exists w1∈Ww_1∈ W such that w≼w1w w_1 and S(w1)=w1′S(w_1)=w _1. From S(w1)=w1′≺w2′S(w_1)=w _1 w _2 and the backward confluence property, it follows that there exists w2∈Ww_2∈ W such that w1≺w2w_1 w_2 and S(w2)=w2′S(w_2)=w _2. By continuously applying the same reasoning we would conclude that, since S(wn)=wn′≺wn+1′S(w_n)=w _n w _n+1, there exists wn+1∈Ww_n+1∈ W such that wn≺wn+1w_n w_n+1 and S(wn+1)=wn+1′S(w_n+1)=w _n+1. Therefore, there exists a sequence w0,w1,⋯,wn+1w_0,w_1,·s,w_n+1 with w=w0w=w_0 and for all i≥0i≥ 0, S(wi)=wi′S(w_i)=w _i. Since 0pt((W,≼),w)≤n0pt((W, ),w)≤ n, wj=wkw_j=w_k for some i,k∈[0..n+1]i,k∈[0..n+1]. Since S is a function, it would mean that S(wj)=wj′S(w_j)=w _j and S(wj)=wk′S(w_j)=w _k, so wj′=wk′w _j=w _k: a contradiction. Proof of Proposition 4.23. We use Corollary 4.21 to conclude that Γ is X-consistent iff Γ is LTL-consistent iff Γ is Y-consistent. Proof of Proposition 4.24. Assume towards a contradiction that Γ⊧̸yΔ _ -0.93333pt 2.88098pt3.0pt 1.3611pt$ y$ -0.93333pt 2.88098pt3.0pt 1.3611pt$ y$ -0.93333pt 2.53336pt3.0pt 0.95277pt$ y$ -0.93332pt 2.53336pt3.0pt 0.68054pt$ y$ . Therefore, there exists =⟨(W,≼,S),V⟩ M= (W, ,S),V and w∈Ww∈ W such that ,w⊧YΓ M,w _ 0.0pt 3.7021pt3.0pt 0.0pt$ Y$ 0.0pt 3.7021pt3.0pt 0.0pt$ Y$ 0.0pt 3.2927pt3.0pt 0.0pt$ Y$ 0.0pt 3.2927pt3.0pt 0.0pt$ Y$ and ,w⊧̸YΔ M,w _ 0.0pt 3.7021pt3.0pt 0.0pt$ Y$ 0.0pt 3.7021pt3.0pt 0.0pt$ Y$ 0.0pt 3.2927pt3.0pt 0.0pt$ Y$ 0.0pt 3.2927pt3.0pt 0.0pt$ Y$ . Since X⊆Y X Y, X is weaker than Y. Therefore, M is also a model within the logic X. Therefore, ,w⊧XΓ M,w _ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ and ,w⊧̸XΔ M,w _ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ , meaning that Γ⊧̸XΔ _ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.7021pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ 0.0pt 3.2927pt3.0pt 0.0pt$ X$ : a contradiction. Proof of Theorem 5.45. Directly from lemmas 5.41 and 5.43.

Instant research discovery