Ill-Founded Proof Systems for Intuitionistic Linear-Time Temporal Logic

Intuitionistic modal and temporal logics have found tangible applications in computer science [7, 9, 12, 13, 16, 22] and with that comes the motivation for developing succinct proof systems that facilitate establishing fundamental properties such as decidability and algorithmic proof search. Temporal logic describes a range of modal logics in which modal and ‘fixed point’ operators are interpreted as temporal relations. An important example is linear-time temporal logic \(\textsf{LTL}\), whose temporal operators include a ‘next’ operator \(\textsf{X}\) and an ‘until’ operator \(\mathbin {\textsf{U}}\). The formula \(\textsf{X} A\) is interpreted as ‘A is true in the next time-step’, and \(A\mathbin {\textsf{U}}B\) as ‘A is true until B is true’. The until operator satisfies the equivalence

showing that \(A\mathbin {\textsf{U}}B\) is a fixed point of the propositional function \( p \mapsto B\vee (A\wedge \textsf{X}p )\).

Advances in the proof theory of temporal logics evidence that ill-founded calculi are particularly suitable for capturing the behaviour of fixed point operators in a syntactic way [1, 8, 10, 15]. So far, the study of such proof systems has focused on classical logic and their applicability to intuitionistic temporal logics remains largely unexplored. One of the obstacles in directly applying the techniques from the classical setting is the interaction of the temporal and intuitionistic relation in the intuitionistic Kripke semantics.

A standard way to present the semantics of intuitionistic propositional logic is in terms of Kripke models \((W,\le , V)\), where \(\le \) is a partial order on the set of worlds W and V a valuation that is monotone in \(\le \). A key property of this semantics is the monotonicity lemma: for all \( v, v' \in W\), if \( v \le v' \) and \( v \models A\) then \( v'\models A\). The semantics of intuitionistic modal/temporal logics can be given in terms of intuitionistic Kripke models \((W,\le , V)\) equipped with an additional relation R on W used to interpret the modal operators. In order to keep the monotonicity property, modalities are interpreted as follows.

One can also use the classical truth conditions for modalities and instead impose confluence properties on R and \(\le \) to ensure monotonicity. Two confluence properties considered in the literature are:

Forward confluence:

if \(v\ge w \) and \( wRw'\) then there exists \(v'\ge w'\) with \(vRv'\).

Backward confluence:

if \(w R w' \) and \( w' \le v'\) then there exists \(v\ge w\) with \(vRv'\).

In the setting of intuitionistic \(\textsf{LTL}\), forward confluence alone suffices to obtain the monotonicity lemma [3]. Since Simpson [20] argues that an intuitionistic reading of possible world semantics results in models that also satisfy backward confluence, intuitionistic modal logic is generally used to refer to the logic obtained when adopting both conditions. Nevertheless, logics corresponding to weaker frame conditions, often called constructive modal logics, have also received considerable interest (see e.g. [2, 23]).

In this work, the language of linear temporal logic is interpreted over models satisfying forward confluence and models satisfying both forward and backward confluence; following the terminology in [3], they are referred to as expanding and persistent models, respectively. To date, neither logic has been given a sound and complete axiomatisation.^{Footnote 1} For each of the resulting logics, we present a cut-free, ill-founded sequent calculus. Both calculi employ a simple form of nested sequents so that formulas can be operated on at different temporal steps. This form of nesting has been used by Kojima and Igarashi [14] to obtain a finitary calculus for a constructive interpretation of \(\textsf{LTL}\) without the until operator.

A standard technique for showing completeness of an ill-founded calculus is to set up a proof search game between two players, Prover and Refuter, such that a winning strategy for Prover corresponds to a proof and a winning strategy for Refuter to a countermodel (see e.g. [1, 19]). When applying this technique to the intuitionistic case, one needs to ensure that the constructed ‘countermodel’ satisfies the required frame conditions. We present such a proof search game for both logics. The use of nested sequents is crucial for the game as it enables postponing the application of non-invertible rules until all relevant information about future time steps is determined.

Intuitionistic temporal logics have been studied in different contexts, the most notable of which are metaprogramming and topological dynamics. The former involves the addition of temporal operators to \(\lambda \)-calculi with the aim of modelling aspects of metaprogramming such as staged computation (see e.g. [7, 21, 24]). The latter concerns the use of intuitionistic temporal logics to reason about dynamical topological systems. Fernández-Duque [11] introduced the logic \(\mathsf {ITL^c}\), in which formulas of \(\textsf{LTL}\) are interpreted in general topological models, and showed that its restriction to the ‘eventually’ operator \(\Diamond \) is decidable.^{Footnote 2} Boudou et al. [4] show the decidability of the same fragment interpreted in expanding models, denoted by \(\mathsf {ITL^e}\), and provide a Hilbert-style axiomatisation for both logics in [5]. A calculus with \(\omega \)-branching inference rules is given in [6] for \(\mathsf {ITL^e}\) extended with the ‘henceforth’ operator. To date, no recursive axiomatisation of the validities in persistent models is known.

Outline. Section 2 introduces the syntax and semantics of intuitionistic linear temporal logic \(\textsf{iLTL}\). Section 3 presents the proof system \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\), which is proven sound and complete with respect to expanding models in Sects. 4 and 5. In Sect. 6, we outline how \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) can be adapted to obtain a system \(\textsf{iLTL}{_\textsf{p}}^{\textsf{nest}}\) that is sound and complete with respect to persistent models.

Fix a countable set \(\textsf{Prop}\) of atomic propositions. Formulas of \(\textsf{iLTL}\) are defined inductively as follows:

where \(p \in \textsf{Prop}\). We denote formulas by A, B,  etc., and atomic propositions by p, q,  etc. We define the formula \(X^n A\) inductively by \(X^0 A := A\) and \(X^{n+1}A := X X^n A\).

Formulas of \(\textsf{iLTL}\) are evaluated on dynamic models, which are intuitionistic Kripke models equipped with a time function that maps each world to its temporal successor.

Definition 1

A dynamic model is a tuple \(M = (W, \le , f, V)\) where

1. 1.

   W is a non-empty set,

2. 2.

   \(\le \) is a partial order on W,

3. 3.

   \(f :W \longrightarrow W\) is a function and

4. 4.

   \(V :W \longrightarrow \mathcal {P}(Prop)\) is a valuation function that is monotone in \(\le \), i.e., for all \(w,v \in W\), if \(w \le v\), then \(V(w) \subseteq V(v)\).

Elements of W are called worlds. If \(w,v \in W\) such that \(f(w) = v\), then v is called the temporal successor of w. If \(w \le v\), then v is called an intuitionistic successor of w. We inductively define \(f^0(w) {:}{=}w\) and \(f^{n+1}(w) {:}{=}f(f^n(w))\).

Given a dynamic model \(M=(W, \le , V, f)\), the truth relation \(M,w \models A\) where \(w \in W\) is defined inductively on A as follows.

Validity and satisfiability over a class of dynamic models are defined in the standard way.

We consider dynamic models that satisfy certain confluence properties, namely forward and backward confluence, which are illustrated in Fig. 1.

Definition 2

A dynamic model \(M=(W, \le , f, V)\) is

• expanding if M is forward confluent: for all \(w,v \in W\),

  $$\begin{aligned} \text {if } w \le v, \text { then } f(w) \le f(v), \end{aligned}$$

• persistent if M is expanding and backward confluent: for all \(w,v' \in W\), if \(v'\ge f(w)\), then there exists \(v \ge w\) with \(f(v) = v'\).

We denote by \(\textsf{iLTL}_\textsf{e}\) and \(\textsf{iLTL}_\textsf{p}\) the set of \(\textsf{iLTL}\)-validities over expanding and persistent models, respectively. It is easy to check that the temporal version of the \(\textbf{K}\)-axiom, namely \(\textsf{X}(A \rightarrow B) \rightarrow (\textsf{X}A \rightarrow \textsf{X}B)\), is valid over expanding models. The converse \((\textsf{X}A \rightarrow \textsf{X}B) \rightarrow \textsf{X}(A \rightarrow B)\) is only valid over persistent models, and so we have \(\textsf{iLTL}_\textsf{e}\subsetneq \textsf{iLTL}_\textsf{p}\).

Forward and backward confluence.

Full size image

With a straightforward induction, one can prove the monotonicity lemma for expanding models. Note that the lemma thus also holds for persistent models.

Lemma 1

Let \(M=(W, \le , V, f)\) be an expanding model, \(w,v \in W\) and A a formula. If \(M,w \models A\) and \(w \le v\), then \(M,v \models A\).

In this section we present an ill-founded sequent calculus that is sound and complete with respect to the class of expanding models. Proofs in this calculus are finitely-branching trees that admit infinitely long branches. Importantly, the calculus has no explicit induction rule and does not make use of the cut-rule.

To ensure soundness, infinite branches are required to satisfy a global soundness condition, which is presented in a standard way using formula traces. To ensure completeness, the calculus incorporates a simple form of nesting.

Definition 3

A nested \(\textsf{iLTL}\)-formula is a tuple (A, n), denoted by \(A^n\), with A an \(\textsf{iLTL}\)-formula and \(n< \omega \). A sequent is an ordered pair \(\langle \varGamma , \varDelta \rangle \), written as \(\varGamma \Rightarrow \varDelta \), where \(\varGamma \) and \(\varDelta \) are finite sets of nested formulas.

For the remainder of this paper we call nested formulas simply formulas. Formulas that are not nested are called plain. Observe that sequents \(\varGamma \Rightarrow \varDelta \) may contain multiple formulas in \(\varDelta \), i.e. we consider a multi-succedent calculus. The intended interpretation of a nested formula \(A^n\) is the plain formula \(\textsf{X}^n A\). The interpretation of a sequent \( A_1^{m_1} , \dotsc , A_k^{m_k} \Rightarrow B^{n_1}_1 , \dotsc , B^{n_l}_l \) is the plain formula

We write \(M,w \models A^n\) if \(M,w \models \textsf{X}^n A\) and \(M,w\models \varGamma \Rightarrow \varDelta \) if M, w satisfies the interpretation of \(\varGamma \Rightarrow \varDelta \). For any set \(\varGamma \) of nested formulas, we define \(\varGamma ^{+1} = \{A^{n+1}: A^n\in \varGamma \}\).

Definition 4

The sequent calculus \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) consists of the rules in Fig. 2. Rules without premises are called axioms.

Rules of the system \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\). The symbols \(\varGamma , \varDelta , \varSigma \) and \(\Pi \) range over arbitrary finite sets of nested formulas which may be empty.

Full size image

The propositional rules of \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) are based on the multi-succedent calculus \(\textbf{G3im}\) from Negri and von Plato [18] and the nesting is inspired by the work of Kojima and Igarashi [14]. The rule \({\rightarrow }\textrm{L}\) differs from the presentation in Negri and von Plato insofar that there is no weakening in the left premise, resulting in invertibility of \({\rightarrow }\textrm{L}\). The choice to use a multi-succedent instead of a single-succedent calculus is motivated by the former’s better compatibility with proof search. Observe that the rule \({\rightarrow } \textrm{R}\) has only a single formula in the succedent of the premise, ensuring that the law of excluded middle is not derivable. Moreover, \({\rightarrow }\textrm{R}\) can only be applied to implications with nesting level 0. Relaxing this restriction by allowing implications of arbitrary nesting depth is unsound for expanding models but sound and complete for persistent models (see Sect. 6).

The \(\mathbin {\textsf{U}}\)-rules capture the equivalence \({A\mathbin {\textsf{U}}B\equiv B\vee (A\wedge \textsf{X}(A\mathbin {\textsf{U}}B))}\) and the ‘shift’ rule \(\textrm{S}\) captures modal necessitation. The rules \(\textsf{X}\textsf{L}\) and \(\textsf{X}\textsf{R}\) are purely structural as \(\textsf{X}A^n\) has the same interpretation as \(A^{n+1}\). Moreover, note that all rules except \(\textrm{S}\) and \({\rightarrow }\textrm{R}\) are invertible in the sense that the conclusion is valid if and only if the premises are.^{Footnote 3} We will therefore refer to \(\textrm{S}\) and \({\rightarrow }\textrm{R}\) as the non-invertible rules and to all other rules as the invertible rules.

It will be helpful to refer to formulas according to their role in a particular rule application. For each rule, the distinguished formula in the conclusion is called principal and the distinguished formulas in the premises are called its residuals; for example, in \({\rightarrow }\textrm{L}\) the principal formula is \(A\rightarrow B^n\) and its residuals are \(A\rightarrow B^n\), \(A^n\) and \(B^n\). In \(\textrm{S}\), all formulas in the conclusion are principal and each formula in the premise is the residual of its corresponding principal formula; in particular, formulas in \(\varSigma \) and \(\Pi \) have no residual. In every rule application, any formula that is neither principal nor residual is called a side formula.

A derivation in \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) of a sequent \(\sigma \) is a finite or infinite tree whose nodes are labelled according to the rules of \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) and whose root is labelled by \(\sigma \). We will read trees ‘upwards’, so the nodes labelled by premises are viewed as successors of the node labelled by the conclusion. A path through such a derivation T is a finite or infinite sequence \(\rho _0,\rho _1, \ldots \) of nodes of T such that for each index i, \(\rho _{i+1}\) is a direct successor of \(\rho _{i}\) in T.

Definition 5

Let \(\rho \) be a path through a derivation T. A (formula) trace on \(\rho \) is a finite or infinite sequence of nested formulas \(A_0, A_1,\dots \) such that for each index i the following hold.

1. 1.

   \(A_i\) occurs on the left-hand side of the sequent labelling \(\rho _i\);

2. 2.

   if \(A_{i}\) is a principal formula in the rule applied at \(\rho _i\), then \(A_{i+1}\) is a residual formula of \(A_i\) in \(\rho _{i+1}\);

3. 3.

   if \(A_{i}\) is a side formula in the rule applied at \(\rho _i\), then \(A_{i+1}=A_{i}\).

For any rule R, we say that a trace \((A_i)_{i}\) actively passes through R if there is an index j such that \(A_j\) is a principal formula in an application of R.

Definition 6

A formula trace is good if it actively passes through infinitely many applications of the rule \(\mathbin {\textsf{U}}\textrm{L}\).

The following lemma describes a straightforward yet key property of good formula traces.

Lemma 2

If \((A_i)_i\) is a good formula trace, then there is a plain formula of the form \( A\mathbin {\textsf{U}}B\) and some \(j<\omega \) such that for all \(k\ge j\), \(A_k\) is of the form \(A\mathbin {\textsf{U}}B^{m_k}\) or \(\textsf{X}(A\mathbin {\textsf{U}}B)^{m_k}\) for \(m_k<\omega \).

A proof in \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) is defined as follows.

Definition 7

An \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\)-derivation T of a sequent \(\sigma \) is a proof of \(\sigma \) if

1. 1.

   every leaf in T is labelled by an axiom;

2. 2.

   every infinite branch of T contains an infinite path that has a good formula trace.

This section establishes soundness of \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) with respect to the class of expanding models. The proof proceeds via a standard argument using signatures: maps that associate a natural number to each ‘relevant’ formula in a sequent \(\sigma \). We assume towards a contradiction that there is a proof \(\pi \) of an invalid sequent \(\sigma \). Then, using a countermodel of \(\sigma \), we find an infinite path \(\rho \) of invalid sequents in \(\pi \) and assign a signature to each of them. By ensuring that these signatures never increase and decrease when passing through the \(\mathbin {\textsf{U}}\textrm{L}\)-rule, it then follows that a good formula trace on \(\rho \) corresponds to an infinite descent of natural numbers. The aforementioned ‘relevant’ formulas are called eventualities.

For a sequent \(\sigma \), let \(\varGamma _\sigma \) and \(\varDelta _\sigma \) denote, respectively, the left-hand and right-hand side of \(\sigma \).

Definition 8

An eventuality is a formula of the form \(\textsf{X}^j (A\mathbin {\textsf{U}}B)^n\) with \(n,j < \omega \). Given a sequent \(\sigma \), a formula E is an eventuality of \(\sigma \) if E is an eventuality occurring in \(\varGamma _\sigma \).

Let \(\mathbin {\textsf{U}}^k\) be the operator defined inductively by \(A\mathbin {\textsf{U}}^0 B=B\) and \(A\mathbin {\textsf{U}}^{k+1}\! B=A\wedge \textsf{X}(A\mathbin {\textsf{U}}^{k}\! B)\). For an eventuality \(E=\textsf{X}^j (A\mathbin {\textsf{U}}B)^n\) and \(k<\omega \) define

Given a sequent \(\sigma \), a signature for \(\sigma \) is a map \(\tau \) which assigns a natural number to each eventuality of \(\sigma \). By \(\varGamma _\sigma [\tau ]\) we denote the set obtained from \(\varGamma _\sigma \) by replacing each eventuality E with \(E[\tau (E)]\). Furthermore, we let \(\sigma [\tau ]\) denote the sequent \(\varGamma _\sigma [\tau ]\Rightarrow \varDelta _\sigma \).

Theorem 1

Every sequent provable in \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) is valid over the class of expanding models.

Proof

Let \(\pi \) be a \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\)-proof of \(\sigma \) and suppose, for contradiction, that \(\sigma \) is not valid. Let \(M=(W,\le ,f,V)\) be an expanding model and \(w\in W\) such that \(M,w\not \models \sigma \). For brevity, we will identify each node in \(\pi \) with the sequent that labels it.

We will inductively define a path \((\sigma _i)_i\) of sequents through \(\pi \), a sequence of worlds \((w_i)_i\) in M and a sequence of signatures \((\tau _i)_i\) such that the following hold for every \(i<\omega \):

1. 1.

   \(\tau _i\) is a signature for \(\sigma _i\);

2. 2.

   \(w_i\models \bigwedge \varGamma _{\sigma _i}[\tau _i]\) and \(w_i\not \models \bigvee \varDelta _{\sigma _i}\) (and thus \(w_i\not \models \sigma _i[\tau _i]\) and \(w_i\not \models \sigma _i\));

3. 3.

   for every eventuality E of \(\sigma _i\), the following hold:

   1. (a)

      \(\tau _i(E)\) is the least natural number k such that \(w_i\models E[k]\);

   2. (b)

      if E is a side formula in the rule application with conclusion \(\sigma _i\), then E is an eventuality of \(\sigma _{i+1}\) and \(\tau _{i+1}(E)\le \tau _i(E)\).

We define \((\sigma _i)_i\), \((w_i)_i\) and \((\tau _i)_i\) as follows.

Set \(\sigma _0=\sigma \). Since \(w\not \models \sigma \), there exists a \(v\ge w\) such that \(v\models \bigwedge \varGamma _\sigma \) and \(v\not \models \bigvee \varDelta _\sigma \). Set \(w_0=v\) and for every eventuality E in \(\varGamma _\sigma \), define \(\tau _0(E)\) to be the least k such that \(w_0 \models E[k]\).

Suppose \(\sigma _i\), \(w_i\) and \(\tau _i\) are given. We use a case distinction based on the rule applied at \(\sigma _i\) in \(\pi \) (i.e. the rule that has \(\sigma _i\) as conclusion). Note that this rule cannot be an axiom, since \(w_i\not \models \sigma _i\). We only show the cases \({\rightarrow }\textrm{R}\), \(\textsf{X}\textrm{L}\), \(\textrm{S}\), and \(\mathbin {\textsf{U}}\textrm{L}\); the other cases are treated in a straightforward way.

\({\rightarrow } \textrm{R}\):

Suppose \(\sigma _i= (\varGamma \Rightarrow A\rightarrow B^0,\varDelta )\) with \(A\rightarrow B^0\) principal in the rule application. Let \(\sigma _{i+1}=(\varGamma , A^0\Rightarrow B^0)\). Since \(w_i \not \models A \rightarrow B^0\), there exists a \(w_{i+1} \ge w_i\) such that \(w_{i+1} \models A^0\) and \(w_{i+1}\not \models B^0\). For any eventuality E in \(\varGamma \cup \{A^0\}\), let \(\tau _{i+1}\) map E to the least k such that \(w_{i+1}\models E[k]\). Since \(w_{i+1}\ge w_i\), by monotonicity (Lemma 1) we have \(\tau _{i+1}(E)\le \tau _{i}(E)\) for each eventuality E in \(\varGamma \).

\(\textsf{X}\textrm{L}\):

Suppose \(\sigma _i= (\varGamma , \textsf{X}A^n\Rightarrow \varDelta )\) with \(\textsf{X}A^n\) principal in the rule application. Let \(\sigma _{i+1}=(\varGamma , A^{n+1}\Rightarrow \varDelta )\) and \(w_{i+1}=w_i\). If \(A^{n+1}\) is an eventuality, define \(\tau _{i+1}(A^{n+1}){:}{=}\tau _i(\textsf{X}A^n)\). On other eventualities, \(\tau _{i+1}\) acts as \(\tau _i\).

\(\textrm{S}\):

Suppose \(\sigma _i= (\varSigma ,\varGamma ^{+1} \Rightarrow \varDelta ^{+1},\Pi )\) such that \(\varGamma \Rightarrow \varDelta \) is the premise of the rule application. Let \(\sigma _{i+1}=(\varGamma \Rightarrow \varDelta )\), \(w_{i+1}=f(w_i)\) and \(\tau _{i+1}(A^n)=\tau _i(A^{n+1})\) for every eventuality \(A^n\) in \(\varGamma \).

\(\mathbin {\textsf{U}}\textrm{L}\):

Suppose \(\sigma _i= (\varGamma , A\mathbin {\textsf{U}}B^n\Rightarrow \varDelta )\) with \(A\mathbin {\textsf{U}}B^n\) principal in the rule application. If \(\tau _i(A\mathbin {\textsf{U}}B^n)=0\), let \(\sigma _{i+1}=(\varGamma , B^n\Rightarrow \varDelta )\) and \(w_{i+1}=w_i\). If \(B^n\) is an eventuality and not in \(\varGamma \), let \(\tau _{i+1}\) map \(B^n\) to the least k such that \(w_{i+1}\models B^n[k]\). On other eventualities, \(\tau _{i+1}\) acts as \(\tau _i\). Alternatively, if \(\tau _i(A\mathbin {\textsf{U}}B^n)>0\), let \(\sigma _{i+1}=(\varGamma , A^n, \textsf{X}(A\mathbin {\textsf{U}}B)^n\Rightarrow \varDelta )\) and \(w_{i+1}=w_i\). If \(A^n\) is an eventuality and not in \(\varGamma \), let \(\tau _{i+1}\) map \(A^n\) to the least k such that \(w_{i+1}\models A^n[k]\). Define \(\tau _{i+1}(\textsf{X}(A\mathbin {\textsf{U}}B)^n)=\tau _i(A\mathbin {\textsf{U}}B^n)-1\). On other eventualities, \(\tau _{i+1}\) acts as \(\tau _i\).

It is easy to verify that \((\sigma _i)_i\), \((w_i)_i\) and \((\tau _i)_i\) satisfy properties 1–3.

Since \(\pi \) is a proof, the infinite branch \((\sigma _i)_i\) must contain a good trace \((A_i)_{i \ge j}\) starting in some sequent \(\sigma _j\). By Lemma 2, we may assume that this trace only passes actively through the rules \(\textsf{X}\textrm{L}\), \(\textrm{S}\) and \(\mathbin {\textsf{U}}\textrm{L}\), and it cannot pass through the latter in a degenerative way.^{Footnote 4} Now consider the infinite sequence \((\tau _i(A_i))_{i \ge j}\) of natural numbers. Note that, by property 3(b), if \(A_i\) is a side formula then \(\tau _{i+1}(A_{i+1})\le \tau _{i}(A_{i})\). Moreover, if \(A_i\) is principal in an application of \(\textsf{X}\textrm{L}\) or \(\textrm{S}\) then \(\tau _{i+1}(A_{i+1})= \tau _{i}(A_{i}),\) and if \(A_i\) is principal in a (non-degenerative) application of \(\mathbin {\textsf{U}}\textrm{L}\) then \(\tau _{i+1}(A_{i+1})<\tau _{i}(A_{i})\). As the trace is good, the latter case occurs infinitely often, and so we obtain an infinite, strictly decreasing sequence of natural numbers and thereby a contradiction.

This section establishes completeness of \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) with respect to the class of expanding models. For each sequent \(\sigma \) we construct an infinite two-player game between Prover (\(\textsf{Prov}\)) and Refuter (\(\textsf{Ref}\)) such that a winning strategy for \(\textsf{Prov}\) corresponds to a proof of \(\sigma \) and a winning strategy for \(\textsf{Ref}\) to the existence of a countermodel for \(\sigma \). The game will be played on a proof search tree, which is a finitely branching, ill-founded tree that presents a systematic search for a proof of \(\sigma \). In this tree, non-invertible rules will only be applied to saturated sequents.

Definition 9

A sequent \(\varGamma \Rightarrow \varDelta \) is left-saturated if the following hold.

1. 1.

   if \(A\wedge B^n\in \varGamma \), then \(A^n,B^n\in \varGamma \);

2. 2.

   if \(A\vee B^n\in \varGamma \), then \(A^n\in \varGamma \) or \(B^n\in \varGamma \);

3. 3.

   if \(A\rightarrow B^n\in \varGamma \), then \(A^n\in \varDelta \) or \(B^n\in \varGamma \);

4. 4.

   if \(\textsf{X}A^n\in \varGamma \), then \(A^{n+1}\in \varGamma \);

5. 5.

   if \(A\mathbin {\textsf{U}}B^n\in \varGamma \), then there exists an \(m\ge n\) such that \(B^m\in \varGamma \) and \(A^k\in \varGamma \) for all \(n\le k< m\).

The sequent is saturated if, in addition,

1. 6.

   if \(A\wedge B^n\in \varDelta \), then \(A^n\in \varDelta \) or \(B^n\in \varDelta \);

2. 7.

   if \(A\vee B^n\in \varDelta \), then \(A^n,B^n\in \varDelta \);

3. 8.

   if \(\textsf{X}A^n\in \varDelta \), then \(A^{n+1}\in \varDelta \);

4. 9.

   if \(A\mathbin {\textsf{U}}B^0\in \varDelta \), then \(B^0,A^0\in \varDelta \) or \(B^0,\textsf{X}(A\mathbin {\textsf{U}}B)^0\in \varDelta \).

Given a sequent \(\sigma \), we say that a formula \(\phi \) is saturated in \(\sigma \) if \(\sigma \) satisfies the relevant saturation clause for \(\phi \).

Note that the saturation clause for right \(\mathbin {\textsf{U}}\)-formulas is restricted to the zeroth nesting level. The saturation clause for left \(\mathbin {\textsf{U}}\)-formulas is needed to ensure that the valuation of the countermodel constructed from a failed proof search is monotone. This will become evident once we define such countermodels later in this section.

As we are working with set sequents, formulas can simultaneously function as principal and side formulas. To avoid creating infinite branches with no good trace, one needs to be explicit about how rules may be applied in the proof search tree. We call an application of a rule succinct if the principal formula(s) is not also a side formula, and preserving if the principal formula(s) is also a side formula. For example, an application of \(\textsf{X}\textrm{L}\) of the form given in Fig. 2 is succinct if \(\textsf{X}A^n \not \in \varGamma \) and preserving if \(\textsf{X}A^n \in \varGamma \). Rule applications of \({\rightarrow } \textrm{R}\) and \(\textrm{S}\) are always succinct. Note that succinct and preserving are dual notions; we find it useful to refer to them as separate concepts as they each highlight a key property of the proof search tree.

Definition 10

A proof search tree T for a sequent \(\sigma \) is a finite or infinite tree whose nodes are labelled according to the rules of \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) and in which the following holds.

1. 1.

   The root of T is labelled by \(\sigma \).

2. 2.

   A node of T is a leaf if and only if it is labelled by an axiom.

3. 3.

   Every left rule application is succinct.

4. 4.

   Every right rule application except \({\rightarrow } \textrm{R}\) is preserving.

5. 5.

   No invertible rule is applied to a sequent in which the principal formula is already saturated.

6. 6.

   Instead of the rules \({\rightarrow } \textrm{R}\) and \(\textrm{S}\), we have the rule

   

   where it is required that every formula in \(\varSigma \cup \Pi \) is of nesting level 0, \(\Pi \) does not contain a formula of the form \(A\rightarrow B^0\) and the conclusion is a saturated sequent. We call the premises of the form \(\varSigma ,\varGamma ^{+1}, A_i^0 \Rightarrow B_i^0\) the left premises, and \(\varGamma \Rightarrow \varDelta \) the right premise of \(\textrm{C}\).

The ‘choice’ rule \(\textrm{C}\) represents a choice between non-invertible rules that \(\textsf{Prov}\) has to make once the sequent is saturated. Note that the empty sequent is saturated; an empty sequent in a proof search tree can only be the conclusion of a \(\textrm{C}\)-rule and has another empty sequent as its only direct successor.

Given a sequent \(\sigma \), one can build a proof search tree as follows. First try to saturate all left formulas by succinctly applying invertible left rules. If a left-saturated sequent is obtained, saturate all right formulas by preservingly applying invertible right rules, then apply \(\textrm{C}\) and start over. Observe that it is possible that some branches in a proof search tree do not contain a saturated sequent due the fifth saturation clause.

The following lemmas describe some key properties of proof search trees. For a node s in a proof search tree, we write \(\varGamma _s\Rightarrow \varDelta _s\) to denote the sequent labelling the node s.

Lemma 3

If T is a proof search tree wherein \(s\in T\) is the conclusion of a \(\textrm{C}\)-application with right premise \(t\in T\), then the following hold.

1. 1.

   t is labelled by a left-saturated sequent;

2. 2.

   if \(r\ge t\) and no \(\textrm{C}\)-application occurs between t and r, then \(\varGamma _r=\varGamma _t\).

Lemma 4

Every infinite branch of a proof search tree T contains infinitely many applications of \(\mathbin {\textsf{U}}\textrm{L}\) or \(\textrm{C}\).

Proof

Let \((\rho _i)_{i < \lambda }\) be a branch of T (where \(\lambda \le \omega \)). Suppose there exists a suffix \((\rho _i)_{j \le i < \lambda }\) that contains no applications of \(\mathbin {\textsf{U}}\textrm{L}\) or \(\textrm{C}\). Due to property 3 to 5 of the proof search tree, there exists a \(k\ge j\) such that all formulas except for left \(\mathbin {\textsf{U}}\)-formulas will be saturated in \(\rho _k\). The only rules which may be applied at that point are \(\mathbin {\textsf{U}}\textrm{L}\) or \(\textrm{C}\), showing that \((\rho _i)_{i < \lambda }\) must be finite.

Lemma 5

Every infinite branch of a proof search tree T that contains only finitely many \(\textrm{C}\)-applications has a suffix with a good formula trace.

Proof

Let \(\beta \) be an infinite branch of T with finitely many \(\textrm{C}\)-applications. Let \(\rho \) be a suffix of \(\beta \) that starts after the last \(\textrm{C}\)-application. By the previous lemma, \(\rho \) must contain infinitely many applications of \(\mathbin {\textsf{U}}\textrm{L}\). We show that \(\rho \) contains a good trace.

Consider the tree \(T_{\rho }\) of formula traces on \(\rho \) (add a fresh node as the root). Now let \(T'_{\rho }\) be the tree obtained from \(T_\rho \) by identifying consecutive nodes that are labelled by the same formula. Note that \(T'_\rho \) cannot be finite, since \(\rho \) must contain infinitely many applications of \(\mathbin {\textsf{U}}\textrm{L}\) and this rule may not be applied to formulas that also function as a side formula. By König’s lemma, \(T'_\rho \) contains an infinite branch. Note that this branch corresponds to an infinite formula trace \((A_i)_{i}\) on \(\rho \) that does not stagnate on a side formula, that is, \((A_i)_{i}\) actively passes through a left rule infinitely often. Property 3 to 5 of the proof search tree and absence of \(\textrm{C}\)-applications then imply that \((A_i)_{i}\) actively passes through \(\mathbin {\textsf{U}}\textrm{L}\) infinitely often.

We are now ready to define the notion of a refutation which corresponds to a winning strategy for \(\textsf{Ref}\).

Definition 11

A refutation of a sequent \(\sigma \) is a subtree R of a proof search tree T for \(\sigma \) such that the following hold.

1. 1.

   R contains the root of T.

2. 2.

   Every branch of R is infinite.

3. 3.

   If a node s in R is (labelled by) the conclusion of an application of \(\textrm{C}\) in T, then R contains all direct successors of s in T.

4. 4.

   If a node s in R is (labelled by) the conclusion of an application of any rule other than \(\textrm{C}\) in T, then R contains exactly one direct successor of s in T.

5. 5.

   No infinite branch of R contains a path with a good formula trace.

Note that the final condition above together with Lemma 4 implies that every branch in a refutation must contain infinitely many applications of the \(\textrm{C}\)-rule.

Proposition 1

Every sequent with a refutation has an expanding countermodel.

The proof of the above proposition is provided in the following section. For now, we turn to defining the proof search game which is instrumental in the completeness proof.

Given a sequent \(\sigma \) and a proof search tree T for \(\sigma \), the proof search game \(\mathcal {G}(T, \sigma )\) is defined as follows. The game is played by two players \(\textsf{Prov}\) and \(\textsf{Ref}\). The arena of the game is the proof search tree T. Each play starts in the root of T, which is labelled by \(\sigma \). If the current play is in position t, where t is a node of T, and t is owned by player \(\textsf{P} \in \{\textsf{Prov}, \textsf{Ref}\}\), then \(\textsf{P}\) plays by choosing a direct successor of t in T. \(\textsf{Prov}\) owns all positions that are conclusions of applications of the \(\textrm{C}\)-rule while every other position is owned by \(\textsf{Ref}\). If a play reaches a node that has no successors (i.e. an axiom), then the play ends and is called finite; otherwise the play is called infinite. Observe that every play directly corresponds to a branch of T. The winning conditions are as follows: finite plays are won by \(\textsf{Prov}\) and infinite plays are won by \(\textsf{Prov}\) if the infinite branch of T to which the play corresponds contains a good trace, and won by \(\textsf{Ref}\) otherwise. We make use of the standard notion of a (winning) strategy for players. The following lemma is then a straightforward consequence of the winning conditions of the game \(\mathcal {G}(T, \sigma )\).

Lemma 6

If there is a winning strategy for \(\textsf{Prov}\) in \(\mathcal {G}(T,\sigma )\), then \(\sigma \) has a \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\)-proof, and if there is a winning strategy for \(\textsf{Ref}\), then \(\sigma \) has a refutation.

As the set of winning plays (for each player) is Borel, it follows from Martin’s determinacy theorem [17] that the game \(\mathcal {G}(T,\sigma )\) is determined for any sequent \(\sigma \) and proof search tree T. That is, exactly one player has a winning strategy in \(\mathcal {G}(T,\sigma )\). As every sequent has a proof search tree, completeness of \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) is then obtained as a direct consequence of Proposition 1 and Lemma 6.

Theorem 2

Every sequent valid over the class of expanding models is provable in \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\).

5.1 Proof of Proposition 1

Let R be a refutation of \(\sigma \). Recall that, for any node \(s\in R\), \(\varGamma _s\Rightarrow \varDelta _s\) denotes the sequent labelling s. We define a dynamic model \(M=(W, \le , f, V)\) as follows.

1. 1.

   \(W=R/{\sim }\), where \(s\sim t\) iff there exists a path between s and t in which no \(\textrm{C}\)-application occurs.

2. 2.

   Define the function f by

   $$\begin{aligned} f(w)=v\ \textrm{ iff }&\ \mathrm {there\ exist }\ s \in w\ \textrm{ and }\ t\in v\ \mathrm { such\ that }\ s\ \mathrm { is\ the\ conclusion} \\ {}&\textrm{and }\ t\ \mathrm { is\ the }\ right\mathrm \ \mathrm { premise\ of\ the\ same }\ \textrm{C}\mathrm {-}\mathrm {application.} \end{aligned}$$

   Note that f is a total function, since every branch of R contains infinitely many \(\textrm{C}\)-applications and every \(\textrm{C}\)-application has a right premise.

3. 3.

   First define the relation \(\le _0\) on W by

   $$\begin{aligned} w\le _0 v\ \textrm{ iff }&\ \mathrm {there\ exist }\ s\ \in w\ \textrm{ and }\ t\ \in v\ \mathrm { such\ that }\ s\ \mathrm { is\ the\ conclusion} \\ {}&\textrm{and }\ t\ \textrm{ a }\ left\mathrm \ \mathrm { premise\ of\ the\ same }\ \textrm{C}\mathrm {-application.} \end{aligned}$$

   Then let \(\le \) be the transitive reflexive closure of the relation

   $$\begin{aligned} \le _1\ {:}{=}\{(f^n(w),f^n(v)): w\le _0 v \text { and } n<\omega \}. \end{aligned}$$
4. 4.

   Define the valuation by \( V(w)=\{p\in \textsf{Prop}: p^0\in \varGamma _{w}\} \) where \( \varGamma _w = \bigcup _{s\in w} \varGamma _{s}. \)

Similar to \(\varGamma _w\) we write \(\varDelta _w\) for \(\bigcup _{s\in w} \varDelta _{s}\).

Lemma 7

M is an expanding model.

Proof

Forward confluence follows directly from the definition of \(\le _1\). For monotonicity of the valuation, note that it suffices to show that the relation \(\le _1\) is monotone in V. In the following, we write [t] for the equivalence class of t with respect to \(\sim \).

Let \(w,v\in W\) with \(w\le _1 v\). Then there exist \(n<\omega \) and \(s,t\in R\) such that \(w=f^n([s])\), \(v=f^n([t])\) and t is a left premise of a \(\textrm{C}\)-application on s. Note that this means that w is reached from [s] by applying the \(\textrm{C}\)-rule n times while always taking the right premise, and similarly for v and [t]. From Lemma 3 and definition of \(\textrm{C}\), it follows that for any atomic proposition p,

So we have the following chain of implications

where the middle implication follows from the definition of \(\textrm{C}\). This shows \(V(w)\subseteq V(v)\) as required.

Lemma 8

For any \(w\in W\), we have \(M,w\models \bigwedge \varGamma _{w}\) and \(M,w\not \models \bigvee \varDelta _{w}\).

Proof

Let A be a formula. By induction on the logical complexity of A, we simultaneously prove that for any \(w\in W\) and \(n<\omega \) we have (a) \(w\models A^n\) if \(A^n\in \varGamma _{w}\) and (b) \(w\not \models A^n\) if \(A^n\in \varDelta _{w}\).

We only treat the propositional case and the connectives \(\rightarrow \) and \(\mathbin {\textsf{U}}\). The proof relies on the \(\textrm{C}\)-rule being applied only on a saturated conclusion. Thus the sequent \(\varGamma _w\Rightarrow \varDelta _w\) is saturated for every \(w\in W\).

We begin with (a). Suppose \(A^n \in \varGamma _w\). If \(A \in \textsf{Prop}\), then \(A^0\in \varGamma _{f^n(w)}\) and thus \(w\models \textsf{X}^n A\). If \(A = B \mathbin {\textsf{U}}C\), by saturation there exists an \(m\ge n\) such that \(C^m\in \varGamma _w\) and \(B^k\in \varGamma _w\) for all \(n\le k< m\). Thus \(w\models A^n\) by the IH. This leaves the case \(A = B \rightarrow C\). Let \(s\in w\) be the (unique) conclusion of a \(\textrm{C}\)-application. By definition of \({\rightarrow }\textrm{L}\), we have \(C^n\in \varGamma _w\) or \(B\rightarrow C^n\in \varGamma _s\). In the first case, the IH implies \(w\models C^n\) hence \(w\models A^n\). The second case is more involved. We have \(A^0\in \varGamma _{f^n(w)}\) by Lemma 3. Define \(u{:}{=}f^n(w)\) and let \(v\ge u\). We will restrict ourselves to the case that \(v\ge _1 u\); the argument can be extended to the general case using the monotonicity lemma. Let \(r,t\in R\) and \(m<\omega \) be such that \(u=f^m([r])\), \(v=f^m([t])\) and t is a left premise of a \(\textrm{C}\)-application with conclusion r. Since \(A^0\in \varGamma _u\), we have \( A^{m}\in \varGamma _{r}\) (by Lemma 3), which implies that \( A^{m}\in \varGamma _{t}\). As before, we then have \(C^m\in \varGamma _{[t]}\) or \( A^{m}\in \varGamma _{t'}\), where \(t'\in [t]\) is the conclusion of a \(\textrm{C}\)-application. This implies \(v\models C^0\) (by the IH) or \(A^{0}\in \varGamma _{v}\) (by Lemma 3). In the second case, saturation implies that \(C^0\in \varGamma _v\) or \(B^0\in \varDelta _v\). Applying the IH, either \(v\models C^0\) or \(v\not \models B^0\). Thus \(u\models A^0\) and thereby \(w\models A^n\).

We now consider (b). Suppose \(A^n \in \varDelta _w\). If \(A\in \textsf{Prop}\), then \(A^n\notin \varGamma _w\) since no sequent in R can be an axiom. By the same argument used to obtain (1), we have \(A^0\notin \varGamma _{f^n(w)}\) and thus \(w\not \models \textsf{X}^n A\). If \(A = B\rightarrow C\), then \(A^0\in \varDelta _{f^n(w)}\). As the \(\textrm{C}\)-rule must be applied to some (namely the highest) sequent in the equivalence class \(f^n(w)\), it must be the case that \(f^n(w)\) has an intuitionistic successor v such that \(B^0\in \varGamma _v\) and \(C^0\in \varDelta _v\). The IH then implies \(f^n(w)\not \models A^0\) and thus \(w\not \models A^n\).

Finally, if \( A = B \mathbin {\textsf{U}}C\), then \(A ^0 \in \varDelta _{f^n(w)}\) because \(\mathbin {\textsf{U}}\textrm{R}\)-applications are preserving. Saturation and the IH implies \(f^n(w)\not \models C^0\) and either \(f^n(w)\not \models B^0\) or \(A^1\in \varDelta _{f^n(w)}\). Similarly, for every \(m\ge n\), if \(A^1\in \varDelta _{f^{m}(w)}\) then \(f^{m+1}(w)\not \models C^0\) and either \(f^{m+1}(w)\not \models B^0\) or \(A^1\in \varDelta _{f^{m+1}(w)}\). So either there exists an \(m\ge n\) such that \(f^m(w)\not \models B^0\) and \(f^k(w)\not \models C^0\) for all \(n\le k\le m\), or \(f^m(w)\not \models C^0\) for all \(m\ge n\). Either way, \(w\not \models A^n\).

We conclude that the expanding model M falsifies \(\sigma \).

5.2 A Sequent Unprovable with Bounded Nesting

We have shown that the calculus \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) is complete with respect to the class of expanding models via a proof search argument. However, our argument does not yield regular completeness. Observe that in the construction of the proof search tree, there is no bound given on the nesting depth occurring in sequents. Indeed, in order to saturate \(\mathbin {\textsf{U}}\)-formulas on the left, one has to keep unfolding them until the left premise is chosen, which, in case of a successful branch, might never happen. Hence, proofs might have arbitrary large nesting depth and there is thus no guarantee that infinite branches will contain repetitions. This observation raises the question of whether the completeness proof can be adapted to obtain a bound on the nesting depth occurring in \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\)-proofs. Unfortunately, this is not possible, as there are sequents that are not provable in \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) with bounded nesting depth. An example for this is the sequent

where \(\Diamond A := \top \mathbin {\textsf{U}}A\) and \(\top :=\bot \rightarrow \bot \). For brevity, instead of the \(\mathbin {\textsf{U}}\)-rules we will use the following rules for \(\Diamond \).

It is easy to see that any formula in the \(\Diamond \)-fragment of \(\textsf{iLTL}\) is provable in \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) if and only if it is provable in \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) with the \(\Diamond \)-rules instead of the \(\mathbin {\textsf{U}}\)-rules.

Let us now consider the following proof \(\pi \) of the sequent \( \Diamond (A \vee B)^0 \Rightarrow C \rightarrow \Diamond A^0, C \rightarrow \Diamond B^0\).

The subproof \(\pi _0\) is given as follows.

The subproof \(\pi _1\) is similar, the only difference being that the formulas \(\Diamond A^0\) and \(\Diamond B^0\) have to be unfolded twice to reach an axiom instead of just once. In the same way, we obtain the subproofs \(\pi _i\) for each \(i<\omega \).

Note that \(\pi \) is indeed a proof, as it contains only one infinite branch and this branch contains a good trace, and that the nesting depth in \(\pi \) is unbounded. Furthermore, note that any proof of this sequent will have an infinite branch on the right with unbounded nesting levels. Working bottom-up, applying any other rule than \(\Diamond \textrm{L}\) to the root sequent results in an unprovable sequent, and applying any rule other than \(\textsf{X}\textrm{L}\) to its right premise results in an unprovable sequent as well. The same argument applies to each sequent in the right-most branch of \(\pi \).

Interestingly, allowing analytic cuts there is a proof of this sequent with nesting depth bounded by 1, the cut formula being \(\Diamond A \vee \Diamond B^0\).

The system \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) can be adapted to a sound and complete proof system for the logic \(\textsf{iLTL}_\textsf{p}\) of validities over persistent models.

Definition 12

The sequent calculus \(\textsf{iLTL}{_\textsf{p}}^{\textsf{nest}}\) consists the rules of \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) except \(\textrm{S}\) and \({\rightarrow }\textrm{R}\) which are replaced by

Derivations, paths, (good) formula traces and proofs are defined for \(\textsf{iLTL}{_\textsf{p}}^{\textsf{nest}}\) just as for \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\), and it is easy to see that Lemma 2 still holds. To prove soundness, one can simply follow the proof of Theorem 1 and in the case for \({\rightarrow }\textrm{R}_\textsf{p}\) invoke the validity of \((\textsf{X}A\rightarrow \textsf{X}B)\rightarrow \textsf{X}(A\rightarrow B)\) over the class of persistent models.

To show completeness, we will adapt the proof search for \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) by introducing different levels of saturation.

Definition 13

Let \(k<\omega \). A sequent \(\varGamma \Rightarrow \varDelta \) is k-saturated if it satisfies clauses 1-8 of Definition 9 and the additional clause

1. 9.

   for all \(n\le k\), if \(A\mathbin {\textsf{U}}B^n\in \varDelta \), then \(B^n,A^n\in \varDelta \) or \(B^n,\textsf{X}(A\mathbin {\textsf{U}}B)^n\in \varDelta \).

Given a sequent \(\sigma \), we say that a formula A is k-saturated in \(\sigma \) if \(\sigma \) satisfies the relevant k-saturation clause for A.

Note that 0-saturation is equivalent to our earlier notion of saturation.

To keep track of the level of saturation in sequents, the proof search tree will be labelled by indexed sequents \(\varGamma \Rightarrow _k \varDelta \), that is, sequents equipped with a natural number \(k<\omega \).

Definition 14

A persistent proof search tree T for a sequent \(\varGamma \Rightarrow \varDelta \) is a finite or infinite tree whose nodes are labelled with indexed sequents following the rules of \(\textsf{iLTL}{_\textsf{p}}^{\textsf{nest}}\) such that:

1. 1.

   The root of T is labelled by \(\varGamma \Rightarrow _0 \varDelta \).

2. 2.

   A node of T is a leaf if and only if it is labelled by an axiom.

3. 3.

   Invertible rule applications leave the index of a sequent unchanged.

4. 4.

   Every left rule application is succinct.

5. 5.

   Every right rule application apart from \({\rightarrow }\textrm{R}_\textsf{p}\) is preserving.

6. 6.

   No invertible rule is applied to a sequent of index k in which the principal formula is already k-saturated.

7. 7.

   In place of the rule \({\rightarrow }\textrm{R}_\textsf{p}\), the rule

   

   is utilised, where \(\varDelta \) may not contain a formula of the form \(A\rightarrow B^k\) and the conclusion of the rule is a k-saturated sequent.

It is easy to see that every sequent has a persistent proof search tree and that Lemma 3, 4 and 5 also hold for persistent proof search trees. Following Definition 11, we define a persistent refutation as a subtree of a persistent proof search tree satisfying properties 1-5 of Definition 11, with \(\textrm{C}\) replaced by \(\textrm{C}_\textsf{p}\). As before, the fifth property ensures that every branch in a persistent refutation passes through the \(\textrm{C}_\textsf{p}\)-rule infinitely often.

Via a game-theoretic argument, we obtain completeness of \(\textsf{iLTL}{_\textsf{p}}^{\textsf{nest}}\) as a corollary of the following proposition.

Proposition 2

If a sequent \(\sigma \) has a persistent refutation, then it has a persistent countermodel.

Due to space limit the proof is omitted. The main difference to the proof of Proposition 1 is that, when constructing a persistent countermodel from a persistent refutation, right premises of the \(\textrm{C}_\textsf{p}\)-rule are not viewed as temporal successors but as a further description of the current world w. In the limit, this description fully determines the temporal ‘successors’ \(f^n(w)\) for every n, whereby these successors can be added accordingly. Due to this limit construction, worlds in the obtained countermodel may have infinitely many intuitionistic successors, which is not the case for the countermodel obtained in Proposition 1.

This investigation is part of a larger programme of devising sequent calculi for intuitionistic modal logic with fixed points to establish fundamental properties such as decidability and algorithmic proof search. To this aim, we introduce ill-founded cut-free sequent calculi for intuitionistic linear-time temporal logic over expanding and persistent models, denoted \(\textsf{iLTL}_\textsf{e}\) and \(\textsf{iLTL}_\textsf{p}\) respectively. The presented systems and the techniques devised to establish soundness and completeness are inspired by the study of ill-founded proof systems for classical temporal logics. In particular, we have illustrated how the method of proof search can be adapted to the intuitionistic realm.

A natural direction for future research is to extend \(\textsf{iLTL}_\textsf{e}\) and \(\textsf{iLTL}_\textsf{p}\) to logics containing greatest fixed point operators such as ‘henceforth’ and, more generally, ‘release’. The latter is the classical dual of \(\mathbin {\textsf{U}}\) which is not definable from \(\mathbin {\textsf{U}}\) in the intuitionistic setting [3]. Although we believe that our approach can be extended to handle more expressive temporal logics, an adaptation of the proof search strategy is by no means trivial. The presence of greatest fixed point formulas on the left-hand side of a sequent presents a challenge in ensuring that the model constructed from a refutation satisfies monotonicity.

Another possible direction is to devise complete cyclic calculi for \( \textsf{iLTL}\)-based logics. The main difficulty in turning an ill-founded proof into a cyclic one lies in our reliance on nested sequents. In the completeness proof, there is no guarantee that every infinite branch in a proof contains a repeated sequent. Indeed, as shown in Sect. 5.2, the sequent \(\Diamond (A \vee B)^0 \Rightarrow C \rightarrow \Diamond A^0, C \rightarrow \Diamond B^0\) admits a proof in \(\textsf{iLTL}{_\textsf{e}}^{\textsf{nest}}\) only with an unbounded nesting depth. This implies that a simple definition of repetition in an infinite branch will not result in a complete cyclic system. Incorporating the cut-rule into the systems, one can obtain a proof of the sequent wherein the nesting depth is at most \( 1 \). Since the required application of cut in this example requires only analytic formulas, it is worthwhile investigating whether the presented systems can be turned into cyclic systems with analytic cuts.