Preface↩︎

This thesis is the culmination of my doctoral studies in computer science at University of Bern between March 2021 and May 2024 and in mathematics at Ghent University between October 2024 and August 2025. My research was conducted under the supervision of Prof. Dr. Andreas Weiermann, Prof. Dr. Thomas Studer and Prof. Dr. David Fernández-Duque.

This thesis investigates a family of intuitionistic modal logics extended with fixed point operators. Such logics are used to reason about dynamic phenomena, such as the change within a mathematical system over time, the change of state in an automaton after a program step or the change of an agent’s knowledge after an information update. For this reason I refer to them as intuitionistic dynamic logics, where the term ‘dynamic’ highlights their role in formalizing processes of change. At the origin of my doctoral studies stood the goal to develop a coherent mathematical theory of intuitionistic temporal logics, whose modal and fixed point operators capture temporal properties such as ‘in the next time step’ or ‘eventually in the future’. As it often happens in theoretical research, my interests expanded over the course of my PhD, leading me to study related systems such as intuitionistic epistemic logic, bi-intuitionistic modal logic and intuitionistic modal logic with the master modality. All of these logics are discussed in detail in this thesis.

Although logic lies at the intersection of mathematics, philosophy and computer science, the focus here is primarily mathematical. A significant part of the thesis is devoted to the proof theory of intuitionistic dynamic logics, which is studied using Hilbert-style axiomatizations as well as non-wellfounded and cyclic sequent calculi. The latter two are proof systems that allow formal proofs to be infinitely long. Such infinite proofs are particularly well-suited to handle the infinite nature of fixed point operators, but they present considerable technical challenges. The remaining part of the thesis addresses model theoretic and computational aspects of intuitionistic dynamic logics, including expressivity, finite model property, decidability and complexity results.

Intuitionistic modal and dynamic logics are also relevant from a philosophical point of view. While I am interested in the philosophy of intuitionism and questions regarding intuitionistic justifications for modalities, such considerations are not included in the thesis. In fact, the intuitionist shall be warned: I use a classical metatheory when reasoning about intuitionistic dynamic logics and I do not attempt to provide an intuitionistic reading of the studied modalities.

Acknowledgments I would like to express my gratitude to the many people who have contributed to my thesis and my life in general during the past four years. First of all, I would like to thank my supervisors, Andreas Weiermann, Thomas Studer and David Fernández-Duque, for their guidance and help throughout my doctoral studies. Thomas, who was my main supervisor during the three years spent at the University of Bern, has helped me greatly to improve as a logician. I am particularly grateful for his course on proof theory, that he held on my request, which helped me learn about areas of proof theory that I had missed in my previous education. As a supervisor, he always provided me with the help I needed while at the same time giving me the academic freedom to pursue my own interests and learn to work independently. I am also grateful for his wise council regarding the many difficulties that I encountered during my doctoral studies. To Andreas, who was my main supervisor at Ghent University, I am particularly grateful that he provided to me the opportunity to continue my doctoral studies for an additional year after my funding ran out in Bern. This allowed me to bring my PhD to a satisfying conclusion. I would also like to thank him for his efforts organizing my defense and ensuring a smooth transition from Bern to Ghent. To David I would like to express my gratitude for his guidance and help in writing some of the papers that lead to this thesis. His impressive mathematical abilities and great ideas have contributed significantly to many of the results presented in the thesis and his explanations to my understanding of the topic. I also sincerely appreciate his council regarding the writing of this thesis and the suggestion for the title.

I thank the members of the examination committee for reading my thesis and the many helpful comments to improve it: Iris van der Giessen, Bahareh Afshari, Martín Diéguez Lodeiro, Seyedmojtaba Mojtahedi and Giovanni Solda.

I am deeply obliged to my co-authors for their contribution to my thesis: To Jan Rooduijn, Lide Grotenhuis, Brett McLean, David Fernández-Duque, Graham E. Leigh, Borja Sierra Miranda, Bahareh Afshari and Thomas Studer. I am very lucky to have had the opportunity to work with so many talented logicians and hope to continue our collaboration in the future. At this place a special thanks goes to Bahareh, who has guided my academic journey ever since I started my master’s degree in Amsterdam. As my master’s thesis supervisor, she introduced me to the topic of modal fixed point logics, helped me find a PhD position and continued her support throughout my doctoral studies. I also thank the logic groups in Bern and Ghent for the good working atmosphere, the interesting seminars and the social activities.

The last four years have by no means been easy for me. Apart from the pressure and the relative solitude that a PhD life brings, I have also struggled with my mental health. It is important in such situations to have a good social network. Luckily, I have been blessed with good friends and a supportive family. I would like to thank my parents Christoph and Beatrice for their continued support throughout my entire life and in particular in the recent weeks and months. I thank my brother Michael and his (soon to be) wife Luza for their care and visits after the submission of my thesis. A special thanks goes to my friends who have always supported me despite my struggles. Thank you Bas, Wijnand, Hugh Mee, Simon, Gabriel, Jiajia, Alessandro, Raphael, Tianwei, Irina, Massimo, Tong and Freddy.
Lukas Zenger
Bern, October 2025

1 Introduction↩︎

The subject of this thesis is intuitionistic dynamic logic: a family of logical systems characterized by two key features. First, they extend intuitionistic propositional logic with modalities and with fixed point operators. As such they are intuitionistic versions of modal fixed point logics. Second, they provide a formal framework for reasoning about change, whether in mathematical structures evolving over time or in the knowledge state of an agent after an information update. This chapter offers an informal overview of intuitionistic dynamic logics, outlines the motivation for their study, and summarizes the main contributions of the thesis. The formal definitions and results are developed in the subsequent chapters.

1.1 What Are Intuitionistic Dynamic Logics?↩︎

Intuitionistic dynamic logics build on two foundations: intuitionistic logic and intuitionistic modal logic, further enriched with fixed point operators.

Intuitionistic propositional logic (\(\mathsf{IPL}\)) shares the language of classical propositional logic (\(\mathsf{CPL}\)) but deviates from the latter in one crucial aspect: classical logic assumes the law of excluded middle, which states that for any proposition \(p\), the formula \(p \vee \neg p\) is true. As a consequence, every formula in classical logic is considered to be either true or false. Intuitionistic logic, on the other hand, rejects the law of excluded middle, which makes it a proper subsystem of \(\mathsf{CPL}\). Intuitionistic logic was developed by Heyting [1]–[3] with regard to the foundations of mathematics and has emerged as the logical basis of constructive mathematics [4]. \(\mathsf{IPL}\) has also found other interpretations based on topology, computation and, most relevant here, information.

In the information based interpretation of \(\mathsf{IPL}\) due to Kripke [5], an information state is a set \(w\) of propositions, each representing a piece of information available at \(w\). Propositions absent from \(w\) are not considered false but rather unsupported by the available data. The law of excluded middle is therefore not expected to hold, which motivates the use of intuitionistic instead of classical logic to reason about information. Kripke introduced formal semantics for \(\mathsf{IPL}\) based on information orderings: tuples \((W, \leq)\) where \(W\) is a set of information states and \(w \leq v\) means that the information state \(v\) contains all information of \(w\) and possibly more. In this semantics truth is monotone in \(\leq\): if \(w \models \varphi\) and \(w \leq v\), then \(v \models \varphi\). The evaluation of implications is given by \(w \models \varphi \rightarrow \psi\) if for all \(v \geq w\) if \(v \models \varphi\), then \(v \models \psi\). An implication \(\varphi \rightarrow \psi\) thus expresses the consequences of gaining information: \({w \models \varphi \rightarrow \psi}\) expresses that whenever \(w\) is extended by information making \(\varphi\) true, the information also makes \(\psi\) true.

Intuitionistic modal logic (\(\mathsf{IML}\)) extends \(\mathsf{IPL}\) by modal operators, typically \(\larger[-1.5]\square\) and \(\larger[-1.5]\Diamond\). Traditionally, \(\larger[-1.5]\square\varphi\) expresses that \(\varphi\) is necessarily true and \(\larger[-1.5]\Diamond\varphi\) that \(\varphi\) is possibly true. Other interpretations include \(\larger[-1.5]\square\varphi\) as \(\varphi\) is known in epistemic logic or \(\varphi\) is true in the next time step in temporal logic. Semantically, \(\mathsf{IML}\) employs dynamic models which are based on information orderings \((W, \leq)\) extended with a binary relation \(R \subseteq W \times W\). In difference to classical logic, where truth is static, the evaluation of formulas on dynamic models takes into account higher worlds relative to \(\leq\) as well as the worlds accessible over \(R\). Truth in \(\mathsf{IML}\) is therefore dynamic.

The information theoretic interpretation of \(\mathsf{IPL}\) naturally extends to \(\mathsf{IML}\), where the relation \(R\) is used to model non-monotonic information updates (e.g. updates that revise or discard information). The formula \(\larger[-1.5]\Diamond\varphi\) expresses that there exists an update after which \(\varphi\) is true, while \(\larger[-1.5]\square\varphi\) expresses that \(\varphi\) is true after every update. This yields the interpretation of \(\mathsf{IML}\) as logics to reason about monotone and non-monotonic information updates.

The study of intuitionistic modal logic originated in the seminal work of Fitch [6] in 1948. Since then \(\mathsf{IML}\) has grown into an active research area within logic, motivated by philosophical reasons [7]–[9] and by applications to computer science [10]–[12].

Intuitionistic dynamic logics further extend \(\mathsf{IML}\) with the capacity to express infinitary properties. To that end the language is extended by operators whose truth conditions are characterized as fixed points of specific functions, yielding the name fixed point operators. Such operators are not definable in the language of \(\mathsf{IML}\) and significantly increase its expressive power.

Apart from the master modality, many other fixed point operators will be encountered in this thesis, most notably in the context of temporal logics. Here, fixed point operators are used to express statements about the future, such as ‘eventually in the future, something will be the case’ or ‘henceforth in the future, something will always be the case’. Similar to the study of classical modal fixed point logics, most notably the modal \(\mu\)-calculus (see e.g. [13]), the addition of fixed point operators to \(\mathsf{IML}\) does not only increase the expressivity of the resulting logics, but also the difficulty of their mathematical theory, mostly due to the infinite nature of these operators. An overview of the state of the art of the study of intuitionistic dynamic logic is provided in the following subsection.

1.2 State of the Art↩︎

In difference to the study of intuitionistic modal logic, the study of intuitionistic dynamic logic is arguably still in its infancy. However, in recent years several intuitionistic dynamic logics have been introduced and studied in the literature. Among those are intuitionistic versions of temporal logic, which have been mainly studied in two different contexts: metaprogramming and topological dynamics. The former involves the addition of temporal operators to \(\lambda\)-calculi to model aspects of metaprogramming such as staged computation (see e.g. [14]–[16]). The latter is of particular interest to this thesis and dates back to the topological logic project. This project aims to develop computationally well-behaved logical systems to reason about topological dynamic systems, i.e. topological spaces equipped with a continuous function, with potential applications in automated theorem proving in mind. Topological dynamic systems are applied in diverse fields ranging from biology to theoretical computer science. The origin of the project dates back to the seminal work of Artemov, Davoren and Nerode [17] in the late 1990’s, who introduced a classical modal logic and showed how to interpret formulas on topological dynamic systems. In particular, the logic features a standard modal box operator interpreted as the interior operator on topological spaces in the sense of Tarski [18] as well as a modal operator ‘next’ to reason about the continuous function \(f\). Their logic was extended by Kremer and Mints [19] with the fixed point point ‘henceforth’ to reason about the asymptotic behaviour of \(f\), resulting in a logic called dynamic topological logic (\(\mathsf{DTL}\)). Unfortunately, \(\mathsf{DTL}\) was later shown to be undecidable [20], with which interest in \(\mathsf{DTL}\) waned. In 2018, Fernández-Duque introduced an intuitionistic version of linear temporal logic, called \(\mathsf{iLTL}\) in this thesis, and showed that it enjoys a natural interpretation both over topological dynamic systems as well as dynamic models based on information orderings [21]. Furthermore, he established the decidability of \(\mathsf{iLTL}\), thus providing a decidable logic capable of expressing interesting properties of topological dynamic systems. The logic \(\mathsf{iLTL}\) is an extension of intuitionistic propositional logic with a modality ‘next’ as well as a fixed point operator ‘eventually’ and thus an intuitionistic dynamic logic in our sense. It was later shown that \(\mathsf{iLTL}\) admits a sound and complete axiomatization [22] and that \(\mathsf{iLTL}\) extended with additional fixed point operators remains decidable [23]. The proof theory of \(\mathsf{iLTL}\), however, remains largely unexplored, with the exception of a cyclic sequent calculus introduced recently by Menéndez Turata in his PhD thesis [24].

Apart from intuitionistic temporal logics, intuitionistic dynamic logics have also been studied in an epistemic setting. Jäger and Marti introduced an intuitionistic version of common knowledge logic called \(\mathsf{ICK}\) [25], [26], which extends intuitionistic propositional logic by modal operators \(\mathsf{K}_i\), where \(\mathsf{K}_i \varphi\) expresses that an agent \(i\) knows \(\varphi\), as well as a fixed point operator expressing a powerful notion of group knowledge called common knowledge. Furthermore, variants of \(\mathsf{ICK}\) with operators for distributed knowledge were also studied in [27]–[29]. In difference to \(\mathsf{iLTL}\), the work in \(\mathsf{ICK}\) is primarily proof theoretic, highlighted by the development and study of axiomatizations and sequent calculi. Artemov and Protopopescu introduced a different version of intuitionistic epistemic logic called \(\mathsf{IEL}\) [8]. In difference to \(\mathsf{ICK}\), which treats knowledge as in the classical case, Artemov and Protopopescu aim to give an intuitionistic reading to knowledge, resulting in a substantially different logical systems.

Last but not least, intuitionistic versions of the modal \(\mu\)-calculus have recently been studied by Pacheco [30] who focuses on game semantics and by Afshari and Grotenhuis [31] who develop non-wellfounded and cyclic proof systems for intuitionistic \(\mu\)-calculus with the Lewis arrow.

1.3 Motivation↩︎

The original motivation for the research presented in this thesis is related to the dynamic topological logic project and the logic \(\mathsf{iLTL}\). As mentioned in the previous subsection, the proof theory of \(\mathsf{iLTL}\) is largely unexplored, a gap which needs to be filled when it comes to application in automated theorem proving. Moreover, while a sound and complete axiomatization for \(\mathsf{iLTL}\) was provided in [22], the problem of finding an axiomatization for the extended language with ‘henceforth’ has remained open for several years. Importantly, while the set of validities of \(\mathsf{iLTL}\) evaluated over topological models coincides with the set of validities over dynamic models based on information orderings, the same is not true in the extended language (see Chapter 6). The main goal of this thesis was therefore to develop the proof theory of \(\mathsf{iLTL}\) and a sound and complete axiomatization for the extended language of \(\mathsf{iLTL}\) with ‘henceforth’, in the setting of dynamic models based on information orderings. The presence of fixed point operators complicates this venture, due to the fact that proof systems require a formal counterpart to induction to reason about fixed point operators. Luckily, modal fixed point logics have been studied extensively in the classical realm and it is the methods developed there that come to the rescue. In the classical realm, automata, games, non-wellfounded and cyclic proofs as well as semantic techniques such as filtrations and simulations have proven suitable for the study of fixed points in modal logic [32]–[34]. Little is known, however, whether these techniques are applicable to the intuitionistic case. In fact, it can be expected that the application of such methods is significantly complicated, due to the underlying intuitionistic logic and the more complicated mathematical structures used to evaluate formulas (i.e. dynamic models). A second motivation, based in mathematical curiosity, is therefore to investigate how to adapt such techniques, in particular non-wellfounded and cyclic proofs, to the intuitionistic case, with the hope that our findings will not only provide a rigorous mathematical theory for \(\mathsf{iLTL}\), but also prove useful for the study of other, related logical systems. Thus the second motivation naturally leads to a third one, which is to explore related logics and to adapt the techniques developed for \(\mathsf{iLTL}\) to these systems.

From a more general perspective, intuitionistic modal and dynamic logics have found tangible applications in computer science, for example to model aspects of metaprogramming such as staged computation [12], [14], [15], [35]–[37] and to philosophy, for example to give an intuitionistic account of knowledge [8], [9], [38]. Furthermore, the information theoretic interpretation of intuitionistic dynamic logics opens the possibility for applications to artificial intelligence, such as to knowledge representation, (epistemic) planning or logic programming. These applications in turn motivate the development of a rigorous mathematical theory, and in particular well-behaved proof systems that facilitate proof-search algorithms. Moreover, applications to computer science lead to the study of the computational properties of intuitionistic dynamic logics.

1.4 Contributions↩︎

This thesis studies five intuitionistic dynamic logics:

1. Intuitionistic master modality (\(\mathsf{IM}\)): an intuitionistic dynamic logic which extends \(\mathsf{IPL}\) by a single modality \(\larger[-1.5]\square\) and the aforementioned master modality \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\).

2. Intuitionistic common knowledge logic (\(\mathsf{ICK}\)): an intuitionistic version of epistemic logic with common knowledge introduced by Jäger and Marti [25].

3. Intuitionistic linear temporal logic (\(\mathsf{iLTL}\)): an intuitionistic version of linear temporal logic introduced by Fernández-Duque [21].

4. Bi-intuitionistic modal logic (\(\mathsf{biML}\)): an extension of \(\mathsf{IPL}\) with modalities \(\larger[-1.5]\square\) and \(\larger[-1.5]\Diamond\) as well as the co-implication connective from bi-intuitionistic logic.

5. Bi-intuitionistic linear temporal logic (\(\mathsf{biLTL}\)): a bi-intuitionistic version of linear temporal logic.

Apart from introducing new logics, namely \(\mathsf{biML}\) and \(\mathsf{biLTL}\), the main contributions of this thesis are threefold: semantic, syntactic and computational.

On the semantic side we study various classes of dynamic models which satisfy different confluence conditions and frame conditions. The former are interaction principles between \(\leq\) and \(R\), which play an important role in the study of intuitionistic modal logics. The latter are conditions placed on \(R\), such as transitivity. We establish expressivity results, and show that several logics satisfy the finite model property. The most important contribution is the proof of the finite model property for \(\mathsf{biML}\) and \(\mathsf{biLTL}\), which is shown via an intricate combinatorial analysis of the semantics by employing labelled and quasi models.

On the syntactic side, we develop several proof systems in form of Hilbert-style axiomatizations as well as cyclic and non-wellfounded sequent calculi. We show how to adapt classical techniques such as canonical model constructions and proof search arguments to obtain soundness and completeness results. In some cases, such as for \(\mathsf{IM}\) or for \(\mathsf{ICK}\), an adaption is relatively straightforward. For other cases, however, such as \(\mathsf{biLTL}\), adapting the classical techniques to obtain completeness is not possible and we are forced to develop different methods. We highlight the development of a sound and complete axiomatization for an extension of the language of \(\mathsf{iLTL}\) with the fixed point operator ‘henceforth’; a problem that has been open for several years.

Finally, on the computational side, we establish decidability and complexity results for the problem of checking validity for several intuitionistic dynamic logics. The most important results are, on the one hand, a precise complexity bound for \(\mathsf{ICK}\) over S5 models, and on the other hand, the proofs that \(\mathsf{biML}\) and \(\mathsf{biLTL}\) are decidable.

1.5 Structure of the Thesis and Sources of the Material↩︎

Chapter 2 serves as an introduction to the mathematical formalisms that are used throughout the thesis. In particular we formally introduce \(\mathsf{IPL}\) and \(\mathsf{IML}\), provide a brief introduction to proof theory and discuss fixed point operators. Furthermore the history of \(\mathsf{IPL}\) and \(\mathsf{IML}\) is discussed. Chapters 3 - 6 each study one of the five intuitionistic dynamic logics mentioned before. Chapters 3 - 5 are based on [39]–[41]; the first two are joint publications with Bahareh Afshari, Lide Grotenhuis and Graham E. Leigh and the last is a joint publication with Jan Rooduijn. Chapters [c: bi-int ml new] and 6 are based on [42], [43], both of which are joint publications with David Fernández-Duque and Brett McLean. A joint publication with Borja Sierra-Miranda and Thomas Studer [44] about non-wellfounded proof theory is not discussed in this thesis.

2 Preliminaries↩︎

This chapter introduces the logical systems upon which the thesis is built. We begin by setting up notational conventions and basic definitions. Then we formally introduce intuitionistic propositional logic, in particular its syntax and its semantics, which is defined over intuitionistic Kripke models. Moreover, we give a general definition of proof system and introduce a Hilbert-style axiomatization and a Gentzen-style sequent calculus for intuitionistic propositional logic; the axiomatizations and sequent calculi presented later on are based on these two systems. Afterwards we formally introduce intuitionistic modal logic, namely its syntax and its semantics, which is defined over dynamic models: extensions of intuitionistic Kripke models by a modal accessibility relation. Furthermore, we discuss a range of confluence conditions and frame conditions. Finally, we discuss fixed point operators and then finish the chapter with a historical overview of intuitionistic (modal) logic.

2.1 Basic Definitions↩︎

This section introduces the notation and the basic mathematical objects, such as partial functions or trees, used throughout the rest of the thesis.

We denote the set of natural numbers by \(\omega\) and write \(n < \omega\) to denote that \(n\) is a natural number. Given a set \(X\), the power set of \(X\) is denoted by \(\mathcal{P}(X)\) and the cardinality by \(\left|X\right|\).

2.1.1 Binary Relations↩︎

Given sets \(X\) and \(Y\) a binary relation is a subset \(R \subseteq X \times Y\) of the cartesian product of \(X\) and \(Y\). Given \(x \in X\) and \(y \in Y\) we write both \((x,y) \in R\) and \(x \mathrel{R}y\) to denote that \(x\) and \(y\) are related by \(R\). Moreover we denote by \(dom(R)\) the domain and by \(ran(R)\) the range of \(R\). Formally, \[\begin{align} dom(R) &\mathrel{\vcenter{:}}= \{ x \in X \mid \text{ there exists } y \in Y \text{ with } x \mathrel{R} y \};\\ ran(R) & \mathrel{\vcenter{:}}= \{ y \in Y \mid \text{ there exists } x \in X \text{ with } x \mathrel{R} y \}.\\ \end{align}\] If \(x \in dom(R)\) we write \(\exists{R(x)}\) and otherwise \(\nexists{R(x)}\). Given \(U \subseteq X\) and \(V \subseteq Y\), we write \[R{\upharpoonright}_{U \times V} \mathrel{\vcenter{:}}= \{(x,y) \in U \times V \mid (x,y) \in R\}\] for the restriction of \(R\) to \(U\) and \(V\). Given two binary relations \(R_1 \subseteq X \times Y\) and \(R_2 \subseteq Y \times Z\), the composition of \(R_1\) with \(R_2\) is denoted by \(R_2 \circ R_1\), formally \[R_2 \circ R_1 \mathrel{\vcenter{:}}= \{(x,z) \in X \times Z \mid \text{ there exists } y \in Y \text{ with } (x,y) \in R_1 \text{ and } (y,z) \in R_2\}.\]

We are interested in specific binary relations, which are introduced below.

We denote (partial) functions by \(f: X \longrightarrow Y\) and write \(f(x) = y\) instead of \(x \mathrel{f} y\). Functions are always assumed to be total; whenever a function is partial, we will explicitly say so.

Partial orders and well-orders are denoted by \(\leq\).¹ As usual, we write \(x < y\) if \(x \leq y\) and \(x \not = y\). Given a partial order \(\leq\) on \(X\), the tuple \((X, \leq)\) is called a poset. If \(\leq\) is a well-order on \(X\), then \((X, \leq)\) is called a well-ordered set. Given a poset \((X, \leq)\) and \(x \in X\), let \[\begin{align} x^\uparrow &\mathrel{\vcenter{:}}= \{ y \in X \mid x \leq y\}\\ x^\downarrow &\mathrel{\vcenter{:}}= \{ y \in X \mid y \leq x\}. \end{align}\] We call \(x^\uparrow\) the upset of \(x\) and \(x^\downarrow\) the downset of \(x\).

Equivalence relations are denoted by \(\sim\). If \(\sim\) is an equivalence relation on \(X\) and \(x \in X\), the equivalence class of \(x\) is given by \[[x] \mathrel{\vcenter{:}}= \{ y \in X \mid x \sim y\}.\]

The quotient of \(X\) under \(\sim\) is given by \[\frac{X}{\sim} \mathrel{\vcenter{:}}= \{[x] \mid x \in X\}.\]

2.1.2 Trees↩︎

Trees will be used primarily for studying formal proofs. We will usually be quite informal about the precise structure of a tree. Here, the definition of trees and related concepts are introduced.

Elements of \(T\) are called nodes and \(r\) is called the root. If \(s,t \in T\) with \(s < t\) and there does not exist an \(s' \in T\) with \(s < s' < t\), then \(s\) is called the parent of \(t\) and \(t\) is called a child of \(s\). If \(s < t\), then \(s\) is called an ancestor of \(t\) and \(t\) is called a descendant of \(s\). Nodes without children are called leafs. A path is a sequence of nodes \((t_i)_i\) such that for all \(i\) the node \(t_{i+1}\) is a child of \(t_i\). Given a finite path \((t_i)_{i \leq n}\) for \(n < \omega\), the length \(l((t_i)_{i \leq n})\) of \((t_i)_{i \leq n}\) is defined to be \(l((t_i)_{i \leq n}) \mathrel{\vcenter{:}}= n\). A branch is a path starting at the root which is either infinite or ends in a leaf. A tree \(\mathcal{T}=(T, \leq, r)\) is finite if \(T\) is finite and infinite otherwise. Given a finite tree \(\mathcal{T}\), the height \(h(\mathcal{T})\) of \(\mathcal{T}\) is defined to be \(h(\mathcal{T}) \mathrel{\vcenter{:}}= max\{l(\rho) \mid \rho \text{ is a branch of } \mathcal{T}\}\). A tree \(\mathcal{T}\) is finitely branching if every node of \(\mathcal{T}\) has only finitely many children. The following is a well-known result about finitely branching trees.

A labelled tree is a tree together with a labelling function which assigns to each node a label.

The height of a finite labelled tree \((T, \leq, r, \ell)\) is the height of \((T, \leq, r)\). Finally, the following notion of subtree will be used repeatedly.

2.2 Intuitionistic Logic↩︎

Every intuitionistic dynamic logic studied in this thesis is an extension of intuitionistic propositional logic with modalities and fixed point operators. We only study propositional logics, therefore we usually call intuitionistic propositional logic simply intuitionistic logic. This section introduces the syntax and semantics of intuitionistic logic (\(\mathsf{IPL}\)). An overview of the history of intuitionistic logic and its many interpretations is deferred to Section 2.6.

The language \(\mathcal{L}_\mathsf{IPL}\) of \(\mathsf{IPL}\) consists of a countable set of atomic propositions \(\mathsf{Prop}\), the constant falsum \(\bot\), the connectives conjunction \(\wedge\), disjunction \(\vee\) and implication \(\rightarrow\) as well as brackets \((\) and \()\). Formulas of \(\mathcal{L}_\mathsf{IPL}\) are given by the following grammar in Backus–Naur form: \[\varphi ::= \bot \, \lvert \, p \, \lvert \, (\varphi \wedge \varphi) \, \lvert \, (\varphi \vee \varphi) \, \lvert \, (\varphi \rightarrow \varphi)\] where \(p \in \mathsf{Prop}\). Formulas (in every system studied subsequently) are always denoted by Greek letters \(\varphi, \psi, \chi\) and \(\gamma\), while propositions are denoted by Latin letters \(p,q,r\). Subscripts are also used such as \(\varphi_1, \varphi_2\) and so on. We write \(\varphi \in \mathcal{L}_\mathsf{IPL}\) to denote that \(\varphi\) is a formula of \(\mathcal{L}_\mathsf{IPL}\). We omit outermost brackets when displaying formulas and simply write e.g. \(\varphi \wedge \psi\) instead of \((\varphi \wedge \psi)\). In fact, brackets will only be used to give unique precedence of the connectives in longer formulas. The connectives negation \(\neg\) and if and only if \(\leftrightarrow\), as well as the constant verum \(\top\) are treated as defined connectives, where \(\top \mathrel{\vcenter{:}}= \bot \rightarrow \bot\), \(\neg \varphi \mathrel{\vcenter{:}}= \varphi \rightarrow \bot\) and \(\varphi \leftrightarrow \psi \mathrel{\vcenter{:}}= (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)\).

Formulas of \(\mathsf{IPL}\) are evaluated on intuitionistic Kripke models.

Intuitionistic Kripke models are usually simply called Kripke models and denoted by \(\mathcal{M}\) and \(\mathcal{N}\). Elements of \(W\) are called worlds or (information) states and are denoted by \(w,v,u\) and so on. The relation \(\leq\) is called the intuitionistic order and if \(w \leq v\), then we call \(v\) an intuitionistic successor of \(w\). The function \(V\) is called a valuation. A tuple \((\mathcal{M}, w)\) where \(\mathcal{M}=(W, \leq, V)\) is a Kripke model and \(w \in W\) is called a pointed Kripke model.

A formula \(\varphi\) is called satisfiable over the class of Kripke models if there exists a Kripke model \(\mathcal{M}=(W, \leq, V)\) and a world \(w \in W\) with \(\mathcal{M},w \models \varphi\) and unsatisfiable otherwise. Furthermore, \(\varphi\) is called valid over the class of Kripke models if \(\mathcal{M}, w \models \varphi\) for all Kripke models \(\mathcal{M}=(W, \leq, R)\) and all worlds \(w \in W\) and falsifiable otherwise.

For the defined connectives a simple computation shows that the following truth conditions hold. The proof is omitted.

A defining property of Kripke semantics for intuitionistic logic is the Monotonicity Lemma, which states that the truth relation is monotone in \(\leq\).

We finish the section by stating two properties of the Kripke semantics for intuitionistic logic. Recall that the law of excluded middle states that for any proposition \(p\) the formula \(p \vee \neg p\) is valid.

A Kripke model \(\mathcal{M}=(W, \leq, V)\) is finite if \(W\) is a finite set. Intuitionistic logic satisfies the finite model property if every falsifiable formula can be falsified in a finite Kripke model. The following is for example proven in [45].

2.3 Proof systems↩︎

An important tool used in our study of intuitionistic dynamic logics are proof systems. Intuitively, a proof system consists of a set of axioms - formulas assumed to be true without proof - and a set of inference rules - rules that govern how to prove new formulas from axioms and formulas which have already been proven. The rules of a proof system do not refer to the semantics of the logic. Instead they are purely mechanical and dictate how to manipulate the syntactic structure of formulas to obtain new ones. Accordingly, just as the formal semantics of a logic determine the set of valid formulas, a proof system determines the set of provable formulas. The bridge between the semantic and syntactic realm are soundness and completeness proofs: soundness establishes that every provable formula is valid while completeness establishes that every valid formula is provable.

We will study two types of proof systems: (Hilbert-style) axiomatizations and (Gentzen-style) sequent calculi. Regarding the sequent calculi, we will in particular study non-wellfounded and cyclic proofs. This section introduces the basic definitions shared by all systems encountered in the thesis. Afterwards we introduce an axiomatization and a sequent calculus for \(\mathsf{IPL}\). A discussion of non-wellfounded and cyclic proofs is deferred to Chapter 3.

2.3.1 General Definitions↩︎

Some proof systems manipulate formulas while others manipulate more complicated mathematical structures. Therefore we give a general definition of inference rules and proof systems relative to an arbitrary set \(\mathcal{S}\).

Given a rule instance \(\langle s, \langle s_1, \ldots, s_n\rangle \rangle\), its arity is \(n\). Rule instances with arity \(0\) are called axioms. A rule instance \(\langle s, \langle s_1, \ldots, s_n \rangle \rangle \in \mathsf{r}\) is depicted as \[\infer[\mathsf{r}]{s}{s_1 & \ldots & s_n}\] with the intended reading that if the premises \(s_1, \ldots, s_n\) are obtained, then we can derive the conclusion \(s\). Inference rules where each rule instance is an axiom are called axiom schemes. Inference rules that are not axiom schemes are called proper. We will mostly consider inference rules where each rule instance has the same arity.³ Such inference rules will be depicted schematically, i.e. we depict the rule by providing one rule instance from which all other instances can be obtained via uniform substitution.

The two types of proof systems studied in this thesis are axiomatizations and sequent calculi. These two types of systems differ with respect to the set of elements they manipulate. Axiomatizations manipulate formulas of a logical language (e.g. \(\mathcal{L}_\mathsf{IPL}\)). Sequent calculi, on the other hand, manipulate so called sequents, which have more structure.

2.3.2 An Axiomatization for Intuitionistic Logic↩︎

This subsection introduces an axiomatization for intuitionistic logic. The axiomatization manipulates \(\mathcal{L}_\mathsf{IPL}\)-formulas. An axiomatization typically consist of a list of axiom schemes together with a few proper inference rules. The presented system is taken from [46].

The rules \(\mathsf{1}\) – \(\mathsf{8}\) are axiom schemes. Instead of writing for example \[\infer[\mathsf{1}]{\varphi \rightarrow (\psi \rightarrow \varphi)}{}\] for an axiom, we prefer to simply write \(\varphi \rightarrow (\psi \rightarrow \varphi)\) when we list the axiomatization to clearly distinguish axiom schemes from proper inference rules. The rule \(\mathsf{MP}\) is the modus ponens rule, which will be featured in all axiomatizations considered in this thesis. It states that from \(\varphi\) and \(\varphi \rightarrow \psi\) we can derive \(\psi\). We implicitly assume that every inference rule is closed under uniform substitution. We will therefore not explicitly add a substitution rule to our systems. In other words, each axiom scheme and inference rule can be instantiated by uniformly substituting the formulas displayed in Table 1 by other formulas. Formal proofs in an axiomatization are called derivations.

If there exists a derivation of \(\varphi\), then we write \(\vdash_\mathrm{IPL_H} \varphi\) and say that \(\varphi\) is \(\mathrm{IPL_H}\)-derivable. If the proof system is clear from context, we omit the mention of \(\mathrm{IPL_H}\).

We will usually not display derivations as trees and instead simply explain which axioms to choose and what rules to apply in order to get the desired result. The following example illustrates this.

The axiomatization \(\mathrm{IPL_H}\) is sound and complete with respect to the class of intuitionistic Kripke models.

Soundness is established by a standard induction on the height of derivations. Completeness is established by a canonical model construction. For a proof, see [46].

For example, in the language extending \(\mathcal{L}_\mathsf{IPL}\) with \(\larger[-1.5]\square\) we have that \(\larger[-1.5]\square\varphi \rightarrow (\larger[-1.5]\square\psi \rightarrow \larger[-1.5]\square\varphi)\) is an intuitionistic tautology, since \(p \rightarrow (q \rightarrow p)\) is an axiom and we obtain the formula by substituting \(p\) by \(\larger[-1.5]\square\varphi\) and \(q\) by \(\larger[-1.5]\square\psi\).

2.3.3 A Sequent Calculus for Intuitionistic Logic↩︎

Hilbert-style axiomatizations provide a neat way to capture the validites of a logic. However, Examples 2.1 and 2.2 hint at a general problem of such a formalism: the presence of the modus ponens rule makes it difficult to construct a proof for a given formula, since in order to prove a formula, we have to guess the correct instances of axiom schemes and then apply modus ponens. To circumvent this issue, we will consider sequent calculi, which manipulate sequents and are generally much nicer to work with. Here, we introduce a sequent calculus for \(\mathsf{IPL}\) which will be the foundation for all sequent calculi studied later on. The system is taken from [47].

We denote sequents by \(\sigma\) and use \(\Gamma_\sigma\) to refer to the left side of \(\sigma\) and \(\Delta_\sigma\) to refer to the right side. As usual \(\Gamma, \varphi\) denotes \(\Gamma \cup \{\varphi\}\).

The interpretation of a sequent \(\sigma\) is the formula \[\sigma^I \mathrel{\vcenter{:}}= \bigwedge \Gamma_\sigma \rightarrow \bigvee \Delta_\sigma\]

Given a pointed model \((\mathcal{M}, w)\), we write \(\mathcal{M}, w \models \sigma\) if and only if \(\mathcal{M}, w \models \sigma^I\). Note that sequents are multi-conclusion, i.e. \(\Delta\) might contain more than one formula. The more standard calculus for \(\mathsf{IPL}\) employs single-conclusion sequents (see e.g. [47]), however as we will later explain, for our purposes multi-conclusion sequents are better suited.

The rules \(\mathsf{id}\) and \(\bot\) are axioms. All other rules are standard inference rules from classical propositional logic, with the exception of \({\rightarrow} \mathsf{R}\), which has a single-conclusion premise. This restriction ensures that the law of excluded middle is not derivable. Note that commas in sequents are interpreted as conjunctions on the left side of the sequent arrow and as disjunctions on the right side, which explains the rules for conjunction and disjunction. In each inference rule, the distinguished formula in the conclusion is called principal and the distinguished formulas in the premises are called residual. For example, in the rule \({\wedge}\mathsf{L}\) the principal formula is \(\varphi \wedge \psi\) and the residual formulas are \(\varphi\) and \(\psi\). All other formulas are called side formulas.

If there is a proof of \(\sigma\), we write \(\vdash_\mathrm{IPL_G} \sigma\) and say that \(\sigma\) is \(\mathrm{IPL_G}\)-provable. We omit the mention of \(\mathrm{IPL_G}\) if the proof system is clear from context. If \(\varphi\) is a formula, then \(\varphi\) is provable if and only if \(\Rightarrow \varphi\) is provable.

One of the advantages of using the sequent calculus \(\mathrm{IPL_G}\) instead of the axiomatization \(\mathrm{IPL_H}\) stems from the fact that the former allows for upwards proof search: given a sequent \(\sigma\) we find a proof by writing \(\sigma\) at the root and then apply rules upwards until axioms are encountered. The rules of \(\mathrm{IPL_G}\) are analytic: all formulas occurring in the premises of a rule are subformulas of formulas in the conclusion. Hence, in a proof of \(\sigma\), only finitely many formulas and thus finitely many different sequents can occur, which implies that there are only finitely many sensible candidates for a proof to check.⁴ Note that this is not possible for a rule like modus ponens: in order to derive \(\psi\), we have to guess a formula \(\varphi\) so that we can apply modus ponens to \(\varphi\) and \(\varphi \rightarrow \psi\) and there are infinitely many candidates for \(\varphi\). There are thus two ways to read the rules of a sequent calculus: downwards (i.e. going from premises to the conclusion) and upwards (i.e. going from the conclusion to the premises). The first way is consistent with the idea that rules preserve validity: if the premises are valid, then the conclusion is valid too. When thinking of mathematical proofs, the downwards reading is correct, since proofs are arguments starting with axioms and ending with the conclusion that is supposed to be proven. However, when performing proof search, we will read rules upwards instead. In this reading, we think of rules as preserving falsifiability: if the conclusion is falsifiable, then so is at least one of the premises. Since proofs in a sequent calculus are generally constructed by reading rules upwards and this reading makes it also easier to understand a proof, we will usually consider the upwards reading interpretation. However, we will always make it clear when applying rules whether we think of them as upwards or downwards.

Soundness is established by a standard induction on the height of proofs. Completeness can be established in two ways: either by a canonical model construction or by embedding the axiomatization \(\mathrm{IPL_H}\) into \(\mathrm{IPL_G}\). For the latter we are required to extend the sequent calculus with the cut rule \[\infer[\mathsf{cut}]{\Gamma \Rightarrow \Delta}{\Gamma, \varphi \Rightarrow \Delta & \Gamma \Rightarrow \varphi, \Delta}\] where \(\varphi\) is any formula, in order to derive \(\mathsf{MP}\). Note that the cut rule is not analytic, since \(\varphi\) does not need to be a subformula of a formula in the conclusion. Thus to obtain completeness for \(\mathrm{IPL_G}\) and to keep the property of analyticity, after embedding \(\mathrm{IPL_H}\) into \(\mathrm{IPL_G}\) plus the cut rule, we must show that the cut rule can be eliminated without altering the set of provable sequents. This elimination process is called cut elimination and can be done for \(\mathrm{IPL_G}\), see e.g. [47]. For more details about sequent calculi and the structural properties of \(\mathrm{IPL_G}\), the reader is referred to [47].

2.4 Intuitionistic Modal Logic↩︎

Intuitionistic modal logic (\(\mathsf{IML}\)) refers to the extension of \(\mathsf{IPL}\) by modalities from modal logic. Traditionally, one considers the modalities \(\larger[-1.5]\square\) and \(\larger[-1.5]\Diamond\), whose interpretation is as follows: a formula \(\larger[-1.5]\square\varphi\) is read as \(\varphi\) is necessarily true and a formula \(\larger[-1.5]\Diamond\varphi\) is read as \(\varphi\) is possibly true. Many other interpretations for \(\larger[-1.5]\square\) and \(\larger[-1.5]\Diamond\) have been proposed and studied in the literature and some will be encountered in this thesis. In particular, in epistemic logic the modality \(\larger[-1.5]\square\) is read as a knowledge operator: \(\larger[-1.5]\square\varphi\) means that \(\varphi\) is known. In linear temporal logic, both \(\larger[-1.5]\square\) and \(\larger[-1.5]\Diamond\) correspond to the temporal modality \(\mathbin{{\bigcirc}}\), where \(\mathbin{{\bigcirc}}\varphi\) is read as \(\varphi\) is true in the next time step. In contrast to classical modal logic, the equivalence \[\larger[-1.5]\square\varphi \leftrightarrow \neg \larger[-1.5]\Diamond\neg \varphi\] is usually not taken to be valid in intuitionistic modal logics (e.g. Simpson’s fifth criterion for an intuitionistic modal logic is that \(\larger[-1.5]\square\) and \(\larger[-1.5]\Diamond\) are independent [7]). Nevertheless, intuitionistic modal logics satisfying the equivalence above have been proposed, for example by Bull [48]. This section introduces the syntax and semantics of intuitionistic modal logic. Furthermore, we discuss confluence conditions and frame conditions for the models of \(\mathsf{IML}\). A brief overview of the history of intuitionistic modal logic is deferred to Section 2.6.

The language \(\mathcal{L}_\mathsf{IML}\) of intuitionistic modal logic extends \(\mathcal{L}_\mathsf{IPL}\) by the modal operators box \(\larger[-1.5]\square\) and diamond \(\larger[-1.5]\Diamond\). Formulas of \(\mathcal{L}_\mathsf{IML}\) are given by the following grammar in Backus–Naur form: \[\varphi ::= \bot \, \lvert \, p \, \lvert \, \varphi \wedge \varphi \, \lvert \, \varphi \vee \varphi \, \lvert \, \varphi \rightarrow \varphi \, \lvert \, \larger[-1.5]\square\varphi \, \lvert \, \larger[-1.5]\Diamond\varphi.\] where \(p \in \mathsf{Prop}\). The modal operator \(\larger[-1.5]\square^k\) for \(k < \omega\) is defined inductively by \(\larger[-1.5]\square^0 \varphi \mathrel{\vcenter{:}}= \varphi\) and \(\larger[-1.5]\square^{k+1} \varphi \mathrel{\vcenter{:}}= \larger[-1.5]\square\larger[-1.5]\square^k \varphi\). Similarly, the modal operator \(\larger[-1.5]\Diamond^k\) is defined by \(\larger[-1.5]\Diamond^0 \varphi \mathrel{\vcenter{:}}= \varphi\) and \(\larger[-1.5]\Diamond^{k+1} \varphi \mathrel{\vcenter{:}}= \larger[-1.5]\Diamond\larger[-1.5]\Diamond^k \varphi\).

Formulas of intuitionistic modal logic are evaluated on intuitionistic Kripke models extended by an additional binary relation to evaluate the modalities. The resulting models are called dynamic models.

The relation \(R\) is called the modal (accessibility) relation. If \(w \mathrel{R}v\), then \(v\) is called a modal successor of \(w\). We define the relation \(R^k \subseteq W \times W\) for \(k < \omega\) inductively as follows. For all \(w,v \in W\), \(w \mathrel{R}^0 v\) if \(w=v\). Moreover, \(w \mathrel{R}^{k+1} v\) if there exists \(u \in W\) with \(w \mathrel{R}u\) and \(u \mathrel{R}^k v\).

Let \(\mathcal{C}\) be a class of dynamic models and \(\varphi\) a formula. Then \(\varphi\) is satisfiable over \(\mathcal{C}\) if there exists a dynamic model \(\mathcal{M}\in \mathcal{C}\) and a world \(w\) such that \(\mathcal{M}, w \models \varphi\), and unsatisfiable otherwise. Moreover, \(\varphi\) is valid over \(\mathcal{C}\) if for any dynamic model \(\mathcal{M}\in \mathcal{C}\) and any world \(w\), \(\mathcal{M}, w \models \varphi\), and falsifiable otherwise.

Note that the modalities are evaluated using both \(\leq\) and \(R\). This deviates from the evaluation of modalities in classical modal logic where \(w \models \larger[-1.5]\square\varphi\) if and only if for all \(v\) if \(w \mathrel{R}v\), then \(v \models \varphi\), and \(w \models \larger[-1.5]\Diamond\varphi\) if and only if there exists \(v\) with \(w \mathrel{R}v\) and \(v \models \varphi\). This deviation is necessary since the classical truth conditions do not preserve the monotonicity property of intuitionistic logic: if for example \(w \models \larger[-1.5]\square\varphi\) and \(w \leq v\), then there is no reason that \(v \models \larger[-1.5]\square\varphi\), since the modal successors of \(w\) and \(v\) might be unrelated to one another. To understand the importance of this, observe that a semantics without the monotonicity property will not yield a ‘logic’ with the most basic property: closure under substitutions.

By using the intuitionistic truth conditions for the modalities instead, monotonicity of the semantics is preserved, as illustrated in the following lemma.

In the definition of a dynamic model the intuitionstic order \(\leq\) and the modal relation \(R\) are unrelated to one another. We now turn our attention to confluence conditions: interaction principles between \(\leq\) and \(R\) that will be of recurring importance in this thesis. We give a general definition.

We will usually consider dynamic models \(\mathcal{M}=(W, \leq, R, V)\) where \(R\) satisfies some confluence condition C for \((\leq, \leq)\). In this case, we simply call \(R\) C-confluent. However, we will also study confluent relations between different posets in Chapter [c: bi-int ml new] and Chapter 6.

One reason why we are interested in confluence conditions is that in forth-up and forth-down confluent dynamic models, the intuitionistic truth conditions for the modalities coincide with the classical truth conditions; the latter can thus be used for convenience. Other reasons will be presented in later chapters. The following is proven in [49].

We are also interested in dynamic models which satisfy certain frame conditions.

In Chapter 5 and Chapter 6 we will study intuitionistic linear temporal logic, where formulas are evaluated over dynamic models which are total functional. The following lemma is straightforward to check, since in total functional models every world has a unique modal successor. The proof is omitted.

Given this lemma, we will call total functional models which are forth-up or forth-down confluent simply forward confluent.

2.5 Fixed Point Operators↩︎

Intuitionistic dynamic logics are extensions of intuitionistic modal logics with fixed point operators. Intuitively, fixed point operators express infinite statements, such as ‘in all future time steps, \(\varphi\) is true’. In this section we briefly explain why such operators are called fixed point operators. Strictly speaking, the theory explained in this section is not needed for understanding the rest of the thesis. However, we believe that it is informative to understand the concept of a fixed point operator, as it relates the presented logics to one another and also to other modal fixed point logics. We do not give a general definition, but instead explain the concept with an example.

Consider a dynamic model of the form \(\mathcal{M}=(W, \leq, R, V)\), where \(R\) is triangle confluent. Consider the language extending \(\mathcal{L}_\mathsf{IPL}\) by the modality \(\larger[-1.5]\square\) as well as a unary operator \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\) which is characterized semantically as \(\mathcal{M}, w \models \ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) if and only if for all \(v \in W\) if \(w \mathrel{R}^* v\), then \(\mathcal{M}, v \models \varphi\) where \(R^*\) is the reflexive transitive closure of \(R\). In other words, \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) is true at \(w\) if \(\varphi\) is true in any world \(v\) reachable from \(w\) over finitely many modal steps. Equivalently, \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) is equivalent to the infinite conjunction \[\bigwedge_{n < \omega} \larger[-1.5]\square^n \varphi.\] The operator \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\) is called a fixed point operator, namely \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) is the greatest fixed point of the propositional function \(x \mapsto \varphi \wedge \larger[-1.5]\squarex\). Let us make precise what is meant by this.

Given a formula \(\varphi\), let \[\llbracket \varphi \rrbracket_\mathcal{M}\mathrel{\vcenter{:}}= \{ w \in W \mid \mathcal{M}, w \models \varphi\}\] be the truth set of \(\varphi\) in \(\mathcal{M}\). Let \(U \subseteq W\) and \(p \in \mathsf{Prop}\) be a proposition not occurring in \(\varphi\). Let \(U^\uparrow\) be the least upwards closed set containing U. Define \(V_U^p: W \longrightarrow \mathcal{P}(\mathsf{Prop})\) as follows: \[V_U^p(w) \mathrel{\vcenter{:}}= \begin{cases} V(w) \cup \{p\} & \text{ if } w\in U^\uparrow \\ V(w) \setminus \{p\} & \text{ otherwise.} \end{cases}\] In other words, the valuation \(V_U^p\) changes the valuation \(V\) by making \(p\) true at the worlds in \(U^\uparrow\) and nowhere else. For any other proposition \(q\), \(q \in V(w)\) if and only if \(q \in V_U^P(w)\). Let \(\mathcal{M}_U^p\) denote the dynamic model \((W, \leq, R, V_U^p)\). Now consider the formula \(\psi = \varphi \wedge \larger[-1.5]\squarep\). This formula induces a function \(f_\psi: \mathcal{P}(W) \longrightarrow \mathcal{P}(W)\) given by \[U \mapsto \llbracket \varphi \wedge \larger[-1.5]\squarep\rrbracket_{\mathcal{M}_U^p}.\]

Given a function \(S: \mathcal{P}(W) \longrightarrow \mathcal{P}(W)\), a fixed point of \(S\) is a subset \(U \subseteq W\) such that \(S(U) = U\). Moreover, \(U\) is the greatest fixed point of \(S\) if for any other fixed point \(U'\) of \(S\) holds that \(U' \subseteq U\) and \(U\) is the least fixed point of \(S\) if for any other fixed point \(U'\) of \(S\) holds that \(U \subseteq U'\). If \(S\) is monotone on \(\mathcal{P}(W)\), meaning that whenever \(U \subseteq U'\) we have \(S(U) \subseteq S(U')\), then the Knaster–Tarski Theorem [50] guarantees that \(S\) has a least and a greatest fixed point.

It is not hard to check that the function \(f_\psi\) is monotone on \(\mathcal{P}(W)\): we have \(\llbracket \varphi \wedge \larger[-1.5]\squarep \rrbracket_{\mathcal{M}} = \llbracket \varphi \rrbracket_\mathcal{M}\cap \llbracket {\larger[-1.5]\squarep} \rrbracket_\mathcal{M}\). Since \(p\) does not occur in \(\varphi\), for any \(U \subseteq U'\), \(\llbracket \varphi \rrbracket_{\mathcal{M}_U^p} = \llbracket \varphi \rrbracket_{\mathcal{M}_{U'}^p}\). Furthermore, clearly \(\llbracket \larger[-1.5]\squarep \rrbracket_{\mathcal{M}_U^p} \subseteq \llbracket \larger[-1.5]\squarep \rrbracket_{\mathcal{M}_{U'}^p}\). Hence \(f_\psi(U) \subseteq f_\psi(U')\). By the Knaster–Tarski Theorem \(f_\psi\) has a greatest fixed point \(U\). One can now show that the greatest fixed point of \(f_\psi\) is exactly the set \(\llbracket \ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi \rrbracket_\mathcal{M}\); for a proof, see [26]. This is the precise meaning behind the statement that \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) is the greatest fixed point of the function \(x \mapsto \varphi \wedge \larger[-1.5]\squarex\).

This construction is not dependent on \(\psi\). For any formula \(\gamma\) we can consider the function \(f_\gamma\) induced by \(\gamma\) and if \(f_\gamma\) is monotone, then there exist the least and greatest fixed points. A defining property of all intuitionistic dynamic logics studied in this thesis is that they are extensions with fixed point operators for specific functions. This is not a necessary restriction; instead we could extend the language of \(\mathsf{IML}\) by operators \(\mu\) and \(\nu\) which are applicable to any formula and define the truth set of a formula \(\mu x. \varphi\) as the least fixed point of the function \(f_\varphi\) induced by \(\varphi\) and similarly, \(\nu x. \varphi\) as the greatest fixed point.⁵ This results in an expressive logical system which is capable of expressing least and greatest fixed points of every monotone function, as opposed to only some. This logic is called intuitionistic modal \(\mu\)-calculus, see Pacheco [30]. For an introduction to modal fixed point logics in general, we refer the reader to the excellent article about the classical modal \(\mu\)-calculus by Stirling [13].

2.6 Historical Remarks↩︎

We finish this chapter by providing a brief historical overview of intuitionistic logic and intuitionistic modal logic.

2.6.1 Intuitionism and Intuitionistic Logic↩︎

The origin of intuitionistic logic goes back to intuitionism, one of the main positions in philosophy of mathematics developed by Dutch mathematician Brouwer [51]. Classical mathematics (at least implicitly) assumes an objective notion of truth: every well-formed mathematical statement such as ‘\(2+2= 4\)’ is either true or false. A common interpretation in philosophy is that truth is a relationship between language and reality [52]. For example, the sentence ‘Young Boys is the best football club in Bern’ is true due to the objective reality regarding football clubs in Bern. But what is the objective reality of the statement ‘\(2+2 = 4\)’ which is regarded to be true in mathematics? The realist position, which originates in the work of Plato, claims that there are objectively existing mathematical objects, such as natural numbers. In other words, there exists a universe of mathematical objects and the statement ‘\(2+2 = 4\)’ expresses the objective reality in this universe and is thus true. Intuitionism rejects the realist position and instead claims that mathematics is a mental activity and mathematical objects exist insofar they have been constructed in the mind of the mathematician. Similarly, proofs are mental constructions and a mathematical statement is true insofar it has been proven. As a consequence, intuitionism rejects indirect proofs which are often used in classical mathematics. For example, an existential statement \(\exists x. \varphi(x)\) is typically proven in classical mathematics by deriving a contradiction from \(\forall x. \neg \varphi(x)\). But such an indirect proof does not result in the construction of an object \(c\) which satisfies \(\varphi(c)\). Instead the indirect proof assumes that the statement \(\exists x. \varphi(x)\) is either true or false, thus deriving a contradiction from its negation \(\forall x. \neg \varphi(x)\) means that \(\exists x. \varphi(x)\) must be true. In intuitionistic mathematics, such an existential statement is proven constructively by constructing the object \(c\) and providing a constructive proof of \(\varphi(c)\). Negations of statements are also treated differently in intuitionistic mathematics. A proof of \(\neg \varphi\) is a proof that \(\varphi\) cannot be proven. Under this interpretation the law of excluded middle does not hold: in classical mathematics \(p \vee \neg p\) is always true since either \(p\) is true or \(p\) is false, in which case \(\neg p\) is true; in intuitionistic mathematics any statement \(p\) is either proven or not proven, but the lack of a proof for \(p\) does not imply that \(p\) cannot be proven, but rather that no proof for \(p\) has been constructed so far. Thus if \(p\) formalizes any unresolved mathematical conjecture, such as the Goldbach conjecture, there is no proof of \(p \vee \neg p\) and so the law of excluded middle fails. This example shows that intuitionistic mathematics uses different logical reasoning principles than classical mathematics. In 1930, Brouwer’s student Heyting isolated the acceptable reasoning principles of intuitionistic mathematics in a formal logical system, leading to the development of intuitionistic logic [1]–[3]. Since then, intuitionistic logic has developed into arguably one of the most successful logical systems, partly due to the following two reasons. First, it is generally accepted that intuitionistic logic succeeded in capturing intuitionistic reasoning and has thus fulfilled its philosophical purpose. Second, alternative interpretations of intuitionistic logic have emerged, which deviate from the original interpretation regarding intuitionism. Among those are interpretations based on computation, topology or information. For example, the Curry–Howard isomorphism relates, roughly speaking, proofs (in some formal proof system for intuitionistic logic) with programs (in some formal model of computation), illustrating a close connection between intuitionistic proofs and computation [53]. This close relation is also illustrated by the fact that many foundational systems for computer science are based on intuitionistic logic [46]. The interpretation of intuitionistic logic guiding this thesis is based on information. As outlined in Chapter 1, we consider intuitionistic logic as a logic to reason about information and information change. This interpretation goes back to Kripke [5], who introduced intuitionistic Kripke models for intuitionistic logic in 1965. As we have seen, these models can be regarded as information orderings and the evaluation of implications as expressing consequences of gaining information. Originally, Kripke provided an interpretation of his semantics as a way to capture the intuitionistic idea that mathematical statements are true if proven and false if proven to be unprovable. The worlds \(w\) of an intuitionistic Kripke model are thought to be information states containing all mathematical theorems which have been proven up to a certain time point. If \(w \leq v\), then \(v\) is thought of as an information state at a later time point obtained by adding more theorems that have been proven in the meantime. If \(w \not \models \varphi\), then \(\varphi\) is not thought to be refuted, but simply to not (yet) been proven. The truth relation should thus be understood as expressing whether a formula has been proven at this point or not. If \(w \models \neg \varphi\), then \(\varphi\) has been proven to be unprovable, implying that for any extension of \(w\), \(\varphi\) cannot be true. Kripke semantics thus provide an intuitive interpretation of intuitionistic logic and are furthermore natural to work with mathematically. However, it should be noted that they are not entirely satisfactory from the point of view of intuitionism: the interpretation of formulas on Kripke models does not refer to the notion of proof directly nor to the idea of constructions; moreover while we have seen that the proof systems of intuitionistic logic presented in Section 2.3 are sound and complete with respect to the class of Kripke models, the completeness proofs require a classical meta theory and are thus not intuitionistically acceptable [7].

For an introduction to intuitionism, we refer the reader to [54]. For a detailed account of the history of intuitionism and constructivism, see [55]. For a detailed introduction to the mathematical theory of intuitionistic logic, see [45], [46].

2.6.2 Intuitionistic Modal Logic↩︎

The modern origin of modal logic arguably goes back to the seminal work of Lewis [56] in 1918, who studied logics of strict implications. After the development of intuitionistic logic by Heyting, both logics were studied independently for several decades. The earliest combination of intuitionistic logic and modal logic is found in the work of Fitch [6] in 1948; however, it was the invention of Kripke semantics for modal logic [57] and for intuitionistic logic [5] by Kripke which laid the foundation for studying intuitionistic modal logic. In the 1980’s, Plotkin and Stirling [58], Ewald [59] and Fischer-Servi [60] independently introduced birelational semantics for intuitionistic modal logic by combining the two types of Kripke models, resulting in the development of the structures that we call dynamic models in this thesis. What followed was the development of a sheer bewildering amount of different intuitionistic modal logics, which differ semantically by the confluence conditions imposed on the dynamic models used for their evaluation. Roughly, these logics fall into two camps: constructive modal logics such as the systems introduced by Fitch [6] and Wijesekera [61] built for modelling computational aspects such as staged computation [11], and intuitionistic modal logics such as the systems by Fischer-Servi [60] and Plotkin and Stirling [58] aimed at capturing an intuitionistic meta reading of modalities and Kripke semantics. In his influential PhD thesis, Simpson [7] set up six criteria that an intuitionistic modal logic should satisfy to be classified as ‘intuitionistic’; one criteria is that there should be an intuitionistically comprehensible explanation of the modalities [7]. Simpson achieves this by providing a translation of intuitionistic modal logic into intuitionistic first-order logic - akin to the translation of modal logic into classical first-order logic - which can then be used as a formalized meta theory. The resulting logic turns out to be \(\mathsf{IK}\), which is semantically obtained by considering all validities over dynamic models satisfying forth-up and back-up confluence.

The restriction to dynamic models satisfying confluence conditions substantially increases the mathematical difficulty of the resulting logics. For example, the logic \(\mathsf{IS4}\) - an intuitionistic version of the modal logic \(\mathsf{S4}\) which satisfies the six criteria posed by Simpson - has only recently been proven to be decidable [62] and the presented proof is highly non-trivial. On the other hand, weaker logics obtained by either not considering any confluence conditions or by considering a restricted language behave more similar to classical modal logics and are generally easier to deal with, see e.g. [25].

3 Intuitionistic Master Modality↩︎

3.1 Introduction↩︎

This chapter introduces a simple intuitionistic dynamic logic called intuitionistic master modality (\(\mathsf{IM}\)). The language of \(\mathsf{IM}\) extends \(\mathcal{L}_\mathsf{IPL}\) by the modality \(\larger[-1.5]\square\) and the fixed point operator \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\) called the master modality, which we encountered in Section 2.5. The modality \(\larger[-1.5]\Diamond\) is not present in the language. Intuitively, \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) expresses that \(\varphi\) is true in any world of a dynamic model reachable from the current world over a finite (but arbitrary) number of modal steps. Thus \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) is true if \(\larger[-1.5]\square^n \varphi\) is true for any natural number \(n\) and it is characterized as the greatest fixed point of the propositional function \(x \mapsto \varphi \wedge \larger[-1.5]\squarex\). Given the interpretation that intuitionistic modal logic reasons about information updates, a formula \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) expresses that \(\varphi\) remains true under any number of information updates. The goal of this chapter is to study the mathematical theory of \(\mathsf{IM}\); in particular the expressivity of its language and its proof theory.

To the best of our knowledge, this work constitutes the first mathematical investigation of \(\mathsf{IM}\). It is worth noting, however, that a multi-modal variant of \(\mathsf{IM}\), known as intuitionistic common knowledge logic (\(\mathsf{ICK}\)), was previously introduced and studied by Jäger and Marti. [25], [27]. Classical versions of \(\mathsf{IM}\) have also been studied extensively, see e.g. [63]. Originally, one of our main motivations to study \(\mathsf{IM}\) was the interpretation of \(\mathsf{IM}\) as an intuitionistic linear temporal logic. To that end formulas are evaluated on dynamic models where the modal relation is a function modeling time. Such models are called functional models. In difference to stronger temporal logics such as \(\mathsf{iLTL}\), which will be studied in Chapter 5, the functional models of \(\mathsf{IM}\) do not satisfy any confluence conditions. The modality \(\larger[-1.5]\square\) is then interpreted as a temporal ‘next’ operator and the master modality as a temporal ‘henceforth’, i.e. \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) is true if \(\varphi\) is true in any future time step. As it turns out, the language of \(\mathsf{IM}\) is not expressive enough for such an interpretation. Namely, the set of valid formulas over functional models coincides with the set of valid formulas of arbitrary dynamic models, implying that the restriction to functions does not have an impact on the logic. This discourages an interpretation of \(\mathsf{IM}\) as temporal logic. Nevertheless, \(\mathsf{IM}\) remains a relevant logical system in its own right: \(\mathsf{IM}\) is an interesting case study for applying techniques from the study of classical modal fixed point logics to the intuitionistic realm. This is due to the relatively simple mathematical theory of \(\mathsf{IM}\), caused by the lack of meaningful confluence conditions imposed on its dynamic models. Moreover, \(\mathsf{IM}\) serves as the stepping stone to investigate other, more expressive, intuitionistic dynamic logics, such as intuitionistic common knowledge logic which will be studied in Chapter 4 or intuitionistic versions of propositional dynamic logic (\(\mathsf{PDL}\)). The techniques developed to investigate \(\mathsf{IM}\) can be applied or adapted for more complex logics, as illustrated in Chapter 4 where much of the proof theoretic work for \(\mathsf{IM}\) is applied successfully to \(\mathsf{ICK}\).

The next section introduces the syntax and semantics of \(\mathsf{IM}\). The semantics is given in terms of dynamic models, where we consider three classes: the class of all dynamic models, the class of functional dynamic models and the class of dynamic models which are triangle confluent. Regarding expressivity, we prove that the language of \(\mathsf{IM}\) cannot distinguish between all three classes of models, in the sense that they all produce the same set of validites (see Theorem 3.1). Afterwards we turn to proof theory and introduce a sound and complete axiomatization for \(\mathsf{IM}\). The completeness proof is by a standard canonical model construction. Our proof is similar to the completeness proof for classical common knowledge logic presented in [64], highlighting the straightforward adaptation of classical techniques to \(\mathsf{IM}\). Completeness for a multi-modal version of \(\mathsf{IM}\) was already established for a different axiomatization by Marti in his PhD thesis [26], and the presented proof closely follows Marti’s proof. The remaining sections study a sequent calculus for \(\mathsf{IM}\). Due to the presence of the master modality, our proof systems require a formal counterpart to induction. Instead of using an induction rule as is done in [25], we instead employ non-wellfounded and cyclic proofs. First, we give a brief introduction to such proof formalisms and then introduce the cyclic calculus \(\mathrm{cIM}\) and the non-wellfounded calculus \(\mathrm{nIM}\). The calculus \(\mathrm{nIM}\) is not studied in its own right but used as a tool to establish completeness for \(\mathrm{cIM}\). We prove soundness of \(\mathrm{cIM}\) by an indirect argument and completeness for \(\mathrm{nIM}\) via a proof search argument. It is then shown how to translate non-wellfounded proofs into cyclic proofs, whence establishing completeness for \(\mathrm{cIM}\) as well. The presented proof search method is quite robust, which will be illustrated by showing how to obtain dynamic, triangle and functional countermodels from a failed proof search, which requires only minor adjustments to the overall argument. This will also provide an alternative proof of Theorem 3.1 using proof theoretic means.

3.2 Syntax and Semantics↩︎

The language \(\mathcal{L}_\mathrm{IM}\) of \(\mathsf{IM}\) extends \(\mathcal{L}_\mathsf{IPL}\) by the modal operator \(\larger[-1.5]\square\) and the fixed point operator \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\) called the master modality. Formulas of \(\mathcal{L}_\mathrm{IM}\) are given by the following grammar in Backus–Naur form: \[\varphi ::= \bot \, \lvert \, p \, \lvert \, \varphi \wedge \varphi \, \lvert \, \varphi \vee \varphi \, \lvert \, \varphi \rightarrow \varphi \, \lvert \, \larger[-1.5]\square\varphi \, \lvert \, \ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi.\] where \(p \in \mathsf{Prop}\). As before we write \(\varphi \in \mathcal{L}_\mathrm{IM}\) to denote that \(\varphi\) is a \(\mathcal{L}_\mathrm{IM}\)-formula and we use the same conventions for the brackets and the notation as introduced for \(\mathcal{L}_\mathsf{IPL}\).

The following lemma is established by a straightforward induction on the structure of \(\varphi\). The proof is omitted.

The complexity of a formula is defined as follows.

We will evaluate formulas of \(\mathcal{L}_\mathsf{IM}\) over three classes of dynamic models: the class of all dynamic models (see Definition 2.17), the class of functional models (see Definition 2.20), and the class of triangle models, which are defined as follows.

By Corollary 2.1 we can use the classical truth conditions for the modalities when evaluating formulas over triangle models, but in order to obtain monotonicity we shall use the intuitionistic truth conditions for modalities when evaluating formulas over dynamic and functional models. Thus we introduce two truth relations \(\models\) and \(\models_t\).

For any binary relation \(S\), let \(S^*\) denote the reflexive transitive closure of \(S\). Given a dynamic model \(\mathcal{M}=(W,\leq,R,V)\), let \(\tilde{R}\) denote the composition \(R \circ {\leq}\), i.e. \(w \mathrel{\tilde{R}} v\) holds if and only if there exists \(u \in W\) with \(w \leq u\) and \(u \mathrel{R}v\). Note that, since \(\leq\) is reflexive, \(w \mathrel{(\tilde{R})^*} v\) holds if and only if there exist a natural number \(n\) and worlds \(u_0, \ldots, u_{2n}\) such that \(u_0 = w\), \(u_{2n} = v\) and for all \(0 \leq i < n\) both \(u_{2i} \leq u_{2i+1}\) and \(u_{2i+1} \mathrel{R}u_{2(i+1)}\) hold.

A formula \(\varphi\) is satisfiable over the class of dynamic (functional) models if there exists a dynamic (functional) model \(\mathcal{M}=(W, \leq, R, V)\) and a world \(w \in W\) such that \({\mathcal{M},w \models \varphi}\), and unsatisfiable otherwise. The formula \(\varphi\) is valid over the class of dynamic (functional) models if for any dynamic (functional) model \(\mathcal{M}=(W, \leq, R, V)\) and any world \(w \in W\) holds that \(\mathcal{M},w \models \varphi\), and falsifiable otherwise.

Next, we introduce the truth relation \(\models_t\) for evaluating formulas on triangle models.

Note that every triangle model \(\mathcal{M}=(W, \leq, R, V)\) satisfies \(R = \tilde{R}\). The monotonicity property for \(\models_t\) follows immediately from Corollary 2.1 and Lemma 3.2.

The logic \(\mathbf{IM_f}\) can be interpreted as an intuitionistic version of linear temporal logic, where \(f\) is the function mapping each world to its temporal successor, \(\larger[-1.5]\square\) is interpreted as ‘next’ and \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\) as ‘henceforth’. It makes sense under such an interpretation to assume \(f\) to be a total function. Note that \(\mathbf{IM_f}\) does not validate some of the standard tautologies of linear temporal logic, such as \(\larger[-1.5]\square(p \vee q) \rightarrow (\larger[-1.5]\squarep \vee \larger[-1.5]\squareq)\).

We finish this section with the following lemma, stating that every formula valid over the class of dynamic models is also valid over the classes of functional and triangle models. Note that this trivially holds since both functional and triangle models are dynamic models and \(\mathcal{M}, w \models \varphi\) if and only if \(\mathcal{M}, w \models_t \varphi\) for any triangle model \(\mathcal{M}\) and any world \(w\) by Corollary 2.1.

3.3 Expressivity↩︎

This section explores whether the language \(\mathcal{L}_\mathsf{IM}\) can distinguish between the classes of dynamic, functional and triangle models. The main result is Theorem 3.1, stating that all three classes have the same set of valid formulas, i.e. \[\mathbf{IM} = \mathbf{IM_t} = \mathbf{IM_f}.\]

That \(\mathbf{IM} = \mathbf{IM_t}\) is straightforward, and was already observed about the language of \(\mathcal{L}_\mathrm{IM}\) without the master modality in [65]. The following lemma provides a brief proof sketch.

3.3.1 Dynamic and Functional Models↩︎

The goal of this subsection is to establish \(\mathbf{IM} = \mathbf{IM_f}\). By Lemma 3.5, \(\mathbf{IM} \subseteq \mathbf{IM_f}\). For the other inclusion, given a formula \(\varphi\) and a dynamic model \(\mathcal{M}\) falsifying \(\varphi\), we have to show how to construct a functional model \(\mathcal{M}'\) falsifying \(\varphi\). The functional model \(\mathcal{M}'\) will be constructed in stages: we start by adding a copy of the world \(w\) of \(\mathcal{M}\) which falsifies \(\varphi\). Then, in later steps, we add copies of worlds of \(\mathcal{M}\) in such a way that the copy of \(w\) satisfies and falsifies the same formulas as \(w\), and the resulting model is functional. The crucial insight is that if a world \(w\) of \(\mathcal{M}\) has multiple modal successors, we can simply add, for each modal successor, a copy of \(w\) as an intuitionistic successor of \(w\) and for each copy one modal successor. Due to the intuitionistic truth conditions, both models then satisfy the same modal formulas. See Figure 6 for an illustration. In order to formalize the construction, we introduce induced structures.

Since we are only interested in falsifying the formula \(\varphi\), it suffices to ensure that the constructed model evaluates formulas in the closure of \(\varphi\) correctly. Therefore the following definition is given relative to a finite and closed set of formulas \(\Sigma\).

Observe that for any \(\mathcal{M}\)-induced structure \(\mathcal{I}\) and any closed and finite set of formulas \(\Sigma\), there are only finitely many defects, due to \(I\) and \(\Sigma\) being finite.

Suppose \(\mathcal{M}=(W, \leq, R, V)\) is a dynamic model and \(w \in W\) a world such that \(\mathcal{M},w \not \models \varphi\). We are going to construct a functional model \(\mathcal{I}_\omega=(I_\omega, \leq_\omega, R_\omega, V_\omega)\) falsifying \(\varphi\) in stages. To that end let \(\Sigma = \mathsf{Cl}(\varphi)\). We define for each natural number \(n\) an \(\mathcal{M}\)-induced structure \(\mathcal{I}_n\) as well as a first-in-first-out queue \(D\) that stores the defects of \(\mathcal{I}_n\) and we simultaneously prove that \(\mathcal{I}_n\) is an \(\mathcal{M}\)-induced structure. The functional model \(\mathcal{I}_\omega\) is then defined as the limit of the sequence \((\mathcal{I}_n)_{n < \omega}\).

Stage 0: Define the \(\mathcal{M}\)-induced structure \(\langle \mathcal{I}_0 =(I_0, \leq_0, R_0, V_0), \pi_0\rangle\) as follows.

• \(I_0 \mathrel{\vcenter{:}}= \{\tilde{x}\}\) where \(\tilde{x}\) is a fresh world not contained in \(W\).

• \(\leq_0 \mathrel{\vcenter{:}}= \{(\tilde{x},\tilde{x})\}\).

• \(R_0 \mathrel{\vcenter{:}}= \emptyset\).

• \(V_0(\tilde{x}) \mathrel{\vcenter{:}}= V(w)\).

• \(\pi_0(\tilde{x}) \mathrel{\vcenter{:}}= w\).

To complete stage 0, initialize the queue \(D\) by adding all defects of \(\mathcal{I}_0\) to \(D\) in arbitrary order. It is immediate to check that \(\mathcal{I}_0\) is an \(\mathcal{M}\)-induced structure.

Stage n+1: Suppose \(\langle \mathcal{I}_n =(I_n, \leq_n, R_n, V_n), \pi_n \rangle\) has been defined and \(D\) currently stores the defects of \(\mathcal{I}_n\). We show first how to construct \(\langle \mathcal{I}_{n+1}, \pi_{n+1}\rangle\) depending on the defect at the head of the queue \(D\) and then how to update \(D\).

(\(\rightarrow\)-defects) Suppose the defect at the head of the queue \(D\) is an \(\rightarrow\)-defect \((y, \psi \rightarrow \chi)\). Then \(y \in I_n\), \(\psi \rightarrow \chi \in \Sigma\) and \(\mathcal{M}, \pi_n(y) \not \models \psi \rightarrow \chi\), however there does not exists a world \(y' \in I_n\) with \(y' \geq_n y\) such that \(\mathcal{M}, \pi_n(y') \models \psi\) and \(\mathcal{M}, \pi_n(y') \not \models \chi\). Since \({\mathcal{M}, \pi_n(y) \not \models \psi \rightarrow \chi}\), there exists a world \(u \geq \pi_n(y)\) such that \(\mathcal{M},u \models \psi\) and \(\mathcal{M},u \not \models \chi\). Let \(y'\) be a fresh world not occurring in \(I_n\) or \(W\) and define

• \(I_{n+1} \mathrel{\vcenter{:}}= I_n \cup \{y'\}\);

• let \(\leq_{n+1}\) be the reflexive transitive closure of \(\leq_n \cup \{(y, y')\}\);

• \(R_{n+1} \mathrel{\vcenter{:}}= R_n\);

• \(V_{n+1}\) is defined by \[V_{n+1}(z) := \begin{cases} V(u) & \text{if } z=y'\\ V_n(z) & \text{otherwise;}\\ \end{cases}\]

• \(\pi_{n+1}\) is defined by \[\pi_{n+1}(z) := \begin{cases} u & \text{if } z= y'\\ \pi_n(z) & \text{otherwise.}\\ \end{cases}\]

To see that \(\mathcal{I}_{n+1}\) is an \(\mathcal{M}\)-induced structure, first note that by induction hypothesis \(I_n\) is a finite set, and therefore \(I_{n+1}\) is a finite set too. Suppose \(x \leq_{n+1} z\). Then either \(x \leq_n z\) which implies by induction hypothesis that \(\pi_n(x) \leq \pi_n(z)\) and thus also \(\pi_{n+1}(x) \leq \pi_{n+1}(z)\), or \(x \leq_n y\) and \(z= y'\), which, by construction and induction hypothesis, implies \(\pi_{n+1}(x) \leq \pi_{n+1}(y) \leq \pi_{n+1}(z)\). That \((I_{n+1}, \leq_{n+1})\) is a poset follows immediately from the induction hypothesis and the construction. Next, \(R_{n+1} = R_n\) by construction and thus, by induction hypothesis, \(R_{n+1}\) is a partial function and if \(R_{n+1}(x) = z\), then \(\pi_{n+1}(x)\mathrel{R}\pi_{n+1}(z)\). If \(x \in I_n\), then \(V_n(x) = V(\pi_n(x))\) by induction hypothesis, so by construction \(V_{n+1}(x) = V(\pi_{n+1}(x))\). Otherwise \(x= y'\) and \(V_{n+1}(x) = V(\pi_{n+1}(x))\) by construction. Thus \(V_{n+1}= V \circ \pi_{n+1}\). Finally, by induction hypothesis \(\pi_n: I_n \longrightarrow W\) is a function. Since \(y'\) is a fresh world, \(\pi_{n+1}:I_{n+1} \longrightarrow W\) is a function as well. Thus \(\langle \mathcal{I}_{n+1}, \pi_{n+1}\rangle\) is an \(\mathcal{M}\)-induced structure.

(\(\larger[-1.5]\square\)-defects) Suppose the defect at the head of the queue \(D\) is a \(\larger[-1.5]\square\)-defect \((y, \larger[-1.5]\square\psi)\). Then \(y \in I_n\), \(\larger[-1.5]\square\psi \in \Sigma\), \(\mathcal{M}, \pi_n(y) \not \models \larger[-1.5]\square\psi\) but there does not exist a world \(y' \in I_n\) with \(y \mathrel{(R_n \circ {\leq_n})} y'\) and \(\mathcal{M}, \pi_n(y') \not \models \psi\). Since \(\mathcal{M}, \pi_n(y) \not \models \larger[-1.5]\square\psi\), there exist worlds \(u_0, u_1 \in W\) with \(\pi_n(y) \leq u_0 \mathrel{R} u_1\) and \(\mathcal{M}, u_1 \not \models \psi\). Let \(y_0, y_1\) be fresh worlds⁷ not occurring in \(I_n\) or \(W\). Define

• \(I_{n+1} \mathrel{\vcenter{:}}= I_n \cup \{y_0, y_1\}\);

• let \(\leq_{n+1}\) be the reflexive transitive closure of \(\leq_n \cup \{(y, y_0)\}\);

• \(R_{n+1} \mathrel{\vcenter{:}}= R_n \cup \{(y_0,y_1)\}\);

• \(V_{n+1}\) is defined by \[V_{n+1}(z) := \begin{cases} V(u_0) & \text{if } z= y_0\\ V(u_1) & \text{if } z= y_1 \\ V_n(z) & \text{otherwise;}\\ \end{cases}\]

• \(\pi_{n+1}\) is defined by \[\pi_{n+1}(z) := \begin{cases} u_0 & \text{if } z= y_0\\ u_1 & \text{if } z= y_1 \\ \pi_n(z) & \text{otherwise.}\\ \end{cases}\]

Let us check that \(\mathcal{I}_{n+1}\) is an \(\mathcal{M}\)-induced structure. That \(I_{n+1}\) is finite, \(x \leq_{n+1} y\) implies \(\pi_{n+1}(x) \leq \pi_{n+1}(y)\) and that \((I_{n+1}, \leq_{n+1})\) is a poset follow by similar argument as above. Suppose \(R_{n+1}(x) = z\). Then either \(R_n(x) = z\), which by induction hypothesis implies that \(\pi_n(x) \mathrel{R} \pi_n(y)\) and so \(\pi_{n+1}(x) \mathrel{R} \pi_{n+1}(y)\) by construction, or \(x=y_0\) and \(z = y_1\). In that case we have by construction \(\pi_{n+1}(x) \mathrel{R} \pi_{n+1}(y)\) as well. Moreover, by induction hypothesis and construction, \(R_{n+1}\) is a partial function. That \(V_{n+1} = V \circ \pi_{n+1}\) and that \(\pi_{n+1}\) is a function follow by similar arguments as above.

(\(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\)-defects) Suppose the defect at the head of the queue \(D\) is a \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\)-defect \((y, \ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\psi)\). Then \({y \in I_n}\), \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\psi \in \Sigma\), \(\mathcal{M}, \pi_n(y) \not \models \ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\psi\) but there does not exist a world \(y' \in I_n\) with \({y \mathrel{(R_n \circ {\leq_n})^*} y'}\) such that \(\mathcal{M}, \pi_n(y') \not \models \psi\). Since \(\mathcal{M}, \pi_n(y) \not \models \ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\psi\), there exists a world \(u \in W\) with \(\pi_n(y) \mathrel{(R \circ {\leq})^*} u\) and \(\mathcal{M},u \not \models \psi\). Let \(u_0, \ldots, u_{2k} \in W\) such that \(u_0 = \pi_n(y)\), \(u_{2k} = u\) and for all \(0 \leq i < k\) holds that \(u_{2i} \leq u_{2i+1}\) and \(u_{2i+1} \mathrel{R}u_{2(i+1)}\). Observe that \(k > 0\) as by assumption \(\mathcal{M}, \pi_n(y) \models \psi\) (again, some worlds \(u_{2i+1}\) might be identical to \(u_{2i}\)). Let \(y_i\) for \(1 \leq i \leq 2k\) be fresh worlds not occuring in \(I_n\) or \(W\). Define

• \(I_{n+1} \mathrel{\vcenter{:}}= I_n \cup \{y_1, \ldots, y_{2k}\}\);

• let \(\leq_{n+1}\) be the reflexive transitive closure of \[\leq_n \cup \{(y, y_1)\} \cup \{(y_{2i}, y_{2i+1}) \, \lvert \, 1 \leq i < k\};\]

• \(R_{n+1} \mathrel{\vcenter{:}}= R_n \cup \{(y_{2i+1}, y_{2(i+1)}) \, \lvert \, 0 \leq i < k\}\);

• \(V_{n+1}\) is defined by \[V_{n+1}(z) \mathrel{\vcenter{:}}= \begin{cases} V(u_i) & \text{if } z= y_i \text{ for } 1 \leq i \leq 2k\\ V_n(z) & \text{otherwise;}\\ \end{cases}\]

• \(\pi_{n+1}\) is defined by \[\pi_{n+1}(z) \mathrel{\vcenter{:}}= \begin{cases} u_i & \text{if } z= y_i \text{ for } 1 \leq i \leq 2k\\ \pi_n(z) & \text{otherwise.}\\ \end{cases}\]

Let us check that \(\mathcal{I}_{n+1}\) is an \(\mathcal{M}\)-induced structure. That \(I_{n+1}\) is finite and \((I_{n+1}, \leq_{n+1})\) is a poset follows by similar arguments as above. Suppose \(x \leq_{n+1} z\). Then either \(x \leq_n z\), in which case by induction hypothesis and construction \(\pi_{n+1}(x) \leq \pi_{n+1}(z)\), or \(x\leq_n y\) and \(z = y_1\), in which case by induction hypothesis and construction \(\pi_{n+1}(x) \leq \pi_{n+1}(y) \leq \pi_{n+1}(z)\), or \(x= y_{2i}\) and \(z =y_{2i+1}\) for \(1 \leq i \leq k\) (observe that by construction no world lies below \(y_{2i}\) in the order \(\leq_{n+1}\)). In this case \(\pi_{n+1}(x) \leq \pi_{n+1}(z)\) by construction. Thus \(x \leq_{n+1} z\) implies \(\pi_{n+1}(x) \leq \pi_{n+1}(z)\). By induction hypothesis \(R_n\) is a partial function and so by construction \(R_{n+1}\) is a partial function as well. Suppose \(R_{n+1}(x) = z\). Then either \(R_n(x) = z\), from which by induction hypothesis and construction follows that \(\pi_{n+1}(x) \mathrel{R} \pi_{n+1}(z)\), or \(x = y_{2i+1}\) and \(z=y_{2(i+1)}\) for \(1 \leq i < k\). In that case \(\pi_{n+1}(x) \mathrel{R} \pi_{n+1}(z)\) by construction. Thus \(R_{n+1}(x) = z\) implies \(\pi_{n+1}(x) \mathrel{R} \pi_{n+1}(z)\). Finally, the cases for \(V_{n+1}\) and \(\pi_{n+1}\) follow by similar arguments as above.

Having defined \(\langle \mathcal{I}_{n+1}, \pi_{n+1}\rangle\), we update the queue \(D\) as follows. First, delete every defect that has been resolved in the step from \(n\) to \(n+1\). Then add every new defect of \(\mathcal{I}_{n+1}\) to the tail of the queue \(D\). Observe that by induction hypothesis, the queue \(D\) stores finitely many defects at stage \(n\). After updating, we add at most finitely many new defects to \(D\), since \(I_{n+1}\) and \(\Sigma\) are finite. We have therefore shown the following:

The functional model \(\mathcal{I}_\omega\) is now defined as the limit of the sequence \((\mathcal{I}_n)_{n < \omega}\).

The structure \(\mathcal{I}_\omega\) is called the \(\mathcal{M}\)-induced model. Observe that \(x \in I_\omega\) if and only if there exists \(n < \omega\) such that \(x \in I_n\). Moreover, \(x \leq_\omega y\) if and only if there exists \(n < \omega\) such that \(x \leq_n y\) and similarly for \(x \mathrel{R}_\omega y\) and \(p \in V_\omega(x)\).

It remains to show that the \(\mathcal{M}\)-induced model preserves truth. Recall that \(\varphi \in \mathcal{L}_\mathrm{IM}\) with \(\mathcal{M}, w \not \models \varphi\) and \(\mathsf{Cl}(\varphi) = \Sigma\).

Theorem 3.1 raises the question whether a similar result holds for serial dynamic models (i.e. dynamic models with a serial modal accessibility relation), serial triangle models and total functional models? Clearly, transforming serial dynamic models into serial triangle models works by employing the same construction as given in Lemma 3.6. For transforming serial dynamic models into total functional models, some small adaptions of the construction presented in the proof of Theorem 3.1 are required. We briefly sketch the basic idea.

In the construction of a functional model, \(\larger[-1.5]\square\)-defects \((x, \larger[-1.5]\square\varphi)\) were resolved by first adding an intuitionistic successor \(y\) of \(x\) and then a modal successor \(z\) of \(y\) to provide a witness where \(\larger[-1.5]\square\varphi\) is falsified. This implies that many worlds in \(\mathcal{I}_\omega\) do not have a modal successor. When constructing a total functional model we must guarantee that every world has a unique modal successor. There are several ways how to achieve this. Perhaphs the easiest solution is to use the same construction as for functional models (i.e. \(\larger[-1.5]\square\)- and \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\)-defects are resolved by adding intuitionistic successors and then modal successors), but to consider an additional type of defect called a functional defect. Such a defect is simply a world \(x\) in an induced structure for which no modal successor exists. Functional defects are then resolved by considering the related world \(\pi(x)\) in the serial dynamic model and chose an arbitrary modal successor \(u\) of \(\pi(x)\), which exists by seriality. Then add a fresh world \(y\) to the induced structure as a modal successor of \(x\) and define \(\pi(y) = u\). The resulting structure is a total functional model which satisfies the corresponding version of Lemma 3.10.

This explanation should suffice to convince us that \(\mathcal{L}_\mathrm{IM}\) cannot distinguish between serial dynamic models, serial triangle models and total functional models either.

3.4 Axiomatization↩︎

This section introduces a Hilbert-style axiomatization capturing the \(\mathcal{L}_\mathrm{IM}\)-validities over the classes of dynamic / triangle / functional models. An axiomatization for a multi-modal version of \(\mathsf{IM}\) was presented in [26]. Here, we present a different axiomatization, which is more in line with axiomatizations given later on in the thesis. The presented axiomatization is called \(\mathrm{IM_H}\). We also establish basic properties of \(\mathrm{IM_H}\), such as soundness and the Deduction Theorem.

The axiom schemes are \(\mathsf{Int}\), \(\mathsf{K}\) and \(\mathsf{Fix}\). Instances of \(\mathsf{Int}\) are intuitionistic tautologies, i.e. \(\mathcal{L}_\mathrm{IM}\)-formulas obtained from a \(\mathrm{IPL_H}\)-derivable formula via uniform substitution; see Definition 2.13. The axiom scheme \(\mathsf{K}\) describes that \(\larger[-1.5]\square\) distributes over implications while \(\mathsf{Fix}\) describes that \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) is equivalent to its unfolding \(\varphi \wedge \larger[-1.5]\square\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\). The inference rules are \(\mathsf{MP}\), \(\mathsf{Nec}\), \(\mathsf{Mon}\) and \(\mathsf{Ind}\). The rule \(\mathsf{Ind}\) is the induction rule. If we have a proof of \(\varphi\) (the base case) and a proof of \(\varphi \rightarrow \larger[-1.5]\square\varphi\) (the induction step), then we can apply \(\mathsf{Ind}\) and \(\mathsf{MP}\) to obtain a proof of \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\).

If \(\Gamma \vdash \varphi\), then \(\varphi\) is called derivable from \(\Gamma\). If \(\Gamma = \emptyset\), then \(\varphi\) is simply called derivable. Note that the rules \(\mathsf{Nec}\), \(\mathsf{Mon}\) and \(\mathsf{Ind}\) cannot be applied to assumptions. We will use the standard proof theoretic conventions and denote sets of formulas with \(\Gamma, \Delta\) etc. and we write \(\Gamma, \varphi\) for \(\Gamma \cup \{\varphi\}\). Moreover, derivations (with or without assumptions) are denoted by \(\pi\) or \(\tau\).

The following lemma serves as an example for derivations and, at the same time, establishes the derivability of some formulas that will become useful in the completeness proof.

We may now prove the Deduction Theorem, which will play a crucial role in the completeness proof.

We obtain the following useful corollary. Recall that \(\bigwedge \emptyset = \top\).

We conclude this section by proving that \(\mathrm{IM_H}\) is sound. First, let us check that all axioms and rules of \(\mathrm{IM_H}\) are valid or validity preserving, respectively.

Soundness of \(\mathsf{IM_H}\) is then established by induction on the height of derivations. The proof is routine.

3.5 Completeness of the Axiomatization↩︎

This section establishes completeness of \(\mathrm{IM_H}\). The proof is by a canonical model construction, where we construct for each formula \(\varphi\) a finite canonical model. The presented proof closely follows the completeness proof for a multi-modal version of \(\mathsf{IM}\) given in [26].

Fix an arbitrary finite and closed set of formulas \(\Sigma\).

\(\Sigma\)-prime theories will form the worlds of the canonical model. The following version of the Lindenbaum Lemma states that any consistent set of \(\Sigma\)-formulas can be extended into a \(\Sigma\)-prime theory.

For a set of formulas \(\Gamma\), define the following notation. \[\begin{align} \larger[-1.5]\square\Gamma & := \{ \larger[-1.5]\square\varphi \mid \varphi \in \Gamma \} \\ \larger[-1.5]\square^{-1} \Gamma & := \{\varphi \mid \larger[-1.5]\square\varphi \in \Gamma\}\\ \end{align}\]

We are ready to define the canonical model relative to a given finite and closed set of formulas \(\Sigma\). From now on until the end of the section, the Greek letters \(\Gamma, \Delta\) and \(\Omega\) refer exclusively to \(\Sigma\)-prime theories for some fixed \(\Sigma\).

The last step to obtain completeness is to establish the Truth Lemma, which states that for any formula \(\varphi \in \Sigma\) and any \(\Sigma\)–prime theory \(\Gamma\), \(\Gamma \vdash \varphi\) if and only if \(\mathcal{M}_\Sigma, \Gamma \models_t \varphi\). For \(\Gamma \in W_\Sigma\), let the reachable component of \(\Gamma\) be the set \(\mathsf{R}_\Sigma^*(\Gamma) \mathrel{\vcenter{:}}= \{\Delta \in W_\Sigma \mid \Gamma \mathrel{R}_\Sigma^* \Delta\}\). Note that \(\mathsf{R}_\Sigma^*(\Gamma)\) is finite.

The characteristic formula \(\chi(\Gamma)\) characterizes the prime theory \(\Gamma\). The reachable component formula \(\gamma(\Gamma)\) characterizes the reachable component of \(\Gamma\).

It remains to show completeness of \(\mathrm{IM_H}\) with respect to the class of triangle models (and so also with respect to the classes of functional and of dynamic models).

The logic \(\mathbf{IM_t}\) has the finite (triangle) model property if every falsifiable formula over the class of triangle models is falsifiable over the class of finite triangle models. Since the canonical model is finite, we obtain the finite (triangle) model property. As usual, the finite model property combined with a finite sound and complete axiomatization yields decidability.

3.6 Non-Wellfounded and Cyclic Proofs↩︎

The axiomatization \(\mathrm{IM_H}\) captures the validities of \(\mathsf{IM}\) in a neat way. However, from a proof theoretic perspective, axiomatizations are unsatisfactory, since the presence of the modus ponens rule obstructs the proof theoretic analysis. As witnessed in the previous sections, to check whether an \(\mathcal{L}_\mathrm{IM}\)-formula \(\varphi\) is derivable in \(\mathrm{IM_H}\), we have to guess the right instances of intuitionistic tautologies in order to apply modus ponens. This drawback can be circumvented by passing to analytic sequent calculi. Analytic means that every provable sequent \(\sigma\) has a proof in which only formulas that are relevant to the formulas in \(\sigma\) may occur. What ‘relevant’ means depends on the specific logic at hand. For \(\mathsf{IM}\) we count as relevant those formulas that belong to the closure of \(\sigma\). The obstacle for constructing an analytic sequent calculus for \(\mathsf{IM}\) lies in the presence of the master modality, which, as a fixed point operator, requires an induction rule to treat its infinite behaviour (recall that \(\mathrm{IM_H}\) featured the rule \(\mathsf{Ind}\)). A sequent calculus with an induction rule for a multi-modal version of \(\mathsf{IM}\) was proposed by Jäger and Marti [25]. Their induction rule translates to our setting as follows. \[\infer[\mathsf{Ind_s}]{\Pi, \ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\Gamma, \psi \Rightarrow \ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi, \Delta}{\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\Gamma, \psi \Rightarrow \varphi, \Delta & \ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\Gamma, \psi \Rightarrow \larger[-1.5]\square\psi, \Delta}\]

This rule states that if we can prove \(\varphi\) from \(\psi\) and we can prove \(\larger[-1.5]\square\psi\) from \(\psi\), then we can also prove \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) from \(\psi\). The drawback of induction rules is that their presence usually leads to a non-analytic system. For example, the calculus presented by Jäger and Marti is proven sound and complete, but the proof makes essential use of the cut rule and no cut elimination result is given. It is unclear whether completeness can be obtained without cut. For example, for a classical version of \(\mathsf{IM}\) (namely common knowledge logic) evaluated over S5 models, a sequent calculus with induction rule is presented by Alberucci and Jäger [66]. Once again the cut rule is required, but the authors manage to obtain a partial cut elimination result. Nevertheless, a restriction to analytic cuts (i.e. instances of the cut rule where the cut formula belongs to the set of formulas which is ‘relevant’) was not achieved.

Let us pause here and briefly discuss why induction rules cause problems for obtaining analytic calculi. Proofs by induction are difficult to formalize due to the problem of finding the right induction hypothesis. A standard example is the following. Suppose we want to show that for all natural numbers \(n\), \[\label{e:32induction32problem} s_n= \sum_{k \leq n} \frac{1}{k^2} < 2.\tag{13}\] This statement does not admit a direct inductive proof: the induction hypothesis gives us that \(s_n < 2\). But in order to prove that \(s_{n+1} < 2\), we would require to know that \(\frac{1}{(n+1)^2} < 2 - s_n\), which is not provided by the induction hypothesis. We may circumvent this problem by guessing a stronger statement which implies (13 ). Namely, the following statement suffices:

\[s_n= \sum_{k \leq n} \frac{1}{k^2} \leq 2 - \frac{1}{n}.\]

This is a problem frequently encountered in inductive proofs and translates into the realm of sequent calculi: the problem of guessing the right induction hypothesis results in an induction rule which is either non-analytic or requires the presence of the cut rule to obtain completeness.

One possible solution is to abandon induction rules for sequent calculi all together and replace them by a formal counterpart for proofs by infinite descent. It is usually accepted that such proofs are equally strong as inductive proofs, see for example [67]. Proofs by infinite descent are not formalized by adding a corresponding rule, but instead by the shape of the proof tree: we consider non-wellfounded proofs, which are proofs in a sequent calculus as defined in Chapter 2 but the proof tree is allowed to have infinitely long branches. The entire infinite branch is then the formal representation of an argument by infinite descent. To obtain infinite branches, we will use simple unfolding rules for \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\) of the form \[\infer{\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi}{\varphi \wedge \larger[-1.5]\square\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi}\] which replace (when read bottom-up) a formula of the form \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) by its unfolding \(\varphi \wedge \larger[-1.5]\square\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\). The presence of such a rule naturally leads to non-wellfounded proofs, as we can generate infinite branches by starting with a formula \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\), unfold it into \(\varphi \wedge \larger[-1.5]\square\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) and then use the other rules of the calculus to decompose \(\varphi \wedge \larger[-1.5]\square\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) back into \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\), creating a repetition. Note that between such a repetition the branch must pass through a modality rule to get from \(\larger[-1.5]\square\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) to \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\). Intuitively, we may think of this step as taking a modal step in a dynamic model: if at \(w\) the formula \(\larger[-1.5]\square\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) is falsified, then there exists a modal successor \(v\) at which \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) is falsified. In order to seperate valid from invalid infinitary reasoning, infinite branches in a non-wellfounded proof must satisfy a global correctness criterion. For \(\mathsf{IM}\), this criterion roughly states that every infinite branch must progress infinitely often, where progress means passing through an unfolding of a \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\)-formula. Infinite branches therefore contain infinitely many instances of the rule for \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\). Intuitively, this conditions implies that an infinite branch proves \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) by proving \(\larger[-1.5]\square^n \varphi\) for any natural number \(n\).

Non-wellfounded proofs therefore trade the finiteness of proofs for analyticity of the calculus. One may object that this seems hardly an improvement, but we would like to disagree. First, one goal of proof theory is to study mathematical proofs as mathematical objects. Proofs by infinite descent are infinite arguments that are commonly employed in mathematics; it seems natural to study such proofs in their own right. Second, some non-wellfounded calculi can be proven to be regularly complete: every valid sequent has a regular non-wellfounded proof. Roughly, a non-wellfounded proof is regular if it contains only finitely many subtrees up to isomorphism. Regular non-wellfounded proofs can be depicted as a finite trees with back-edges: arrows that point from the leaves back into the tree. The intended meaning is that the infinite tree can be obtained by taking the finite tree with back-edges and co-recursively glue the trees rooted at the nodes to which the arrows point at on top of the corresponding leaf. Such finite trees with back-edges are called cyclic proofs and may be understood as finite representations of infinite proofs. Just as infinite branches in a non-wellfounded proof satisfy a global criterion, finite branches in a cyclic proof that end in a leaf with a back-edge must satisfy a local correctness criterion. Cyclic calculi therefore enjoy the advantages of both sides: finite proofs and analytic rules. However, not every non-wellfounded calculus is regularly complete; we will see an example in Chapter 5.

The goal of this section is to introduce a non-wellfounded sequent calculus called \(\mathrm{nIM}\) and a cyclic sequent calculus called \(\mathrm{cIM}\) for \(\mathsf{IM}\). We begin by introducing the basic definitions and the two calculi. The focus then lies on the cyclic calculus \(\mathrm{cIM}\) which is proven to be sound and complete. The non-wellfounded calculus \(\mathrm{nIM}\) is only used as a tool to establish completeness for \(\mathrm{cIM}\): we will use a proof search argument to show that \(\mathrm{nIM}\) is complete. The proof search argument provides another example of the adaptation of techniques which are successfully used for classical modal fixed point logics to the intuitionistic realm. However, the presence of the intuitionistic order complicates the overall argument. Completeness of \(\mathrm{cIM}\) is then derived by showing how to prune non-wellfounded proofs into cyclic proofs.

3.6.1 Basic Definitions↩︎

In order to formalize the aforementioned correctness criteria, the two calculi \(\mathrm{nIM}\) and \(\mathrm{cIM}\) employ a simple formula annotation. Intuitively, this annotation keeps track of the development of a master modality formula throughout a branch. The annotation is used to show that the cyclic calculus is sound. Moreover, it simplifies the global correctness criterion for infinite branches in the non-wellfounded calculus, even though the use of annotations is not necessary to obtain a sound non-wellfounded calculus (see Chapter 5 for a non-wellfounded calculus without annotation).

Annotated formulas are written as \(\varphi^a\). We display annotated formulas without using brackets, e.g. the formula \(\varphi \to \psi^\mathsf{u}\) should be read as \((\varphi \rightarrow \psi)^\mathsf{u}\). For the remainder of this chapter, the term formula refers to annotated formula. Formulas without annotations are referred to as plain formulas. Finite sets of annotated formulas are denoted by \(\Gamma, \Delta, \Sigma\) and \(\Pi\) with or without subscripts. For a set of annotated formulas \(\Gamma\) define \[\Gamma^- = \{\varphi \mid \varphi^a \in \Gamma\} \text{ and } \Gamma^\mathsf{u}= \{\varphi^\mathsf{u}\mid \varphi^a \in \Gamma\}.\]

Sequents are denoted by \(\sigma\), where \(\Gamma_\sigma\) and \(\Delta_\sigma\) denotes the left and right side of \(\sigma\) respectively. The interpretation of \(\sigma\) is the formula \(\sigma^I \coloneq \bigwedge \Gamma_\sigma^- \rightarrow \bigvee \Delta_\sigma^-\). Note that annotations convey no semantic meaning. Given a pointed model \((\mathcal{M},w)\) we write \(\mathcal{M},w \models \sigma\) iff \(\mathcal{M}, w \models \sigma^I\), i.e. the notation for the interpretation is usually surpressed. Given a sequent \(\sigma\), the closure of \(\sigma\) is the set \(\mathsf{Cl}(\sigma) \coloneq \mathsf{Cl}(\Gamma^-_\sigma) \cup \mathsf{Cl}(\Delta^-_\sigma)\).

Note that sequents \(\sigma\) are multi-conclusion, i.e. \(\Delta_\sigma\) may contain more than one formula. This streamlines the proof search argument for completeness as it allows writing the disjunction and left-implication rules in invertible form. But it is not an essential restriction; we showed in [39] how single-conclusion proofs are obtained from multi-conclusion proofs by a co-recursive proof translation.

In the next subsections we will define the non-wellfounded calculus \(\mathrm{nIM}\) and the cyclic calculus \(\mathrm{cIM}\). Both calculi consist of the rules depicted in Table 4.

The rules in Table 4 for \(\wedge, \vee, \rightarrow\) as well as \(\mathsf{id}\) and \(\bot\) are annotated versions of the rules for \(\mathrm{IPL_G}\). The annotations do not play a role for these rules, since only formulas of the form \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\psi\) or \(\larger[-1.5]\square\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\psi\) can be in focus. The rules \(\mathsf{u}\) and \(\mathsf{f}\) are called the focus rules and are used to change the focus annotation of a formula. The rule \(\larger[-1.5]\square\) is a standard modal rule, while \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\mathsf{L}\) and \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\mathsf{R}\) replace a master modality formula \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) - when read bottom-up - with its unfolding and thus reflect the equivalence \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi \leftrightarrow \varphi \wedge \larger[-1.5]\square\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\). Note that the annotations play a role in the rules \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\mathsf{R}\) and \(\larger[-1.5]\square\). All rules apart from \(\mathsf{u}\) and \(\mathsf{f}\) are called logical rules.

Note that the rules \({\rightarrow} \mathsf{R}\) and \(\larger[-1.5]\square\) have single-conclusion premises. Therefore it is routine to check that these two rules are not invertible, while all other rules are.

We will therefore refer to \(\larger[-1.5]\square\) and \({\to}\mathsf{R}\) as the non-invertible rules and to all other rules as invertible. It will also be useful to refer to formulas occurring in a rule instance according to their specific role. For each rule except \(\larger[-1.5]\square\), the distinguished formula in the conclusion is called principal and the distinguished formula(s) in the premises are called its residual(s). For the rule \(\larger[-1.5]\square\), all formulas in the conclusion are called principal and each formula in the premise is the residual of its corresponding boxed formula in the conclusion (formulas in \(\Sigma\) and \(\Pi\) have no residuals). In every rule instance, any formula that is neither principal nor residual is called a side formula.

The condition that sequents have at most one formula in focus imposes restrictions on rule applications, as is illustrated by the following lemma.

We will usually construct proofs bottom-up. That is if \(\sigma\) is a sequent and \(\mathsf{r}\) a rule, then ‘\(\mathsf{r}\) is applied to \(\sigma\)’ means that we consider a rule instance of \(\mathsf{r}\) with conclusion \(\sigma\).

3.6.2 Non-Wellfounded Proofs↩︎

We introduce the non-wellfounded calculus \(\mathrm{nIM}\). The calculus is based on the rules from Table 4. We then define the notions of (non-wellfounded) pre-proof and of (non-wellfounded) proof, where a proof is defined as a pre-proof which satisfies certain correctness conditions on its finite and infinite branches.

Non-wellfounded (pre-)proofs in \(\mathrm{nIM}\) are called \(\mathrm{nIM}\)-(pre-)proofs. For the following it may be instructive to recall the basic definitions about trees, in particular the definitions of paths and branches (c.f. Chapter 2, Section 2.1).

Note that pre-proofs are finite-branching since every rule of \(\mathrm{nIM}\) has only finitely many premises and therefore, by König’s Theorem, infinite pre-proofs contain infinite branches.

If there is no danger of confusion, we will tacitly identify a node in a pre-proof with the sequent labelling it and thereby paths and branches of a pre-proof with sequences of sequents. In order for a pre-proof to be a proof it must satisfy a global correctness criterion on its infinite branches: every infinite branch must contain a good suffix.

An illustration of a non-wellfounded proof is provided in Example 3.2 below. The following lemma establishes a straightforward yet crucial property of good suffixes.

3.6.3 Cyclic Proofs↩︎

Next, we introduce the cyclic calculus \(\mathrm{cIM}\) which uses the same rules as \(\mathrm{nIM}\). As before, we first introduce cyclic pre-proofs and then characterize the subset of pre-proofs that are proofs.

Cyclic (pre-)proofs in \(\mathrm{cIM}\) are called \(\mathrm{cIM}\)-(pre-)proofs.

In order to distinguish cyclic pre-proofs from cyclic proofs, we require to formulate a local correctness criterion for those branches in a cyclic proof that do not end in an axiom. This criterion is essentially a finite version of the global correctness criterion for \(\mathrm{nIM}\)-proofs.

Given a \(\mathrm{cIM}\)-pre-proof \(\pi\), a pair of nodes \((u,v)\) of \(\pi\) is called a repetition if \(u \not= v\), there exists a path from \(u\) to \(v\) and both nodes are labelled by the same sequent. A repetition \((u,v)\) is successful if the path from \(u\) to \(v\) is successful.

Given a cyclic proof \(\pi\), leafs labelled by axioms are called axiomatic leafs and all other leafs are called non-axiomatic leafs.

3.7 Soundness of the Cyclic Calculus↩︎

The remainder of this chapter deals with establishing soundness and completeness of \(\mathrm{cIM}\) for the classes of dynamic, functional and triangle models. Apart from simply providing soundness and completeness proofs, we also aim to give an alternative (proof-theoretic) proof of Theorem 3.1. By Lemma 3.5, we have \(\mathbf{IM} \subseteq \mathbf{IM_t}\) and \(\mathbf{IM} \subseteq \mathbf{IM_f}\). In the proof of Theorem 3.1, we established the other inclusions by showing how to translate dynamic models into triangle models and into functional models. Here, we will establish the other inclusions by first showing that every \(\mathrm{cIM}\)-provable formula belongs to \(\mathbf{IM}\), and then that every formula in \(\mathbf{IM_t}\) and \(\mathbf{IM_f}\) is \(\mathrm{cIM}\)-provable.

This section carries out the first step by proving soundness of \(\mathrm{cIM}\) with respect to the class of dynamic models.¹¹ Therefore, the terms ‘valid’, ‘invalid’ and so on refer in this section exclusively to the class of dynamic models.

Since cyclic proofs may contain non-axiomatic leafs, a more complex argument than an induction on the height of a proof is required to establish soundness. Intuitively, the cyclic calculus is sound because success of repetitions ensures that along every repetition, progress is made in the form of a modal step: as a result, when proving \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\phi\) we are essentially proving \(\larger[-1.5]\square^n\phi\) for every \(n<\omega\). To prove this formally, we argue by contraposition. We first assign to each invalid sequent with a formula in focus a measure in the form of a natural number. Then, assuming there is a cyclic proof \(\pi\) of an invalid sequent, we show that there must be a successful repetition \((u,v)\) in \(\pi\) of invalid sequents whose measure strictly decreases along the path \((u,v)\). As \(u\) and \(v\) are labelled by the same sequent, this contradicts the fact that measures are well-defined. The following proof is routine (c.f. Lemma 3.13).

Let \(\sigma\) be a sequent that has a formula in focus, i.e., \(\Delta_\sigma\) contains a formula of the form \(\larger[-1.5]\square^j \ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi^\mathsf{f}\) for \(j \in \{0,1\}\). Denote by \(\sigma(n)\) the sequent \(\Gamma_\sigma \Rightarrow \Delta_\sigma, \larger[-1.5]\square^j \larger[-1.5]\square^n \varphi^\mathsf{u}\), i.e., the sequent expanding the right side of \(\sigma\) by the formula \(\larger[-1.5]\square^j \larger[-1.5]\square^n \varphi^\mathsf{u}\).

As a consequence, every invalid sequent \(\sigma\) with a formula in focus can be assigned a measure: \[\mu(\sigma) \mathrel{\vcenter{:}}= \min \{n < \omega \mid \sigma(n) \text{ is invalid}\}.\] We may now prove a strenghtening of Lemma 3.23.

Note that soundness of \(\mathrm{cIM}\) with respect to the class of dynamic models implies soundness with respect to the classes of functional and of triangle models.

3.8 Completeness of the Cyclic Calculus↩︎

This section establishes completeness of the cyclic calculus with respect to triangle and functional models. The argument proceeds in two steps. First, we set up a general framework for proving completeness via proof search games, from which completeness of the non-wellfounded calculus \(\mathrm{nIM}\) is deduced. We then show how to transform an arbitrary \(\mathrm{nIM}\)-proof into a \(\mathrm{cIM}\)-proof, whence obtaining completeness of \(\mathrm{cIM}\).

3.8.1 Proof Search Games↩︎

Each sequent \(\sigma\) will be associated with a proof search tree which will form the arena of a two-player game between Prover, whose winning strategies establish proofs of \(\sigma\), and Refuter, whose winning strategies describe countermodels for \(\sigma\). Completeness then becomes a corollary of determinacy of the game.

A proof search tree for \(\sigma\) is built by applying rules bottom-up to \(\sigma\). The invertible rules are applied first until a saturated sequent is obtained.

As we are working with set sequents, formulas can simultaneously function as principal and as side formulas. We call an application of a rule preserving if the principal formula(s) also occurs as a side formula. For example, in the following two applications of \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\mathsf{L}\) to the sequent \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi^\mathsf{u}\Rightarrow \psi^\mathsf{u}\), the left application is preserving but the right application is not:

When a rule is applied preservingly to a sequent \(\sigma\), we ensure that the premise(s) preserve the information contained in \(\sigma\) by preserving all formulas of \(\sigma\). Note that applications of the non-invertible rules \(\larger[-1.5]\square\) and \({\to}{\mathsf{R}}\) are never preserving. Moreover, applications of \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\mathsf{R}\) where the principal formula is in focus are not preserving either (since sequents can only have one formula in focus).

We will now give a general definition of proof search trees, that will be employed in the following completeness arguments. The particular form of the proof search tree depends on the kind of countermodel one wants to obtain from a winning strategy of Refuter. In general, proof search trees are built by first applying invertible rules until a saturated sequent is encountered. Then a non-invertible rule must be applied. Since we do not know which non-invertible rule to apply to which formula, all possible non-invertible rule instances are merged into a new rule, called the choice rule. Depending on the specific form of the choice rule, different kinds of countermodels can be read off from a failed proof search. Therefore, the following general definition of proof search tree is given relative to an arbitrary choice rule. For technical reasons proof search trees will be labelled by indexed sequents \(\Gamma \Rightarrow_k \Delta\), i.e. sequents decorated with a natural number \(k\) which is called the index of the sequent. Each rule is applied to indexed sequents just as it is applied to normal (non-indexed) sequents. Every proof search tree for a sequent \(\sigma\) additionally contains an enumeration of the formulas in \(\mathsf{Cl}(\sigma)\).

The \(\mathsf{C}\)-rule replaces both the non-invertible and the focus rules. Each completeness proof we present will be relative to a suitable ‘choice’ rule \(\mathsf{C}\). For completeness with respect to triangle models, the respective choice rule will leave the index of sequents unchanged, implying that every sequent in such a proof search tree will be indexed by \(0\). Thus for that proof the index can be ignored, which we will do without further mention. The completeness proof for functional models on the other hand will make use of the index and the respective choice rule will change the index of sequents. Similarly, the enumeration of \(\mathsf{Cl}(\sigma)\) will only be used in the completeness proof for functional models.

Let \(\sigma\) be a sequent and let \(\Gamma_\sigma^{ns} \subseteq \Gamma_\sigma\) and \(\Delta_\sigma^{ns} \subseteq \Delta_\sigma\) be the sets of formulas occurring on the left side and right side of \(\sigma\), respectively, which are not saturated and are not of the form \(\larger[-1.5]\square\varphi\). Recall that \(c(\Gamma)\) denotes the complexity of \(\Gamma\) (c.f. Definition 3.2).

As a corollary of this construction we obtain the following result.

Next, we define proof search games, which are played by two players called Prover and Refuter on a given proof search tree \(\mathcal{T}\).

We will usually identify plays in \(\mathcal{G}(\mathcal{T}, \mathsf{C})\) and branches of \(\mathcal{T}\) without explicit mention. The following definitions are given for both players Prover and Refuter. We simply write Player instead.

A strategy thus tells Player how to move in every owned position. Note that each node \(u \in \mathcal{T}\) is unique, implying that strategies as defined here are aware of the history of the game. Player uses strategy \(f\) if whenever the current play is in position \(u\) and \(\exists f(u)\), then Player moves to \(f(u)\).

Given a game \(\mathcal{G}(\mathcal{T}, \mathsf{C})\) and a strategy \(f\) for Player, the strategy tree of \(f\) is the subtree of \(\mathcal{T}\) which consists of all plays that can occur when Player uses \(f\). The formal definition is as follows.

Given a sequent \(\sigma\) and a proof search tree \(\mathcal{T}\) for \(\sigma\), a refutation of \(\sigma\) is defined as follows.

It is immediate to see from the definition of the winning conditions of Refuter that the strategy trees of winning strategies for Refuter are refutations.

In the next sections we will show that when using specific choice rules \(\mathsf{C}\), refutations of \(\sigma\) correspond to countermodels for \(\sigma\), while the winning strategies for Prover correspond to \(\mathrm{nIM}\)-proofs of \(\sigma\). To show that refutations correspond to countermodels, we will make use of the following ‘canonical’ model construction. For this construction, we assume that the premises of the choice rule \(\mathsf{C}\) have been partitioned into two groups: the intuitionistic premises and the modal premises.

The construction of \(\mathcal{M}_\mathcal{R}\) reflects the idea that applying invertible rules to sequents in \(\mathcal{R}\) provides more information about the current ‘world’, while applying non-invertible rules (captured by the \(\mathsf{C}\)-rule) corresponds to taking either a modal or an intuitionistic step.

3.8.2 Completeness for Triangle Models↩︎

To show completeness of \(\mathrm{nIM}\) for triangle models, we consider the following choice rule \(\mathsf{C_t}\). A \(\larger[-1.5]\square\)-formula is a formula of the form \(\larger[-1.5]\square\varphi\) for any formula \(\varphi\). Similarly, a \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\)-formula is a formula of the form \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) for any formula \(\varphi\) and an \(\rightarrow\)-formula is a formula of the form \(\varphi \rightarrow \psi\) for any formulas \(\varphi, \psi\).

We have established that winning strategies for Prover correspond to \(\mathrm{nIM}\)-proofs and winning strategies for Refuter to (triangle) countermodels. In order to obtain completeness, we require that the game \(\mathcal{G}(\mathcal{T}, \mathsf{C_t})\) is determined, which means that exactly one of the two players has a winning strategy. It is well-known that proof search games like \(\mathcal{G}(\mathcal{T}, \mathsf{C_t})\) can be reformulated as Gale–Steward games. In fact, since Gale–steward games only permit infinite plays, it suffices to extend every finite branch in the proof search tree \(\mathcal{T}\) by an infinite sequence of nodes labelled by the same sequent as the leaf and determine that such plays are then won by Prover if the suffix contains only axioms and by Refuter otherwise. The resulting game is then a Gale–Steward game. It is a standard result in non-wellfounded proof theory that the set of winning plays for each player in such a game is Borel. In fact, the winning sets belongs to a low level of the Borel hierarchy, namely \(\Delta_3\). Therefore we may apply the following theorem.

To prove that the set of winning plays for each player is Borel is out of the scope of this thesis. We would require to build a Büchi automaton which recognizes the good branches in the adapted proof search tree. For a precise construction, see [24].

3.8.3 Completeness for Functional Models↩︎

To obtain completeness with respect to functional models, it suffices to replace the choice rule \(\mathsf{C_t}\) in the previous argument by a suitable choice rule \(\mathsf{C_f}\). The design of \(\mathsf{C_f}\) will guarantee that the canonical model (relative to \(\mathsf{C_f}\)) is functional. In the completeness proof for triangle models, when we reached a saturated sequent, the choice rule \(\mathsf{C_t}\) created multiple premises corresponding to intuitionistic and modal successors of the current world. Here, when we reach a saturated sequent with multiple \(\larger[-1.5]\square\)-formulas on the right side, only one of these formulas can be used to create a modal successor, since we are building a functional model. This leaves the question how to deal with the remaining \(\larger[-1.5]\square\)-formulas on the right side, which also have to be falsified. In the proof of Theorem 3.1, whenever a world in an \(\mathcal{M}\)-induced structure had multiple \(\larger[-1.5]\square\)-defects, the issue of falsifying all of them was resolved by adding copies of that world as intuitionistic successors and resolving one \(\larger[-1.5]\square\)-defect in each of these copies. A similar strategy will work in the completeness proof here. Namely, the choice rule \(\mathsf{C_f}\) will pick exactly one \(\larger[-1.5]\square\)-formula on the right (if one exists) to create a modal successor, while the other \(\larger[-1.5]\square\)-formulas generate intuitionistic successors, where they can be falsified as well. To keep track of which right \(\larger[-1.5]\square\)-formula has to be ‘taken care of’ at a particular step, the proof search tree will make use of the indexes introduced earlier.

Recall that a proof search tree for \(\sigma\) contains an enumeration \(e\) of the formulas of \(\mathsf{Cl}(\sigma)\). Suppose \(\lvert \mathsf{Cl}(\sigma) \rvert = m\).

The choice rule \(\mathsf{C_f}\) thus chooses the \(k\)-th formula in the enumaration of \(\sigma\) to create a modal successor if the \(k\)-th formula is a \(\larger[-1.5]\square\)-formula and present on the right side of the conclusion. Otherwise, the world \(w\) containing the conclusion of \(\mathsf{C_f}\) does not have a modal successor. Moreover, \(\mathsf{C_f}\) adds an intuitionistic successor which is a copy of \(w\) where the index is increased. Note that the premise \(\Gamma_\tau \Rightarrow_{(k+1)_m}\Delta_\tau\) differs from the conclusion only in the index and is therefore saturated, implying that it is the conclusion of another \(\mathsf{C_f}\)-instance, where the corresponding world either has no modal successor or a modal successor falsifying a different \(\larger[-1.5]\square\)-formula.

Combining these results, once again together with determinacy of the game, yields completeness of \(\mathrm{nIM}\) with respect to functional models. The proof of the following theorem is analogous to the proof of Theorem 3.10.

3.8.4 Translating Non-Wellfounded into Cyclic Proofs↩︎

With completeness of \(\mathrm{nIM}\) for triangle and functional models at hand, we now show that \(\mathrm{cIM}\) is complete by translating non-wellfounded proofs into cyclic proofs. Due to the presence of the focus annotation, the translation is relatively straightforward.

Note that the existence of a successful repetition in \(\rho\) implies the existence of a lowermost successful repetition in \(\rho\).

The following then follows immediately from Lemma 3.31.

Completeness of \(\mathrm{cIM}\) then follows as a corollary of Theorem 3.10, Theorem 3.12 and Lemma 3.32.

Theorem 3.7 and Theorem 3.13 together provide an alternative proof of Theorem 3.1 that \(\mathbf{IM}= \mathbf{IM_t} = \mathbf{IM_f}\).

3.9 Conclusion↩︎

We have introduced a simple intuitionistic dynamic logic called intuitionistic master modality. The following summarizes the results established in this chapter.

1. We have presented three classes of models to evaluate formulas of \(\mathsf{IM}\), namely dynamic models, triangle models and functional models.

2. Theorem 3.1 shows that all three classes generate the same set of validities.

3. We have presented a sound and complete axiomatization for \(\mathsf{IM}\) and established several properties about derivations, such as the Deduction Theorem. The presented completeness proof closely follows the completeness proof for a multi–modal version of \(\mathsf{IM}\) presented by Marti [26] (who uses a different axiomatization) and yields the finite model property for \(\mathsf{IM}\) as well as decidability.

4. We have developed a sound and complete cyclic calculus for \(\mathsf{IM}\). Completeness was established via a proof search argument, whose robustness was illustrated by giving an alternative proof of Theorem 3.1.

That the language of \(\mathsf{IM}\) without the master modality cannot distinguish between dynamic and triangle models has already been observed by other authors, for example Litak and Visser [65]. Adding the master modality to the language does not impact this result, as in order to evaluate \(\larger[-1.5]\square\) and \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\), the truth conditions of dynamic models consider the same worlds as when one takes the closure under triangle confluence. The result that \(\mathsf{IM}\) cannot distinguish between dynamic and functional models is new and perhaps more surprising. However, this is once again caused by the evaluation of the modalities, where in order to evaluate a \(\larger[-1.5]\square\)-formula at a world \(w\), one has to consider all modal successors of all intuitionistic successors of \(w\). This implies that it does not matter whether we consider models with one or multiple modal successors, as we can always add more intuitionistic successors to obtain additional modal successors. A consequence of Theorem 3.1 is that stronger confluence conditions are needed when we want to obtain an interesting intuitionistic linear temporal logic, namely conditions that allow us to evaluate modalities by only looking at the modal successor of the current world. This will be done in Chapter 5, where we will study dynamic models where the modal accessibility relation is a total function \(f\) which is order-preserving.

Our observations regarding the three classes of models naturally lead to the following question.

Over such models \((W, \leq, f, V)\) if \(f\) is a total function, then note that for any world \(w \in W\) and any \(v \geq w\), \(f(w) = f(v)\). In other words, the entire intuitionistic tree rooted at \(w\) has the same modal successor. This implies that the modalities satisfy classical principles like the boxed law of excluded middle: \(\larger[-1.5]\squarep \vee \neg \larger[-1.5]\squarep\) is valid.¹⁴ A similar phenomenon will be encountered in Chapter 4 when we combine triangle confluence with frame conditions.

The completeness proof for \(\mathrm{IM_H}\) demonstrates a rather straightforward adaptation of the mathematical methods used to obtain completeness for classical modal logic with the master modality to the intuitionistic case. In fact, the presented canonical model construction combines the canonical model construction for intuitionistic logic (see [46]) with the standard technique to handle the master modality from the classical realm (see e.g. [64]). Due to the lack of strong confluence properties, we can directly define finite canonical models for fragments of the language. As we will see in Chapter 6, this is no longer possible when stronger confluence conditions are considered.

The developed cyclic calculus \(\mathrm{cIM}\) for \(\mathsf{IM}\) is an extension of a multi-succedent calculus for \(\mathsf{IPL}\) with rules for \(\larger[-1.5]\square\) and \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\). Many classical techniques, such as focus annotations and proof search games, are directly applicable to \(\mathsf{IM}\) as demonstrated in this chapter. The main difference between the intuitionistic and the classical case is that the presence of the intuitionistic implication complicates the proof search argument, as we have to deal with falsifying \(\rightarrow\)-formulas in intuitionistic successors and \(\larger[-1.5]\square\)-formulas in modal successors, as opposed to only dealing with the latter in classical modal logic with the master modality (for an in depth study of cyclic proof systems for classical modal logic with the master modality, see the PhD thesis of Rooduijn [63]; for proof search arguments for classical common knowledge logics, see [69]). The increase in the mathematical difficulty is not substantial though, once again due to the lack of strong enough confluence conditions, which allows us to falsify \(\rightarrow\)- and \(\larger[-1.5]\square\)-formulas independently of one another. The system \(\mathrm{cIM}\) is well-behaved: it is analytic and does not require a cut rule; furthermore it also does not require additional structure on sequents such as labels or nesting, and has a simple success condition on cyclic branches. Our work therefore lies the foundation for studying the proof theory of \(\mathsf{IM}\) in more details. In particular, the following questions are left open.

Studer showed that classical common knowledge logics does not have Craig interpolation and hence also not uniform and Lyndon interpolation [70]. The provided counterexample however requires the language to feature at least two agents, which implies that there is hope for obtaining Craig interpolation for \(\mathsf{IM}\). The cyclic system \(\mathrm{cIM}\) is thereby a good starting point for studying this problem from a proof theoretic point of view. Another open proof theoretic question concerns the problem of cut elimination.

In recent work, Sierra-Miranda and Studer showed cut elimination for a non-wellfounded proof system for classical modal logic with the master modality [71]. The similarities between their system and \(\mathrm{nIM}\) suggest that their proof may be adaptable to the intuitionistic case.

4 Intuitionistic Common Knowledge Logic↩︎

4.1 Introduction↩︎

Epistemic logic describes a family of logical systems used to reason about knowledge and belief of agents as well as studying various notions of group knowledge. Traditionally, epistemic logics are devised as (classical) modal logics. Given a finite set of agents \(\mathsf{A}\), the language of epistemic logic extends propositional logic with modal operators \(\mathsf{K}_i\) for \(i \in \mathsf{A}\) which are interpreted as the knowledge operator of agent \(i\). Thus a formula of the form \(\mathsf{K}_i \varphi\) is read as ‘agent \(i\) knows that \(\varphi\)’. Of particular interest is the study of nesting of knowledge among different agents, i.e. what agents know about the knowledge of other agents. For example, the formula \(\mathsf{K}_i \mathsf{K}_j \neg \mathsf{K}_i \neg \varphi\) expresses that agent \(i\) knows, that agents \(j\) knows, that agent \(i\) considers \(\varphi\) to be possible. Such kind of reasoning naturally leads to the study of notions of group knowledge. Perhaps the most famous example of such a notion is common knowledge. Informally, among a group of agents a formula \(\varphi\) is common knowledge if every agent knows \(\varphi\) and every agent knows, that every agent knows \(\varphi\), and so on. Write \(\mathsf{E}\varphi\) for ‘everybody (in the group) knows \(\varphi\)’. Formally, \(\mathsf{E}\varphi\) is defined as \[\mathsf{E}\varphi \mathrel{\vcenter{:}}= \bigwedge_{i \in \mathsf{A}} \mathsf{K}_i \varphi.\] As usual, let \(\mathsf{E}^0 \varphi \mathrel{\vcenter{:}}= \varphi\) and \(\mathsf{E}^{n+1} \varphi \mathrel{\vcenter{:}}= \mathsf{E}\mathsf{E}^n \varphi\). Then ‘common knowledge of \(\varphi\)’ is equivalent to the infinite conjunction \[\bigwedge_{k < \omega} E^k \varphi.\] In order to express common knowledge, we use a new operator \(\mathsf{C}\) where \(\mathsf{C}\varphi\) is given as the greatest fixed point of the propositional function \(x \mapsto \varphi \wedge \mathsf{E}x\). Epistemic logic with common knowledge is called common knowledge logic (\(\mathsf{CK}\)) and has found applications in computer science, such as in the study of distributed systems (see e.g. [72]).

Epistemic logic over an intuitionistic base logic, called intuitionistic epistemic logic has been studied at least since the 1990’s and the work by Williamson [38]. In the last decade, several systems of intuitionistic epistemic logic have been developed. These systems fall into two general categories. The first category aims to develop systems of intuitionistic epistemic logic to study knowledge from the point of view of intuitionism. Such systems usually attempt to provide a BHK interpretation of knowledge. In this category falls the work of Williamson [38], the intuitionistic epistemic logic IEL developed by Artemov and Protopopescu [8], as well as recent work about logics of knowing-wh (which are epistemic logics featuring operators to capture different types of knowledge such as knowing-how) and explicit interpretations of intuitionistic logic by Wang et al. (see e.g. [73]–[77]). The second category is primarily motivated by mathematical reasons as well as applications to computer science and studies intuitionistic modal logics, where the \(\larger[-1.5]\square\)-operator is interpreted as a knowledge operator and which are extended by fixed point operators for group knowledge such as common knowledge or distributed knowledge. In particular, logics from this category do not attempt to give a BHK reading of knowledge and largely treat knowledge classically. To this category belongs most notably the intuitionistic common knowledge logic \(\mathsf{ICK}\), developed by Jäger and Marti [25]. Jäger and Marti focus on the mathematical theory of \(\mathsf{ICK}\) by developing a sound and complete axiomatization and a sound and complete sequent calculus with induction rule. Moreover, they also study intuitionistic epistemic logic with distributed knowledge [27], which is further studied in [28], [29]. \(\mathsf{ICK}\) is a multi-modal version of the logic \(\mathsf{IM}\) studied in the previous chapter. Given a finite set of agent names \(\mathsf{A}\), the language features a \(\larger[-1.5]\square\)-operator for each agent \(i \in \mathsf{A}\), written as \(\mathsf{K}_i\). In that setting the master modality becomes more expressive, as it is no longer simply a reflexive transitive closure operator of \(\larger[-1.5]\square\), but instead of \(\mathsf{E}\). For example, it is easily verified that over triangle models where the modal accessibility relation is reflexive and transitive, the master modality is definable in terms of \(\larger[-1.5]\square\). This is not the case in the multi-modal setting of \(\mathsf{ICK}\) with common knowledge. Formulas of \(\mathsf{ICK}\) are evaluated on triangle models, satisfying standard frame conditions such as reflexive triangle models, S4 triangle models and S5 triangle models. Jäger and Marti provide a sequent calculus for \(\mathsf{ICK}\) over the class of triangle and over the class of reflexive triangle models, but do not extend their work to the S4 and S5 case [25]. Furthermore, Marti also provides an axiomatization [69]. The presented sequent calculus characterizes common knowledge via an induction rule, and features a cut rule which is used in the completeness proof. Whether cut elimination is possible is not discussed, however in a similar calculus for classical common knowledge logic presented by Alberucci and Jäger [66], the cut rule cannot be eliminated (at least for the logic over S5 models) and no restriction to analytic cuts is possible, which sheds doubt on whether such an enterprise is possible for \(\mathsf{ICK}\).

In this chapter we aim to use the cyclic calculus developed in Chapter 3 to build a uniform proof theory for \(\mathsf{ICK}\) evaluated over the classes of triangle models, reflexive triangle models, S4 triangle models and S5 triangle models. To that end we will first show how to translate \(\mathrm{cIM}\) into a multi-modal version and then introduce rules for the frame conditions. As it turns out, the adaptation of the calculus to account for reflexive and S4 models is straightforward by adding the standard modal rules for reflexivity and transitivity to the calculus. Moreover, completeness can be established by following the proof search argument introduced in the previous chapter with only minor changes to the ‘choice rule’. The case for S5 is more difficult. First, the combination of triangle confluence with S5 frame conditions results in rather strange models where given a world \(w\), the entire intuitionistic tree rooted at \(w\) belongs to the equivalence class of \(w\) under \(R\). In such a setting knowledge essentially reduces to classical knowledge, which satisfies classical principles such as the ‘boxed law of excluded middle’: for every proposition \(p\), the formula \(\mathsf{K}_i p \vee \neg \mathsf{K}_i p\) is valid. Second, the S5 conditions lead to the standard proof theoretical problems already encountered for classical S5 modal logic: we will show that the extension of \(\mathrm{cIM}\) with rules for the frame conditions is not cut-free complete. This could perhaps be circumvented by passing to labelled or nested sequents, but we will follow the method presented in a joint publication with Rooduijn [41] on classical common knowledge logic over S5 and instead extend the calculus with a cut rule. Analytic completeness is then established via a canonical model construction by restricting applications of the cut rule to analytic cuts. Importantly, the extension with the cut rule allows us to prove completeness directly; a detour to a non-wellfounded system as for \(\mathrm{cIM}\) is no longer required. It is in fact unclear whether the proof search argument can be adapted in the presence of the cut rule. Furthermore, we investigate the relationship between \(\mathsf{ICK}\) over S5 and \(\mathsf{CK}\) over S5 by developing a translation from \(\mathsf{CK}\) into \(\mathsf{ICK}\) and we show that proof search in the cyclic calculus for the S5 case can be automated by reducing the problem of finding proofs to the problem of solving a certain parity game. Finally, combining the translation and parity game, we show that the problem of finding proofs in the cyclic calculus for \(\mathsf{ICK}\) over S5 triangle models is ExpTime-complete.

4.2 Syntax and Semantics↩︎

Let \(\mathsf{A}\) be a finite set of agent names. The language \(\mathcal{L}_\mathsf{ICK}\) extends \(\mathcal{L}_\mathsf{IPL}\) by modal operators \(\mathsf{K}_i\) for \(i \in \mathsf{A}\) and the fixed point operator \(\mathsf{C}\), where \(\mathsf{C}\varphi\) is characterized as the greatest fixed point of the propositional function \(x \mapsto \varphi \wedge \mathsf{E}x\). Formulas of \(\mathcal{L}_\mathrm{ICK}\) are defined by the following grammar in Backus-Naur form: \[\varphi ::= \bot \, \lvert \, p \, \lvert \, \varphi \wedge \varphi \, \lvert \, \varphi \vee \varphi \, \lvert \, \varphi \rightarrow \varphi \, \lvert \, \mathsf{K}_i \varphi \, \lvert \, \mathsf{C}\varphi.\] where \(p \in \mathsf{Prop}\) and \(i \in \mathsf{A}\). The modal operator \(K_i\) is the knowledge operator of agent \(i\): \(\mathsf{K}_i \varphi\) is read as ‘agent i knows \(\varphi\)’. The modal operator \(\mathsf{C}\) is the common knowledge operator: \(\mathsf{C}\varphi\) is read as ‘\(\varphi\) is common knowledge (among the agents in \(\mathsf{A}\))’. The modality \(\mathsf{E}\), read as ‘everybody knows’, is defined by \[\mathsf{E}\varphi \mathrel{\vcenter{:}}= \bigwedge_{i \in \mathsf{A}} K_i \varphi.\] Due to the presence of multiple knowledge operators, the definition of the closure of a formula (c.f. Definition 3.1) is adjusted as follows.

Additionally, we define the negation closure of a formula, which will be used to treat \(\mathsf{ICK}\) over S5 models.

The following lemma is easily verified by an induction on the structure of formulas.

The complexity of a formula is defined as follows.

Formulas of \(\mathcal{L}_\mathrm{ICK}\) are evaluated over triangle models equipped with a modal accessibility relations for each agent. We follow [25] and call such models (intuitionistic) epistemic models.

Given an epistemic model \(\mathcal{M}=(W, \leq, \{R_i\}_{i \in \mathsf{A}}, V)\), define the relation \[R := \bigcup_{i \in A} R_i\] and let \(R^*\) be the reflexive and transitive closure of \(R\).

Since only triangle models are studied in this chapter, we will supress the index \(t\) in \(\models_t\) and simply write \(\models\). The notions of satisfiability and validity are defined as before. Since \(\mathsf{ICK}\) is simply a multi-modal version of \(\mathsf{IM}\) it is obvious that the monotonicity lemma (c.f. Lemma 3.2) still holds.

We will study \(\mathcal{L}_\mathsf{ICK}\) over the classes of epistemic models, reflexive epistemic models, S4 epistemic models and S5 epistemic models. The definition of these classes of models is a generalization of Definition 2.20.

For simplicity we will usually refer to reflexive epistemic models simply as reflexive models throughout this chapter, and similarly for S4 and S5 epistemic models.

Note that \(\mathbf{ICK} \subseteq \mathbf{ICK_T} \subseteq \mathbf{ICK_{S4}} \subseteq \mathbf{ICK_{S5}}\). The following lemma shows that the logics \(\mathbf{ICK}\), \(\mathbf{ICK_T}\) and \(\mathbf{ICK_{S4}}\) contain the standard validities of classical epistemic logic regarding the knowledge and common knowledge operators (see e.g. [64] for axiomatizations of classical common knowledge logics over different frame conditions). The proof is by standard semantical arguments using the frame conditions that the models of the relevant logic satisfy and is omitted.

The logic \(\mathbf{ICK_{S5}}\), on the other hand, contains some validities that are rather unexpected in the context of intuitionistic logic. The combination of S5 frame conditions with triangle confluence has a strong impact on the models and thus on the resulting logic. Given worlds \(w\) and \(v\) if \(w \leq v\), then by reflexivity \(v \mathrel{R_i} v\) and so by triangle confluence \(w \mathrel{R_i} v\) for all \(i \in \mathsf{A}\). In other words, the intuitionistic order is a subset of each modal accessibility relation: \({\leq} \subseteq {R_i}\) for each \(i \in \mathsf{A}\) (note that this already holds for S4 models). Moreover, by symmetry, we obtain that \(v \mathrel{R_i} w\), implying that given \(w\), the entire intuitionistic tree rooted at \(w\) belongs to the equivalence class of \(w\) under the equivalence relation induced by \(R_i\).

This leads to an interesting observation. Since every intuitionistic successor \(v\) of \(w\) belongs to the equivalence class of \(w\), every world accessible from \(v\) is accessible from \(w\) and vice versa, implying that for \(w \leq v\), \(w \models \mathsf{K}_i \varphi\) if and only \(v \models \mathsf{K}_i \varphi\). Moreover, since truth is persistent in \(\leq\) and falsity is persistent in \(\geq\), implications with a ‘boxed’ antecedent (i.e. formulas of the form \(\mathsf{K}_i \varphi \rightarrow \psi\) or \(\mathsf{C}\varphi \rightarrow \psi\)) are evaluated classically, as shown in the following lemma.

As a corollary we obtain that \(\mathsf{ICK}\) over S5 models satisfies a boxed version of the law of excluded middle: for any formula \(\varphi\) the formula \(\mathsf{K}_i \varphi \vee \neg \mathsf{K}_i \varphi\) is valid. The proof is omitted.

4.3 Cyclic Calculi↩︎

This section introduces four sequent calculi for \(\mathsf{ICK}\) with the aim to capture the validities of \(\mathsf{ICK}\) over the classes of all epistemic models, reflexive models, S4 models and S5 models. Each calculus shares the same set of basic rules as \(\mathrm{cIM}\) and additional rules for the modalities, which differ depending on which frame condition ought to be captured. The calculus for \(\mathsf{ICK}\) over the class of epistemic models is denoted \(\mathrm{cICK}\) and is simply a multi-modal version of \(\mathrm{cIM}\). The calculi \(\mathrm{cICK}_{\mathrm{T}}\), \(\mathrm{cICK}_{\mathrm{S4}}\) and \(\mathrm{cICK}_{\mathrm{S5}}\) are modular extensions of \(\mathrm{cICK}\). The focus lies mostly on \(\mathrm{cICK}_{\mathrm{S5}}\), which is the extension of \(\mathrm{cICK}\) by two rules for the modalities and, additionally, the cut rule and a special rule dealing with implications \(\varphi \rightarrow \psi\) where \(\varphi\) is a boxed formula. We begin by introducing the basic components of the calculi. Since \(\mathrm{cICK}\) and its extensions are multi-modal versions of \(\mathrm{cIM}\), most definitions are identical or similar to the case of \(\mathsf{IM}\); for convenience we briefly repeat the basic definitions here and refer the reader to Chapter 3, Section 3.6 for further details.

An annotated formula is a tuple \((\varphi, a)\), written \(\varphi^a\), where \(\varphi \in \mathcal{L}_\mathsf{ICK}\) and \(a \in \{\mathsf{u}, \mathsf{f}\}\). The annotation \(\mathsf{u}\) designates that the formula is unfocused and \(\mathsf{f}\) that the formula is in focus.

We denote sequents by \(\sigma\) and write \(\Gamma_\sigma\) and \(\Delta_\sigma\) for the left and right side of \(\sigma\), respectively. The interpretaion of a sequent \(\sigma\) is the formula \(\sigma^I \mathrel{\vcenter{:}}= \bigwedge \Gamma_\sigma^- \rightarrow \bigvee \Delta_\sigma^-\). The closure \(\mathsf{Cl}(\sigma)\) of a sequent \(\sigma\) is defined as \(\mathsf{Cl}(\sigma) \mathrel{\vcenter{:}}= \mathsf{Cl}(\Gamma_\sigma) \cup \mathsf{Cl}(\Delta_\sigma)\). Additionally, the negation closure of a sequent \(\sigma\) is defined as \(\mathsf{Cl}^\neg (\sigma) \mathrel{\vcenter{:}}= \mathsf{Cl}^\neg(\Gamma_\sigma) \cup \mathsf{Cl}^\neg (\Delta_\sigma)\). Each calculus consists of all of the basic rules depicted in Table 5 and additionally some of the rules depicted in Table 6.

For every rule in Table 5 as well the rules \(\mathsf{CL}\), \(\mathsf{CR}\) and \(\mathsf{K_i}{\rightarrow}\), the distinguished formula in the conclusion is called principal and the distinguished formulas in the premises are its residuals. For example, in the rule \(\mathsf{\mathsf{C}L}\) the principal formula is \(\mathsf{C}\varphi^\mathsf{u}\) and the residual formulas are \(\varphi^\mathsf{u}\) and \(\mathsf{K}_i \mathsf{C}\varphi^\mathsf{u}\) for \(i \in \mathsf{A}\). The rule \(\mathsf{cut}\) has no principal formulas, while both distinguished formulas in the premises are residual. These distinguished formulas are called the cut formulas. For the knowledge rules for agent \(i\) (i.e. \(\mathsf{K_i}\), \(\mathsf{T_i}\), \(\mathsf{S4_i}\) and \(\mathsf{S5_i}\)) every formula in the conclusion is principal and every formula in the premise is the residual of the corresponding principal formula. Formulas in \(\Sigma, \Pi\) have no residual formulas. All other formulas occurring in a rule are called side formulas.

4.3.1 Cyclic Proofs↩︎

We define the notion of cyclic proof for each system introduced above. Once again, the definitions simply adapt the definitions for \(\mathsf{IM}\) to the case for \(\mathsf{ICK}\).

Let \(\mathsf{P} \in \{\mathrm{cICK}, \mathrm{cICK}_\mathrm{T}, \mathrm{cICK}_\mathrm{S4}, \mathrm{cICK}_\mathrm{S5}\}\). A \(\mathsf{P}\)-pre-proof of a sequent \(\sigma\) is a finite tree \(\pi\) labeled by sequents according to the rules of \(\mathsf{P}\) and whose root is labeled by \(\sigma\).

Given a pre-proof \(\pi\), a pair of nodes \((u,v)\) of \(\pi\) is a repetition if \(u \not = v\), there exists a path from \(u\) to \(v\) and both nodes are labeled by the same sequent. A repetition \((u,v)\) is successful if the path from \(u\) to \(v\) is successful.

An example of a cyclic proof showing that \(\mathsf{C}\varphi^\mathsf{u}\Rightarrow \mathsf{C}(\varphi \vee \psi)^\mathsf{u}\) is \(\mathrm{cICK}\)-provable is displayed in Figure 9, where it is assumed that \(\mathsf{A}=\{1,2\}\). By inspecting the proof it is obvious that the example can be generalized to \(n\) agents for any natural number \(n>0\). Note that the presented calculi combine standard rules for \(\mathsf{IPL}\) and for common knowledge logic (see for example [41], [47]). The only exception is the calculus \(\mathrm{cICK}_{\mathrm{S5}}\) which features the rule \({\rightarrow}\mathsf{K_i}\). This rule formalizes the observation from Lemma 4.3 that implications of the form \(\mathsf{K}_i \varphi \rightarrow \psi\) behave classically. Observe that the rule is only applicable if the principal formula is of the form \(\mathsf{K}_i \varphi \rightarrow \psi\). It is therefore a special case of the classical right implication rule. We now give two examples showing that \(\mathrm{cICK}_{\mathrm{S5}}\) proves the boxed law of excluded middle for \(\mathsf{K}_i\) and \(\mathsf{C}\), which illustrate how the rule \({\rightarrow}\mathsf{K_i}\) can be used to prove classical principles.

Example 4.2 hints towards the fact that \(\mathrm{cICK}_\mathsf{S5}\) is not cut-free complete. This does not come as a surprise, given that it is well-known that classical S5 modal logic does not have a cut-free (plain) sequent calculus. A famous counterexample in the classical realm is the formula \(p \rightarrow \Box \Diamond p\). In the intuitionistic setting, \(\Box\) and \(\Diamond\) are not interdefinable, therefore our language cannot express \(\Diamond\). However, we may still use the formula as a counterexample, by identifying \(\Box\) with \(\mathsf{K}_i\) and \(\Diamond\) with \(\neg \mathsf{K}_i \neg\). An easy computation shows that \(\neg \mathsf{K}_i \neg\) is not evaluated as a \(\Diamond\), but instead its truth conditions are as follows: \(\mathcal{M}, w \models \neg \mathsf{K}_i \neg \varphi\) if and only if there exist \(u,u' \in W\) with \(w \mathrel{R_i} u\), \(u \leq u'\) and \(\mathcal{M}, u' \models \varphi\). Therefore the following holds.

Note that the cut formulas used in the cyclic proof in Example 4.2 belong to the negation closure of the root sequent. Similarly, the sequent \(p^\mathsf{u}\Rightarrow K_i \neg K_i \neg p^\mathsf{u}\) is provable by using \(\neg K_i \neg p^\mathsf{u}\) as cut formula, which also belongs to the negation closure of the root sequent. Following this observation we will show that \(\mathrm{cICK}_\mathsf{S5}\) is complete when the cut-rule is restricted to analytic cuts, i.e. instances of \(\mathsf{cut}\) where the cut formula belongs to the negation closure of the root sequent. Therefore we will still obtain analytic completeness for \(\mathrm{cICK}_\mathsf{S5}\).

4.4 Soundness↩︎

This section establishes the soundness of all cyclic systems introduced before. We follow the same strategy as for the soundness proof of \(\mathrm{cIM}\) in Section 3.7, but some small adaptions are needed. The following lemma is routine (c.f. Lemma 3.13).

Let \(\sigma\) be a sequent with a formula in focus, i.e. \(\Delta_\sigma\) contains a formula of the form \(\mathsf{K}_i^j \mathsf{C}\varphi^\mathsf{f}\) for \(j \in \{0,1\}\). Denote by \(\sigma(n)\) the sequent \(\Gamma_\sigma \Rightarrow \Delta_\sigma, \mathsf{K}_i^j \mathsf{E}^n \varphi^\mathsf{u}\), i.e. the sequent expanding the right side of \(\sigma\) by the formula \(\mathsf{K}_i^j \mathsf{E}^n \varphi^\mathsf{u}\). The following lemma is then proven as Lemma 3.24.

Therefore we may define the following measure,

\[\mu(\sigma) := \min \{n < \omega \, \mid \, \sigma(n) \text{ is invalid}\}\]

and then prove a strengthening of Lemma 4.5.

Soundness for each cyclic calculus then follows by the same argument as used to prove Theorem 3.7.

4.5 Completeness↩︎

This section establishes completeness of all cyclic calculi introduced above. Completeness of \(\mathrm{cICK}, \mathrm{cICK}_\mathrm{T}\) and \(\mathrm{cICK}_\mathrm{S4}\) for their respective classes of models will be shown by using the proof search technique introduced in Section 3.5. Since the resulting proofs are very similar, only brief sketches are provided. The main part of this section is the completeness proof for \(\mathrm{cICK}_\mathsf{S5}\).

4.5.1 Completeness for Epistemic, Reflexive and S4 Models↩︎

In order to prove completeness of \(\mathrm{cICK}\), \(\mathrm{cICK}_\mathsf{T}\) and \(\mathrm{cICK}_\mathsf{S4}\), we define corresponding non-wellfounded calculi \(\mathsf{nICK}\), \(\mathsf{nICK_T}\) and \(\mathsf{nICK_{S4}}\) following the definitions in Section 3.6. We then employ the same proof search strategy, where the definition of a saturated sequent is adapted from the definition for \(\mathrm{nIM}\) in the obvious way. Proof search trees are defined in Definition 3.27 (by replacing \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\) with \(\mathsf{C}\)). Neither the indexes nor the enumeration of the formulas in \(\mathsf{Cl}(\sigma)\) are needed and so are ignored henceforth. Proof search games are defined as for \(\mathrm{nIM}\). The definition of the canonical model has to be adapted to the multi-modal case: given a choice rule \(\mathsf{C}\), we assume that the modal premises are partitioned into \(\lvert \mathsf{A}\rvert\) groups. Then replace clause 3. in Definition 3.33 by the following clause.

1. For each \(i \in \mathsf{A}\), \(R_i \subseteq W \times W\) is such that

   \(w \mathrel{R_i} v\) iff there exists \(s \in w\) and \(t \in v\) such that \(s\) is the conclusion and \(t\) a modal premise from group \(i\) of the same \(\mathsf{C}\)-rule instance.

The calculus \(\mathsf{nICK}\) is simply a multi-modal version of \(\mathrm{nIM}\), so for the choice rule a slightly adapted version of \(\mathsf{C_t}\) suffices to obtain completeness, namely the rule \[\infer[\mathsf{C_t'}]{\Pi, \{\mathsf{K}_i \Gamma_i\}_{i \in \mathsf{A}} \Rightarrow \{(\varphi_i \rightarrow \psi_i)^{\mathsf{u}}\}_{i=0}^l,\{\{\mathsf{K}_i\chi^{a_{i_j}}_{i_j}\}_{j=0}^{m_i}\}_{i \in \mathsf{A}}, \Sigma}{\Pi, \{\mathsf{K}_i \Gamma_i\}_{i \in \mathsf{A}}, \varphi^\mathsf{u}_0 \Rightarrow \psi^{\mathsf{u}}_0 &\dotsm & \Pi, \{\mathsf{K}_i \Gamma_i\}_{i \in \mathsf{A}}, \varphi^\mathsf{u}_l \Rightarrow \psi^{\mathsf{u}}_l & \{ \{\Gamma_i \Rightarrow \chi^{b_{i_j}}_{i_j}\}_{j = 0}^{m_i}\}_{i \in \mathsf{A}}}\] where the annotations \(b_{i_j}\) are equal to \(\mathsf{f}\) whenever the underlying formula \(\chi_{i_j}\) is a \(\mathsf{C}\)-formula, and equal to \(\mathsf{u}\) otherwise. Moreover, we require that \(\Pi\cup\Sigma\) contains no \(\mathsf{K}_i\)-formulas for any \(i \in \mathsf{A}\) and that \(\Sigma\) contains no \(\rightarrow\)-formulas. The modal premises are those of the form \(\Gamma_i \Rightarrow \chi^{b_{i_j}}_{i_j}\), where \(\{\Gamma_i \Rightarrow \chi_{i_j}^{b_{i_j}}\}_{j = 0}^{m_i}\) is group \(i\) and the others are the intuitionistic premises. In case the conclusion of a \(\mathsf{C_t}'\)-instance has no \(\rightarrow\)- or \(\mathsf{K}_i\)-formulas on the right-hand side for \(i \in \mathsf{A}\), then we stipulate that \(l = -1\) or \(m_i=-1\), respectively.

Observe that the conclusion and each modal premise form an instance of the rule \(\mathsf{K_i}\). It is then routine to show that winning strategies for Prover correspond to \(\mathrm{cICK}\)-proofs and winning strategies for Refuter to refutations. Finally, when proving that refutions induce countermodels, as in the proof of Proposition 3.8, we take the canonical model induced by the refutation, close it under triangle confluence¹⁶ and then show that it falsifies the root sequent of the refutation. The proof is similar to the proof of Proposition 3.8.

For \(\mathsf{nICK_T}\) the definition of saturated sequent has to be extended with the following clause:

1. If \(\mathsf{K}_i \varphi^\mathsf{u}\in \Gamma\), then \(\varphi^\mathsf{u}\in \Gamma\).

Note that the rule \(\mathsf{T_i}\) is invertible. Hence the same choice rule \(\mathsf{C_t}'\) can be used and when proving that refutations induce a countermodel, we only have to close the modal relations of the canonical model under reflexivity. The additional saturation clause 8. ensures that for any world \(w\) of the canonical model \(\mathcal{M}\) and any formula \(\mathsf{K}_i \varphi\) holds that if \(\mathcal{M}, w \models \mathsf{K}_i \varphi\), then \(\mathcal{M}, w \models \varphi\).

Finally, for \(\mathsf{nICK_{S4}}\) we employ the following choice rule \[\infer[\mathsf{C_{S4}}]{\Pi, \{\mathsf{K}_i \Gamma_i\}_{i \in \mathsf{A}} \Rightarrow \{(\varphi_i \rightarrow \psi_i)^{\mathsf{u}}\}_{i=0}^l,\{\{\mathsf{K}_i\chi^{a_{i_j}}_{i_j}\}_{j=0}^{m_i}\}_{i \in \mathsf{A}}, \Sigma}{\Pi, \{\mathsf{K}_i \Gamma_i\}_{i \in \mathsf{A}}, \varphi^\mathsf{u}_0 \Rightarrow \psi^{\mathsf{u}}_0 &\dotsm & \Pi, \{\mathsf{K}_i \Gamma_i\}_{i \in \mathsf{A}}, \varphi^\mathsf{u}_l \Rightarrow \psi^{\mathsf{u}}_l & \{ \{\mathsf{K}_i \Gamma_i \Rightarrow \chi^{b_{i_j}}_{i_j}\}_{j = 0}^{m_i}\}_{i \in \mathsf{A}}}\] with the same conditions as for \(\mathsf{C_t}'\). Note that the only difference to \(\mathsf{C_t}'\) is that the applications of \(\mathsf{K_i}\) were replaced by applications of \(\mathsf{S4_i}\). When proving that refutations induce countermodels, it then suffices to close the modal accessibility relations of the canonical model induced by the refutation under reflexivity and transitivity. Note that since formulas in \(\mathsf{K}_i \Gamma\) are preserved when moving to a modal premise of group \(i\), closing the modal accessibility relation \(R_i\) under transitivity does not lead to the failure of any formula in \(\mathsf{K}_i \Gamma\). Therefore we obtain completeness for the non-wellfounded calculi \(\mathsf{nICK}\), \(\mathsf{nICK_T}\) and \(\mathsf{nICK_{S4}}\). By following the construction given in Lemma 3.32 we obtain completeness for the cyclic calculi.

4.5.2 Completeness for S5 Models↩︎

This section shows that \(\mathrm{cICK}_\mathsf{S5}\) is complete with respect to the class of S5 epistemic models. Due to the presence of \(\mathsf{cut}\) we can prove completeness directly via a canonical model construction, which arguably simplifies the completeness proof. To obtain analytic completeness, applications of \(\mathsf{cut}\) will be restricted to a finite set of formulas relevant to the root sequent. So far we counted as relevant the formulas in the closure of the root sequent. However, as we have seen, the logic \(\mathbf{ICK_{S5}}\) satisfies many classical principles, implying that we need a stronger notion of closure to obtain completeness, namely the negation closure. In the following we provide the basic definitions and lemmas to obtain the canonical model for \(\mathrm{cICK}_\mathsf{S5}\).

\(\Sigma\)-saturated sequents will be the worlds of the canonical model. Let us first prove an analogue of the Lindenbaum Lemma for saturated sequents.

Next, we will establish some important properties of saturated sequents, that will become useful in the proof of the Truth Lemma (c.f. Lemma 4.11).

Given a set of formulas \(\Gamma\), let \(\mathsf{K}_i^{-1} \Gamma \mathrel{\vcenter{:}}= \{\varphi \mid \mathsf{K}_i \varphi \in \Gamma\}\). The canonical model relative to \(\Sigma\) is defined as follows.

4.6 A Modal Variant of Kuroda’s Translation↩︎

Glivenko’s Theorem [78] shows that classical propositional logic (\(\mathsf{CPC}\)) can be embedded into \(\mathsf{IPC}\) via a double-negation translation, which maps every propositional formula \(\varphi\) onto \(\neg \neg \varphi\). The formula \(\neg \neg \varphi\) is classically equivalent to \(\varphi\) (but not intuitionistically) and furthermore satisfies the property that \(\varphi\) is classically valid if and only if \(\neg \neg \varphi\) is intuitionistically valid. A similar translation embedding classical first-order predicate logic into intuitionistic first-order predicate logic is Kuroda’s translation [79], which prefixes every formula with \(\neg \neg\) and additional adds \(\neg \neg\) after every universal quantifier.

This section shows that classical common knowledge logic (\(\mathsf{CK}\)) over S5 models can be embedded into \(\mathsf{ICK}\) over S5. This will be achieved by constructing a modal variant of Kuroda’s translation, which assigns to each formula \(\varphi\) of \(\mathcal{L}_\mathsf{ICK}\) a formula \(tr(\varphi)\) by adding \(\neg \neg\) in front of \(\varphi\) and after every knowledge and common knowledge operator. We will then show that for any formula \(\varphi\),

1. \(\varphi\) is classically equivalent to its translation \(tr(\varphi)\) and

2. \(\varphi\) is classically valid if and only \(tr(\varphi)\) is intuitionistically valid,

which entails that \(\mathsf{CK}\) can be regarded as a fragment of \(\mathsf{ICK}\). First, let us briefly recall some basic definitions for \(\mathsf{CK}\).

The language of classical common knowledge logic is \(\mathcal{L}_{\mathsf{ICK}}\). Formulas are evaluated on classical S5 epistemic models. In order to distinguish these models from the S5 epistemic models for \(\mathsf{ICK}\), we will refer to the former as classical and to the latter as intuitionistic S5 epistemic models.

In difference to intuitionistic epistemic models, classical epistemic models do not feature the intuitionistic order \(\leq\). Formulas are evaluated on classical S5 epistemic models as follows. Let \(\mathcal{M}= (W, \{R_i\}_{i \in \mathsf{A}}, V)\) be a classical S5 epistemic model and \(w \in W\) a world.

The notions of satisfiability and validity are defined as usual. Let \(\mathbf{CK_{S5}}\) denote the set of valid \(\mathcal{L}_{\mathsf{ICK}}\)-formulas over the class of classical S5 models. It is easily checked that \(\mathcal{M}, w \models \neg \varphi\) where \(\neg \varphi = \varphi \rightarrow \bot\) if and only if \(\mathcal{M}, w \not \models \varphi\) and therefore that \(\mathcal{M}, w \models \varphi\) if and only if \(\mathcal{M}, w \models \neg \neg \varphi\).

The following definition introduces a function \(tr: \mathcal{L}_{\mathsf{ICK}} \longrightarrow \mathcal{L}_{\mathsf{ICK}}\) which serves as our modal variant of Kuroda’s translation.

In the following we show that \(tr\) satisfies Properties 1. and 2. stated above.

Recall that \(\mathbf{ICK_{S5}}\) has the finite model property. Therefore to check whether a formula is valid it suffices to consider the class of finite intuitionistic S5 epistemic models. Let \({\mathcal{M}=(W, \leq, \{R_i\}_{i \in \mathsf{A}}, V)}\) be a finite intuitionistic S5 epistemic model. Then \(w \in W\) is called a maximal world if for all \(v \in W\), if \(w \leq v\), then \(w=v\).

Note that every classical S5 epistemic model \(\mathcal{M}=(W, \{R_i\}_{i \in \mathsf{A}}, V)\) induces an intuitionistic S5 epistemic model \(\mathcal{M}^i = (W, \leq, \{R_i\}_{i \in \mathsf{A}}, V)\) by setting \(w \leq v\) if and only if \(w = v\). Observe that \(R_i\) is triangle confluent for each \(i \in \mathsf{A}\).

4.7 Complexity↩︎

The last section of this chapter investigates the computational properties of the cyclic calculus \(\mathrm{cICK}_{\mathsf{S5}}\). First, we show that proof search in \(\mathrm{cICK}_{\mathsf{S5}}\) can be automated by reducing the problem of finding a \(\mathrm{cICK}_\mathsf{S5}\)-proof for a sequent to the problem of solving a certain parity game (for which computationally well-behaved algorithms exist, see e.g. [80]). From this we obtain an exponential upper bound for solving the proof search problem for \(\mathrm{cICK}_\mathsf{S5}\) (see Table 7). By using the results from the previous section about the modal variant of Kuroda’s translation as well as soundness and completeness, we then provide a polynomial reduction of the proof search problem for \(\mathrm{cICK}_\mathsf{S5}\) to the validity problem for \(\mathbf{CK}\) (see Table 8), which is known to be ExpTime-complete [81], thus establishing that the proof-search problem is ExpTime-complete as well. We assume familiarity with parity games; for an introduction the reader is referred to [32].

4.7.1 Proof Search Games↩︎

Each sequent \(\sigma\) is associated with a parity game \(\mathcal{G}_\sigma\) called the proof search game associated to \(\sigma\). This game is played two players, one called Prover and the other called Refuter. Intuitively, like before, Prover is trying to show that a given sequent is provable, while Refuter tries to show the opposite. In difference to the proof search games employed in Chapter 3, the games here are parity games and not Gale–Steward games. The proof search games employed here are not used to prove completeness and hence we do not require to obtain a countermodel from a winning strategy for Refuter. Instead, it suffices to show that Prover has a winning strategy in \(\mathcal{G}_\sigma\) if and only if \(\sigma\) has a \(\mathrm{cICK}_{\mathrm{S5}}\)-proof. Crucially, parity games are memoryless determined, meaning that exactly one of the two players has a memoryless winning strategy (see e.g. [32]). From this we will be able to obtain that \(\mathrm{cICK}_{\mathrm{S5}}\) is uniformly complete, c.f. Theorem 4.8.

Recall that a rule instance in a sequent calculus is a tuple \(\langle \sigma, \langle \sigma_1, \ldots, \sigma_n \rangle \rangle\) and a rule is a set of rule instances (c.f. Definition 2.9).

We use \(\pi_n^k\) to denote the projection function which takes as input an \(n\)-tuple and outputs the \(k\)-th component. Thus for a rule position \(i =\langle \sigma, \mathsf{r}, \langle \sigma_1, \ldots, \sigma_n \rangle\rangle\), \(\pi_3^1(i) = \sigma\), \(\pi_3^2(i) = \mathsf{r}\) and \(\pi_3^3(i) = \langle \sigma_1, \ldots, \sigma_n \rangle\). Given a finite set of formulas \(\Sigma\), a \(\Sigma\)-rule position is a rule position involving only \(\Sigma\)-sequents. For the remainder of this section \(\Sigma\) always denotes a finite and negation closed set of formulas. We associate to each \(\Sigma\)-sequent \(\sigma\) a game as follows.

Observe that the only dead ends are rule instances of axioms. Therefore Prover wins every finite play. It is straightforward to check that for every \(\Sigma\)-sequent \(\sigma\) the game \(\mathcal{G}_\sigma\) is a parity game. Given a set \(X\), let \(X^{< \omega} \mathrel{\vcenter{:}}= \bigcup_{n < \omega} X^n\). Therefore the set of all initial segments of all possible plays in a game is a subset of \((S \cup I)^{< \omega}\). The following definitions apply to both Prover and Refuter. We write ‘Player’ instead.

A strategy \(\mathcal{S}\) for Player is winning if Player wins every play in which \(\mathcal{S}\) is used. The strategy tree of a memoryless strategy \(\mathcal{S}\) is the tree of all possible plays that can occur when Player uses \(\mathcal{S}\).

Note that due to \(\Sigma\) being finite and rules having finitely many premises, strategy trees are finite branching (and possibly non-wellfounded). The goal is to show that a sequent \(\sigma\) has a \(\mathrm{cICK}_\mathrm{S5}\)-proof if and only if Prover has a memoryless winning strategy in \(\mathcal{G}_\sigma\). To that end we require to do some preliminary work. Recall that in a cyclic proof \(\pi\) there exists for every non-axiomatic leaf \(l\) a node \(u\) such that \((u, l)\) is a successful repetition. As there might exist several candidates for the node \(u\), we fix for each non-axiomatic leaf \(l\) one candidate \(c(l)\) which we call the companion of \(l\).

Observe that cyclic proofs can be considered to be finite trees with back edges which satisfy the property that if \(u \in dom(f)\), then \(u\) is a non-axiomatic leaf and \(f(u)\) is the companion of \(u\).

If condition 3. applies, then we say that \(\rho\) passes through the leaf \(l\). The following lemma states a first basic result about infinite looping paths through finite trees with back edges. The proof of the lemma follows immediately from the fact that such trees are finite.

Next, we define a partial order on the range of the back edge function \(f\).

Note that \(u \preceq v\) implies that \(v\) is the companion of some leaf \(v'\) and \(u\) lies on the path from \(v\) to \(v'\). It is routine to check that the dependency order \(\preceq\) is reflexive, transitive and antisymmetric, implying that \(\preceq\) is a partial order on \(ran(f)\). We will use the dependency order to show that for every infinite looping path there exists a lowermost companion through which the path passes infinitely often. Let \((\mathcal{T},f)\) be a finite tree with back edges and let \(\rho\) be an infinite looping path through \((\mathcal{T},f)\). Denote by \(Inf(\rho)\) the set of nodes of \(\mathcal{T}\) that occur infinitely often in \(\rho\).

A slightly different version of the following lemma is proven in [82].

Recall that a play \(m\) in a proof search game is a sequence \(m(0),m(1),m(2), \ldots\) of positions. Observe that all even positions \(m(2i)\) are owned by Prover and all odd positions \(m(2i+1)\) by Refuter. For an initial segment \(m(0), \ldots m(i)\) of \(m\) we say that its length is \(i\).

Let us now consider the converse direction of Proposition 4.6.

Let \(R_I\) be the set of all rule instances of \(\mathrm{cICK}_{\mathrm{S5}}\) involving only \(\Sigma\)-sequents. Observe that the above constructed proof is uniform in the following sense:

Note that in a uniform proof the first repetition in each branch is successful. We conclude:

It should be noted that the construction of the proof search games and the corresponding proofs are not depending on \(\mathrm{cICK}_\mathsf{S5}\). In fact, the same proof holds for all proof systems for intuitionistic common knowledge logic (and of intuitionistic master modality) considered in this thesis.

4.7.2 Exponential Completeness↩︎

This subsection shows that the proof search problem for \(\mathrm{cICK}_{\mathrm{S5}}\) is ExpTime-complete. Let us first establish an exponential upper bound. Recall the notion of complexity of a formula and of a set of formulas (c.f. Definition 4.3). Given a sequent \(\sigma\), define the complexity of \(\sigma\) to be \(c(\sigma) \mathrel{\vcenter{:}}= c(\Gamma_\sigma) + c(\Delta_\sigma)\). Note that if \(\Sigma\) is the negation closure of \(\Gamma^- \cup \Delta^-\), then \(\lvert \Sigma \rvert\) is linear in \(c(\Gamma \Rightarrow \Delta)\).

In order to get a polynomial bound for deciding the winner of a given proof search game we can now make use of one of the many existing algorithms for solving parity games. For instance the following result by Calude et al. [80].

Let \(\sigma\) be a sequent and let \(\Sigma\) be its negation closure. By Lemma 4.19 the number \(n\) of positions in \(\mathcal{G}_\sigma\) is polynomial in the size of \(\lvert \mathcal{P}(\Sigma) \lvert\). Since the number of different priorities in our games is constant, Theorem 4.9 implies that there is an algorithm deciding the winner of \(\mathcal{G}_\sigma\) in time polynomial in \(\lvert \mathcal{P}(\Sigma) \lvert\) and so exponential in \(c(\sigma)\). By the same argument the above mentioned algorithm also computes a memoryless winning strategy in exponential time.

4.8 Conclusion↩︎

This chapter studied sound and complete analytic cyclic sequent calculi for intuitionistic common knowledge logic over epistemic models satisfying additional frame conditions. The introduced calculi are extensions of \(\mathrm{cIM}\) with rules for multiple modalities and frame conditions. Our work extends the seminal studies by Jäger and Marti [25], [26] and uses techniques developed in [39], [41]. The following summarizes the main results.

1. We have presented the cyclic calculi \(\mathrm{cICK}\), \(\mathrm{cICK}_{\mathrm{T}}\), \(\mathrm{cICK}_{\mathrm{S4}}\) and \(\mathrm{cICK}_{\mathrm{S5}}\) and shown that \(\mathrm{cICK}_{\mathrm{S5}}\) is not cut-free complete.

2. We have proven soundness and completeness of all four calculi with respect to the classes of epistemic models, reflexive epistemic models, S4 epistemic models and S5 epistemic models, respectively. The completeness proof for the first three calculi was an adaptation of the proof search method for \(\mathrm{cIM}\), thereby demonstrating the robustness of the method once more, while completeness for \(\mathrm{cICK}_{\mathrm{S5}}\) was proven by employing the technique of analytic cuts and a canonical model construction.

3. We have embedded classical common knowledge over S5 into intuitionistic common knowledge logic over S5 by adapting Kuroda’s translation to the modal case.

4. We have shown that proof search in \(\mathrm{cICK}_\mathsf{S5}\) can be automated by translating the calculus into a parity game and we have established a precise complexity bound for the proof search problem of \(\mathrm{cICK}_\mathsf{S5}\).

The calculus \(\mathrm{cICK}_{\mathrm{S5}}\) requires analytic cuts for completeness. An alternative solution would be to pass to calculi that manipulate sequents which have more structure, such as labelled or nested sequents. Labelling or nesting is a successful tool to handle frame conditions, thus the cut rule can be dropped. However, the combination of labelled/nested sequents with non-wellfounded proofs leads to the problem of how to detect successful repetitions in non-wellfounded branches of a proof and thus of how to obtain cyclic proof systems. The notion of repetition employed for \(\mathrm{cIM}\) and \(\mathrm{cICK}\) is too strong here, as in general it can not be expected to find a precise repetition in the presence of labels or nesting. Instead, a more likely solution is to weaken the notion of repetition. For example, since nested sequents are essentially finite trees of normal sequents, which might grow indefinitely along a non-wellfounded branch, a more promising notion of repetition would be a pair of sequents \((\sigma, \sigma')\) such that \(\sigma\) can be embedded into \(\sigma'\), implying that every rule applied between \(\sigma\) and \(\sigma'\) can be repeated at \(\sigma'\). We have been unable to solve this problem so far, and to the best of my knowledge there is no satisfying solution proposed in the literature. We thus leave it as an open question for future research.

Another open question regards the S5 epistemic models studied in this chapter. As demonstrated, the interaction of S5 frame conditions with triangle confluence leads to models where the modalities behave essentially ‘classical’. While this is an interesting mathematical observation, it is unclear whether such a logic is interesting from an application driven point of view. A possible next step is to replace triangle confluence with forth-down confluence. It is not hard to see that forth-down confluent and triangle confluent models result in the same logic when the modal accessibility relation satisfies no frame conditions. However, for S5 frame conditions, when using forth-down confluent models, the observation that the entire intuitionistic tree of a world \(w\) belongs to the same equivalence class no longer holds, implying that in such a setting triangle confluence is stronger than forth-down confluence. The following questions are thus left open by our work.

5 Intuitionistic Linear Temporal Logic↩︎

5.1 Introduction↩︎

The intuitionistic dynamic logics studied so far are evaluated over dynamic models which satisfy weak confluence conditions. As seen in Theorem 3.1 the language of \(\mathsf{IM}\) (and thus also the language of \(\mathsf{ICK}\)) cannot distinguish between dynamic models, triangle models and in particular functional models. This observation discouraged an interpration of \(\mathcal{L}_\mathrm{IM}\) as an intuitionistic linear temporal logic. In this chapter we will turn our attention to more expressive logics which are evaluated over classes of dynamic models satisfying stronger confluence properties. Specifically, we will study a version of intuitionistic linear temporal logic called \(\mathsf{iLTL}\), whose formulas are evaluated over two classes of total functional models: those satisfying forward confluence, and those satisfying both forward and back-up confluence (c.f. Definition 2.19). We follow [83] and call such models expanding and persistent, respectively. The language of \(\mathsf{iLTL}\) is capable of distinguishing between arbitrary (serial) dynamic models and expanding models, and also between expanding models and persistent models.

The origin of \(\mathsf{iLTL}\) goes back to the dynamic topological logic project. This project aims to develop computationally well-behaved logics to reason about topological dynamics: topological spaces equipped with a continuous function. Such dynamic systems are applied in diverse fields ranging from biology to physics and theoretical computer science. The dynamic topological logic project originated in the work of Artemov, Davoren and Nerode [17] who used modal logic - where \(\larger[-1.5]\square\) is evaluated as the ‘interior’ operator in the sense of Tarski [18] - extended with a temporal ‘next’ operator to reason about the action of the continuous function. Their logic was extended by Kremer and Mints [19] who introduced the logic \(\mathsf{DTL}\), which additionally features a fixed point operator from temporal logic to reason about the asymptotic behaviour of the continuous function. After \(\mathsf{DTL}\) was proven undecidable [20], the focus of the project shifted to intuitionistic versions of \(\mathsf{DTL}\) and thus to intuitionistic dynamic logics.

The logic \(\mathsf{iLTL}\) was studied in this context by Fernández-Duque [21]. For the following, familiarity with basic topology is assumed. A topological dynamic system is a tuple \(\mathcal{X}=(X, \tau, f)\) where \((X, \tau)\) is a topological space (e.g. the real line with the Euclidean topology) and \(f: X \longrightarrow X\) is a continuous function acting on \(X\). The function \(f\) is thought of as a temporal function, which maps each point of \(X\) onto its temporal successor. A topological model then consists of a topological dynamic system \((X, \tau, f)\) equipped with a valuation function \(V: \mathsf{Prop}\longrightarrow \tau\) which assigns to each proposition an open set, intuitively the set of points where the proposition holds. The language of \(\mathsf{iLTL}\) extends \(\mathcal{L}_\mathsf{IPL}\) by the temporal operators \(\mathbin{{\bigcirc}}\), \(\Diamond\) and \(\mathbin{\Box}\), where \(\mathbin{{\bigcirc}}\varphi\) is read as ‘in the next time step \(\varphi\) holds’, \(\Diamond\varphi\) is read as ‘eventually in the future \(\varphi\) holds’ and \(\mathbin{\Box}\varphi\) is read as ‘henceforth in the future \(\varphi\) holds’. Temporal formulas of \(\mathcal{L}_\mathsf{iLTL}\) are evaluated using the temporal function \(f\). More formally, we assign a truth set to formulas, which is the set of points at which the formula is true, as follows, where \(\circ\) denotes the interior operator.

Note that the truth set of each formula is open. In particular for the temporal cases, this follows from \(f\) being continuous, \(\tau\) being closed under arbitrary unions and in the case for \(\mathbin{\Box}\) from taking the interior of the infinite intersection. Write \(\mathcal{X} \models \varphi\) if \(\llbracket \varphi \rrbracket = X\) for any valuation \(V\). The resulting logic (without \(\mathbin{\Box}\)) was shown to be decidable and capable of expressing interesting properties about the underlying topological dynamic system by Fernández-Duque [21]. For example, call a topological dynamic system \((X, \tau, f)\) Poincaré-recurrent if any open set \(U \subseteq X\) contains a recurrent point, i.e. there exists \(x \in U\) and a natural number \(n > 0\) such that \(f^n(x) \in U\).

Furthermore, Boudou, Diéguez and Fernández-Duque provided a sound and complete axiomatization \(\mathrm{iLTL_H}\) for the \(\mathbin{\Box}\)-free fragment of \(\mathsf{iLTL}\) over the class of topological dynamic models [22], which is presented in Table ¿tbl:tab:32axiomatization32iltl?.¹⁷

When identifying the modal box operator \(\larger[-1.5]\square\) of \(\mathsf{IM}\) with \(\mathbin{{\bigcirc}}\), the difference between the modal axioms of \(\mathrm{IM_H}\) and \(\mathrm{iLTL_H}\) is the presence of two additional axioms, namely \(\mathsf{D}\) which expresses the seriality of the temporal function and \(\mathsf{Dist_\vee}\) which expresses that \(\mathbin{{\bigcirc}}\) distributes over disjunctions, which is not the case for \(\mathsf{IM}\). The axiom \(\mathsf{Dist_\wedge}\) is also not present in \(\mathrm{IM_H}\), but, as shown in Lemma 3.11, is derivable in \(\mathrm{IM_H}\) and thus also in \(\mathrm{iLTL_H}\). Apart from completeness with respect to the class of topological dynamic models, it was also shown in [22] that \(\mathrm{iLTL_H}\) is sound and complete with respect to the class of expanding models. Furthermore, Balbiani, Boudou, Diéguez and Fernández-Duque established that the language of \(\mathsf{iLTL}\) including \(\mathbin{\Box}\) is decidable over the class of expanding models [23], [83].

Several problems about \(\mathsf{iLTL}\) remain open. The first is about finding a sound and complete axiomatization for the language of \(\mathsf{iLTL}\) including \(\mathbin{\Box}\) (only an infinitary axiomatization has been found in [84]). This problem will be addressed in Chapter 6, where we present a finitary axiomatization for the language which is additionally extended by the co-implication connective of bi-intuitionistic logic. Second, it is unknown whether \(\mathsf{iLTL}\) over persistent models is decidable or even recursively enumerable and third, the proof theory of \(\mathsf{iLTL}\) remains largely unexplored. This chapter addresses the third problem. We will study non-wellfounded proof systems for \(\mathsf{iLTL}\) without \(\mathbin{\Box}\). Instead of using \(\Diamond\) in the language, we consider a slightly stronger temporal operator \(\mathbin{\mathsf{U}}\) (‘until’) with the intended semantics that a formula \(\varphi \mathbin{\mathsf{U}}\psi\) holds at a world \(w\) if \(\psi\) holds eventually in the future and until then \(\varphi\) holds. Thus \(\Diamond\) is definable in terms of \(\mathbin{\mathsf{U}}\). We present well-behaved non-wellfounded proof systems for \(\mathsf{iLTL}\) over the classes of expanding and persistent models, by adapting the techniques used for \(\mathsf{IM}\) and \(\mathsf{ICK}\). In order to capture the stronger confluence conditions of expanding and persistent models, our calculi employ a simple form of nested sequents, such that formulas can be operated on at different time steps. Such nesting is inspired from the work of Kojima and Igarashi [85] on sequent calculi for intuitionistic linear temporal logics featuring \(\mathbin{{\bigcirc}}\) as the only temporal operator. The resulting non-wellfounded calculi are analytic and sound and complete. However, it turns out that both calculi are not complete when restricted to regular proofs, implying that we won’t be able to prove completeness for a cyclic version of the calculus. In his recent PhD thesis, Menéndez Turata [24] improved upon our work and showed how to obtain complete cyclic proof systems for \(\mathsf{iLTL}\) over expanding models for the full language, but did not address persistent models.

We begin by introducing syntax and semantics of \(\mathsf{iLTL}\). Then we introduce two non-wellfounded sequent calculi \(\mathrm{niLTL_e}\) and \(\mathrm{niLTL_p}\) which are shown to be sound and complete for the classes of expanding and persistent models, respectively. Soundness is shown by a proof by infinite descent, which nicely illustrates the connection between such proofs and non-wellfounded proofs. Completeness is shown by proof search. In difference to \(\mathsf{IM}\), the proof search argument is significantly more complicated due to the confluence conditions of the models. Finally, we show that both calculi are not regularly complete by providing counterexamples.

5.2 Syntax and Semantics↩︎

The language \(\mathcal{L}_\mathsf{iLTL}\) of intuitionistic linear-time temporal logic \(\mathsf{iLTL}\) extends \(\mathcal{L}_\mathsf{IPL}\) by the temporal operators \(\mathbin{{\bigcirc}}\) and \(\mathbin{\mathsf{U}}\). Formulas are given by the following grammar in Backus–Naur form: \[\varphi \Coloneqq \bot \mid p \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid \varphi \rightarrow \varphi \mid \mathbin{{\bigcirc}}\varphi \mid \varphi \mathbin{\mathsf{U}}\varphi\] where \(p \in \mathsf{Prop}\). The operator \(\mathbin{{\bigcirc}}\) is the ‘next’-operator: read \(\mathbin{{\bigcirc}}\varphi\) as ‘in the next time step, \(\varphi\) holds’ and \(\mathbin{\mathsf{U}}\) is the ‘until’-operator: read \(\varphi \mathbin{\mathsf{U}}\psi\) as ‘\(\varphi\) holds until \(\psi\) holds (and \(\psi\) eventually holds)’. \(\mathbin{\mathsf{U}}\) is a least fixed point operator: \(\varphi \mathbin{\mathsf{U}}\psi\) is characterized as the least fixed point of the propositional function \(x \mapsto \psi \vee (\varphi \wedge \mathbin{{\bigcirc}}x)\). The aforementioned temporal modality \(\Diamond\) (‘eventually’) can be defined in terms of \(\mathbin{\mathsf{U}}\) by \[\Diamond\varphi \mathrel{\vcenter{:}}= \top \mathbin{\mathsf{U}}\varphi.\] The temporal modality \(\mathbin{\Box}\) (‘henceforth’) is however not definable in this language [83].

Formulas of \(\mathsf{iLTL}\) are evaluated on two classes of dynamic models where the modal accessibility relation is a function which in one case is forward confluent and in the other case both forward and back-up confluent (c.f. Definition 2.19). Recall that given a dynamic model \(\mathcal{M}=(W, \leq, f, V)\) where \(f\) is a function, \(f\) is forward-confluent if and only if \(f\) is monotone in \(\leq\), i.e. if \(w \leq v\), then \(f(w) \leq f(v)\) (c.f. Lemma 2.7).

The confluence conditions guarantee that classical truth conditions for the temporal modalities can be used without losing the monotonicity property.

As usual, a formula \(\varphi\) is satisfiable over the class of expanding (persistent) models if there exists an expanding (persistent) model \(\mathcal{M}=(W, \leq, f, V)\) and a world \(w \in W\) with \(\mathcal{M}, w \models \varphi\) and unsatisfiable otherwise. A formula \(\varphi\) is valid over the class of expanding (persistent) models if for all expanding (persistent) models \(\mathcal{M}=(W, \leq, f, V)\) and all worlds \(w \in W\) holds that \(\mathcal{M}, w \models \varphi\) and invalid otherwise.

Since every persistent model is an expanding model, clearly \(\mathbf{iLTL_e} \subseteq \mathbf{iLTL_p}\) holds. The following lemma shows that the inclusion is strict.

5.3 Nested Non-Wellfounded Proofs↩︎

This section presents non-wellfounded sequent calculi for \(\mathsf{iLTL}\) over expanding models and over persistent models, respectively. In difference to the non-wellfounded calculus \(\mathrm{nIM}\) for \(\mathsf{IM}\), the systems do not feature a focus annotation. Recall that the focus annotation in \(\mathrm{nIM}\) was used to prove soundness of the cyclic system. Since we only study non-wellfounded systems here, the focus annotation is no longer needed. However, due to the lack of a focus annotation, the global correctness criterion imposed on infinite branches is formulated differently using formula traces. To ensure completeness, the calculi incorporate a simple form of nesting, which is inspired by the work of Kojima and Igarashi [85] who developed a nested sequent calculus for a version of \(\mathsf{iLTL}\) where the only temporal modality is \(\mathbin{{\bigcirc}}\).

Note that in difference to the definition of sequents for \(\mathrm{nIM}\), every tuple \(\Gamma \Rightarrow \Delta\) with \(\Gamma, \Delta\) being finite sets of nested formulas is a sequent. As before, we denote sequents by \(\sigma\) and \(\Gamma_\sigma\), \(\Delta_\sigma\) denote the left side and right side of \(\sigma\), respectively. For the remainder of this chapter nested formulas are simply called formulas. Formulas that are not nested are called plain. As for \(\mathrm{nIM}\) we consider multi-conclusion sequents. Once again, this is to simplify the proof search argument in the completeness proof. At first glance, nested formulas might look little different to annotated formulas, but this is misleading. The difference becomes clear in the interpretation of a sequent.

To simplify notation, we write \(\mathcal{M},w \models \varphi^n\) if \(M,w \models \mathbin{{\bigcirc}}^n \varphi\) and \(\mathcal{M},w\models \sigma\) if \(M,w \models \sigma^I\). For any set \(\Gamma\) of nested formulas, define \[\Gamma^{+1} \mathrel{\vcenter{:}}= \{\varphi^{n+1}: \varphi^n\in \Gamma\}.\]

We will now introduce the sequent calculi \(\mathrm{niLTL_e}\) and \(\mathrm{niLTL_p}\), which will be proven to be sound and complete with respect to the classes of expanding models and of persistent models, respectively. Both calculi are based on the basic rules depicted in Table 9 as well as some of the additional rules in Table 10.

The rules \(\mathsf{id}\) and \(\bot\) are called axioms. The basic rules for \(\wedge, \vee, \rightarrow\) are nested versions of the corresponding rules in the sequent calculus for intuitionistic logic \(\mathrm{IPL_s}\) (see Definition 2.15). The \(\mathbin{\mathsf{U}}\)-rules capture the equivalence \[\varphi\mathbin{\mathsf{U}}\psi\equiv \psi\lor (\varphi\land \mathbin{{\bigcirc}}(\varphi\mathbin{\mathsf{U}}\psi)).\] Note that the rules \(\mathbin{{\bigcirc}}\mathsf{L}\) and \(\mathbin{{\bigcirc}}\mathsf{R}\) are purely structural as \(\mathbin{{\bigcirc}}\varphi^n\) has the same interpretation as \(\varphi^{n+1}\). Regarding the additional rules observe that the rule \({\rightarrow} \mathsf{R}\) can only be applied to implications with nesting level \(0\) while the rule \({\rightarrow} \mathsf{R_p}\) can be applied to implications of arbitrary nesting level. Interestingly, this is the crucial difference between the calculi \(\mathrm{niLTL_e}\) and \(\mathrm{niLTL_p}\). To understand why, it is instructive to think semantically about what these rules express. Naturally, both rules should preserve validity when read top-down. The rule \({\rightarrow} \mathsf{R_p}\) then expresses that if \(\mathbin{{\bigcirc}}^n \varphi \rightarrow \mathbin{{\bigcirc}}^n \psi\) is valid, so is \(\mathbin{{\bigcirc}}^n (\varphi \rightarrow \psi)\). By Lemma 5.1 this rule preserves validity over persistent models, but not over expanding models. Thus, for \(\mathrm{niLTL_e}\), we must use the standard implication rule, where the nesting level is \(0\). This restriction forces us to include an additional rule for \(\mathrm{niLTL_e}\), namely the ‘shift’-rule \(\mathsf{S}\), that allows us to reduce the nesting level of formulas and captures necessitation. For \(\mathrm{niLTL_p}\), the shift-rule is not required.

Recall the (semantic) definition of an invertible rule (c.f. Definition 3.17). The following lemma is routine.

We will therefore refer to the additional rules as the non-invertible rules and to all other rules as the invertible rules.

For each rule, the distinguished formula in the conclusion is called principal and the distinguished formulas in the premises are called its residuals. For \(\mathrm{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 \(\Sigma\) and \(\Pi\) have no residual. In every rule application, any formula that is neither principal nor residual is called a side formula. For the remainder of this section, let \(\mathsf{P} \in \{\mathrm{niLTL_e}, \mathrm{niLTL_p}\}\).

Recall the definition of a path through a tree (c.f. Section 2.1). If there is no danger of confusion, paths will be identified with the sequence of sequents that label the nodes of the path.

For any rule \(\mathsf{r}\), a trace \((\varphi_i^{n_i})_{i}\) passes actively through \(\mathsf{r}\) if there is an index \(j\) such that \(\varphi_j^{n_j}\) is a principal formula in an instance of \(\mathsf{r}\). To keep the notation simple, when reasoning about traces \((\varphi_i^{n_i})_i\), we will usually omit the index for the nesting and simply write \((\varphi_i)_i\). It will always be clear from context that we refer to nested formulas and not to plain formulas.

Note that the focus annotation employed in the non-wellfounded system \(\mathrm{nIM}\) in Chapter 3 captures specific formulas traces. Namely a good suffix in a branch of an \(\mathrm{nIM}\)-pre-proof always has a formula in focus which is of the form \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\psi^f\) or \(\larger[-1.5]\square\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\psi^f\) for some formula \(\psi\). Therefore we obtain a trace through a good suffix by considering the infinite sequence of focused formulas \((\varphi_i)_i\) occurring in the suffix. Note that this sequence satisfies the definition of a formula trace above (minus the first condition, which has to be replaced by the condition that the trace formula (i.e. the formula in focus) occurs on the right side of the sequent). The focus annotation thus keeps track of one trace through a suffix of an infinite branch, and in order for the suffix to be good, it is required that the trace passes infinitely often through an instance of \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\mathsf{R}\). Here, we define similarly the notion of a good trace.

The following lemma describes a straightforward yet key property of good formula traces, where the complexity of a nested formula is simply the complexity of the underlying plain formula. We provide a proof sketch.

5.4 Soundness↩︎

This section establishes soundness of \(\mathrm{niLTL_e}\) with respect to the class of expanding models and of \(\mathrm{niLTL_p}\) with respect to the class of persistent models. The proof is essentially an infinitary version of the soundness proof for \(\mathrm{cIM}\). The measure \(\mu(\sigma)\) assigned to sequents is generalised to signatures: maps that associate a natural number to each ‘relevant’ formula in a sequent \(\sigma\). We then assume towards a contradiction that there is a proof \(\pi\) of an invalid sequent \(\sigma\) and show, using a countermodel of \(\sigma\), how to find an infinite path \(\rho\) of invalid sequents in \(\pi\) such that their signatures never increase but strictly decrease infinitely often, thus obtaining a contradiction to the well-foundedness of the natural numbers. The aforementioned ‘relevant’ formulas are called eventualities.

Let \(\mathbin{\mathsf{U}}^k\) be the operator defined inductively by \(\varphi\mathbin{\mathsf{U}}^0 \psi=\psi\) and \(\varphi\mathbin{\mathsf{U}}^{k+1}\! \psi=\varphi\land \mathbin{{\bigcirc}}(\varphi\mathbin{\mathsf{U}}^{k}\! \psi)\). For an eventuality \(E=\mathbin{{\bigcirc}}^j (\varphi\mathbin{\mathsf{U}}\psi)^n\) and \(k < \omega\) define \[\begin{align} E[k]:=\mathbin{{\bigcirc}}^j (\varphi\mathbin{\mathsf{U}}^{k}\! \psi)^n. \end{align}\] Given a sequent \(\sigma\), a signature for \(\sigma\) is a map \(\tau\) which assigns a natural number to each eventuality of \(\sigma\). Let \(\Gamma_\sigma[\tau]\) be the set obtained from \(\Gamma_\sigma\) by replacing each eventuality \(E\) with \(E[\tau(E)]\). Furthermore, let \(\sigma[\tau]\) denote the sequent \(\Gamma_\sigma[\tau]\Rightarrow \Delta_\sigma\).

Note that Lemma 5.7 implies that given \(\mathcal{M}, w\) and \(E\) with \(\mathcal{M}, w \models E\), there exists a least natural number \(k\) with \(\mathcal{M}, w \models E[k]\).

We finish the section by proving that \(\mathrm{niLTL_p}\) is sound with respect to the class of persistent models. The proof follows the same argument as for \(\mathrm{niLTL_e}\), with the only differences that the case for \(\mathsf{S}\) can be skipped and the case for \({\rightarrow}\mathsf{R}\) must be replaced by the case for \({\rightarrow}\mathsf{R_p}\).

5.5 Completeness↩︎

This section establishes completeness of \(\mathrm{niLTL_e}\) with respect to the class of expanding models and of \(\mathrm{niLTL_p}\) with respect to the class of persistent models. As for \(\mathrm{nIM}\) the proof proceeds via a proof search argument. For each sequent \(\sigma\) we construct an infinite two-player game between Prover and Refuter such that a winning strategy for Prover corresponds to a proof of \(\sigma\) and a winning strategy for Refuter to the existence of a countermodel for \(\sigma\). The game will be played on a proof search tree, which is a finitely branching, non-wellfounded tree that presents a systematic search for a proof of \(\sigma\). The presented completeness proofs share many similarities with the completeness proof for \(\mathrm{nIM}\). However, there are some crucial differences, due to the presence of forward and back-up confluence, that the countermodels induced by a refutation must satisfy.²⁰ For \(\mathrm{nIM}\), when a formula \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) was present on the right side of a sequent, it sufficed to unfold it once to saturate the formula, i.e. it was enough to guarantee that \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) was locally correct in the world corresponding to the saturated sequent. In the presence of forward confluence, this does not suffice. Suppose for example that a formula of the form \(\Diamond(\varphi \vee \psi)^0\) (i.e. \(\top \mathbin{\mathsf{U}}(\varphi \vee \psi)^0\)) occurs on the left side of a sequent \(\sigma\) corresponding to the world \(w\). The countermodel then must contain a temporal successor \(f^n(w)\) which satisfies \(\varphi \vee \psi\), which will be guaranteed by the fact that no infinite branch in a refutation can contain a good trace, i.e. after finitely many times unfolding \(\Diamond(\varphi \vee \psi)\) the Refuter must chose the left premise of \(\mathbin{\mathsf{U}}\mathsf{L}\), which will result in the corresponding world satisfying \(\varphi \vee \psi^0\). Saturation then guarantees that \(\varphi^0\) or \(\psi^0\) is contained on the left side of the saturated sequent, implying that the corresonding world \(f^n(w)\) satisfies \(\varphi\) or \(\psi\). However if there exists a world \(v \geq w\), then by forward confluence \(f^n(v) \geq f^n(w)\), so by monotonicity \(f^n(v)\) must satisfy the same disjunct as \(f^w(v)\). In the way proof search trees are defined, the finite segment in a branch corresponding to \(f^n(v)\) is unrelated to the finite segment corresponding to \(f^n(w)\) in the proof search tree. Thus it could happen that at the segment corresponding to \(f^n(w)\), when we apply \(\vee \mathsf{L}\) to \(\varphi \vee \psi^0\), Refuter chooses \(\varphi\), while at the segment corresponding \(f^n(v)\), Refuter chooses \(\psi\), implying that the resulting model is not monotone. To circumvent this problem, we will make use of the nesting and impose that in order to saturate a sequent, we must apply \(\mathbin{\mathsf{U}}\mathsf{L}\) finitely many times until the left premise is chosen, implying that some branches (namely those containing a good trace) will never encounter a saturated sequent. The nesting is crucial for this, as we are able to continue unfolding by eliminating \(\mathbin{{\bigcirc}}\)-operators and instead increase the nesting level.

5.5.1 Completeness for Expanding Models↩︎

We start by giving a suitable notion of saturated sequent.

Note that the saturation clause for right \(\mathbin{\mathsf{U}}\)-formulas is restricted to the zeroth nesting level. As before, 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. Note that rule applications of \({\to} \mathrm{R}\) and \(\mathrm{S}\) are always succinct.

The choice rule \(\mathsf{C}\) represents a choice between non-invertible rules that Prover 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 \(\mathrm{C}\)-rule and has another empty sequent as its only direct successor. This is why, in difference to proof search trees for \(\mathrm{nIM}\), every leaf in a proof search tree is labeled by an axiom.

Intuitively, 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 \(\mathsf{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 proof is similar to the proof of Lemma 3.26 and omitted.

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

Next we define proof search games. As before, proof search games are played on proof search trees by two players called Prover and Refuter. Since only one frame condition is considered (and therefore only one choice rule is needed), the choice rule \(\mathsf{C}\) is not displayed in the name of the proof search game.

Observe that every play in \(\mathcal{G}(\mathcal{T}, \sigma)\) corresponds to a branch of \(\mathcal{T}\). As for \(\mathrm{nIM}\) a strategy for Player is a partial function \(f\) which maps any position \(t\) owned by Player onto a child node of \(t\). Player uses strategy \(f\) if whenever a play is in position \(t\) owned by Player, then Player chooses \(f(t)\). A strategy \(f\) is a winning strategy if Player wins every play in which \(f\) is used. The strategy tree of a strategy \(f\) is the subtree of \(\mathcal{T}\) consisting of all plays that can occur when Player uses \(f\). For detailed definitions, see Definition 3.29, Definition 3.30 and Definition 3.31. The following lemma then follows directly from the winning conditions of Prover.

Winning strategies for Prover therefore correspond to proofs. Similarly, winning strategies for Refuter correspond to refutations.

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

Fix a sequent \(\sigma\) and a refutation \(\mathcal{R}\) of \(\sigma\).

Similar to \(\Gamma_w\) we write \(\Delta_w\) for \(\bigcup_{s\in w} \Delta_{s}\). The following is straightforward to check.

As for \(\mathrm{nIM}\), the set of winning plays for each player is Borel and therefore, by Martin’s Determinacy Theorem [68], the game \(\mathcal{G}(\mathcal{T}, \sigma)\) is determined. Thus we obtain completeness.

5.5.2 Completeness for Persistent Models↩︎

Completeness for \(\mathrm{niLTL_p}\) is once again established using a proof search argument. Due to the more complex frame conditions on persistent models, an adaption of the argument given for \(\mathrm{niLTL_e}\) is needed. In particular, the canonical model relative to a refutation is defined differently. For \(\mathrm{niLTL_e}\), right premises of the \(\mathsf{C}\)-rule generated temporal successors of the current world. For \(\mathrm{niLTL_p}\), right premises of (the appropriate version of the) \(\mathsf{C}\)-rule will instead serve as a further description of the current world. To formalize this, an improved notion of saturation is required.

Note that a sequent is a pre-sequent where \(\Gamma, \Delta\) are finite.

Note that \(0\)-saturation is equivalent to the notion of saturation provided in Definition 5.13. Furthermore note that if a pre-sequent \(\sigma\) contains a formula \(\varphi \mathbin{\mathsf{U}}\psi^n\) on the right side, then if \(\sigma\) is strongly saturated, \(\Delta_\sigma\) must be infinite. The proof search tree defined below is labeled by indexed sequents \(\Gamma\Rightarrow_k \Delta\), that is, sequents decorated with a natural number \(k<\omega\), as were used for obtaining completeness of \(\mathrm{nIM}\) with respect to the class of functional models. Formally, there is no difference between indexed sequents here and the ones used for \(\mathrm{nIM}\): both are simply sequents decorated with a natural number. However, here the indexed sequents will play a different role in the argument, as they are used to keep track of the saturation level of the current sequent, and not to keep track which \(\larger[-1.5]\square\)-formula has to be falsified in the \(\mathsf{C}\)-instance.

Observe that the right premise of \(\mathsf{C_p}\) is an instance of a structural rule which does not change any formulas but instead increases the index by \(1\). Therefore, given that the conclusion is \(k\)-saturated, the right premise is still \(k\)-saturated, but not necessarily \((k+1)\)-saturated.

The following lemmas are proven as before; proofs are omitted.

The game \(\mathcal{G}(\mathcal{T}, \sigma)\) for \(\mathcal{T}\) a proof search tree for \(\sigma\) is defined as before (c.f. Definition 5.15) where \(\mathsf{C}\) is replaced by \(\mathsf{C_p}\).

Winning strategies for Refuter, on the other hand, correspond to refutations which are defined as in Definition 5.16, with \(\mathsf{C}\) replaced by \(\mathsf{C_p}\). Note that the fifth condition together with Lemma 5.20 imply that every branch in a refutation must contain infinitely many applications of the \(\mathsf{C_p}\)-rule. The proof of the following lemma is identical to the proof of Lemma 5.13.

It remains to show that the existence of a refutation for \(\sigma\) implies the existence of a countermodel. In the following let \(\sigma\) be a sequent and let \(\mathcal{R}\) be a refutation for \(\sigma\).

The construction of the canonical model formalizes the idea that the entire refutation corresponds to the intuitionistic tree rooted at time point \(0\), while every temporal successor is added in ‘manually’.

For any \(w^0 \in W\), denote by \(\Delta_{w^0}\) the set of formulas \[\Delta_{w^0} = \bigcup_{s \in w^0} \Delta_s.\]

As for \(\Gamma_{w^0}\), note that \(\Delta_{w^0}\) is in general infinite.

Finally, as before, completeness follows from determinacy of \(\mathcal{G}(\mathcal{T}, \sigma)\).

5.6 A Counterexample to Regular Completeness↩︎

The previous section showed that the calculus \(\mathrm{niLTL_e}\) is complete with respect to the class of expanding models and \(\mathrm{niLTL_p}\) is complete with respect to the class of persistent models. The proofs utilized a proof search argument. Unfortunately the presented proof does not yield regular completeness for either \(\mathrm{niLTL_e}\) or \(\mathrm{niLTL_p}\), due to the presence of the nesting. In particular, the constructed proof search trees do not establish a bound on the nesting level occurring in the sequents in a proof. For \(\mathrm{niLTL_e}\) the \(\mathsf{S}\)-rule is only applied to saturated sequents (as part of the \(\mathsf{C}\)-rule), however successful branches may only pass through finitely many instances of \(\mathsf{C}\), implying that the nesting level may grow indefinitely. The calculus \(\mathrm{niLTL_p}\) does not even feature a rule which reduces the nesting level. This phenomenon causes issues when it comes to establishing cyclic completeness. In order to obtain a cyclic calculus, we would require a bound on the nesting depth to find successful repetitions. In this section we show that this is not possible by providing an example of a valid sequent which is not provable in \(\mathrm{niLTL_e}\) with a bounded nesting level. Consider the following sequent: \[\Diamond (\varphi \vee \psi)^0 \Rightarrow \gamma \rightarrow \Diamond \varphi^0, \gamma \rightarrow \Diamond \psi^0.\] Recall that \(\Diamond \varphi = \top \mathbin{\mathsf{U}}\varphi\). First of all, let us show that \(\sigma\) is \(\mathrm{niLTL_e}\)-provable. In the proof depicted below, let \(\Delta = \{\gamma \rightarrow \Diamond\varphi^0, \gamma \rightarrow \Diamond\psi^0\}\)

The subproof \(\pi_0\) is given as follows.

The subproof \(\pi_1\) is similar, the only difference being that the formulas \(\Diamond \varphi^0\) and \(\Diamond \psi^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 level 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 \(\mathbin{\mathsf{U}}\mathsf{L}\) to the root sequent results in an unprovable sequent, and applying any rule other than \(\mathbin{{\bigcirc}}\mathsf{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\). Therefore \(\sigma\) cannot be proven with a bound on the nesting level, implying that \(\mathrm{niLTL_e}\) is not regularly complete.

5.7 Conclusion↩︎

This chapter studied non-wellfounded proof systems for intuitionistic linear temporal logic \(\mathsf{iLTL}\) featuring the temporal operators \(\mathbin{{\bigcirc}}\) and \(\mathbin{\mathsf{U}}\). The following summarizes the main contributions.

1. We have introduced the non-wellfounded nested calculus \(\mathrm{niLTL_e}\) and shown that it is sound and complete for the class of expanding models.

2. We have introduced the non-wellfounded nested calculus \(\mathrm{niLTL_p}\) and shown that it is sound and complete for the class of persistent models.

The nesting is used to manipulate formulas within the scope of \(\mathbin{{\bigcirc}}\)-operators, which is needed to deal with the confluence conditions imposed on expanding and persistent models. The main difference between the two calculi lies in the right implication rules: for \(\mathrm{niLTL_e}\), only implication formulas with nesting level \(0\) can function as principal formulas; for \(\mathrm{niLTL_p}\), any implication formula can be principal. The rule \({\rightarrow}\mathsf{R_p}\) directly corresponds to the dual \(\mathsf{K}\)-axiom \((\mathbin{{\bigcirc}}\varphi \rightarrow \mathbin{{\bigcirc}}\psi) \rightarrow \mathbin{{\bigcirc}}(\varphi \rightarrow \psi)\) which is valid over the class of persistent models but not over the class of expanding models. Both systems are arguably elegant and easy to work with. The main drawback of our work is that the presented systems are not regularly complete, as shown in Section 5.6. The presented example shows that the problem of obtaining regular completeness lies in the non-invertibility of the right implication rule. In order to prove the sequent \[\Diamond (\varphi \vee \psi)^0 \Rightarrow \gamma \rightarrow \Diamond \varphi^0, \gamma \rightarrow \Diamond \psi^0\] we cannot find a bound on the nesting level since whenever we apply \({\rightarrow}\mathsf{R}\) we lose one of the two formulas on the right side. Therefore, the only solution is to continue unfolding \(\Diamond(\varphi \vee \psi)\) on the left side, thereby increasing the nesting level indefinitely. Only once we follow a left branch after an instance of \(\mathsf{UL}\) we may decompose the formula \(\varphi \vee \psi^n\) and then in each branch chose the correct implication formula on the right side to obtain an axiom.

Our observations imply that the presented calculi need to be adapted to obtain regular completeness. One possibility is to extend the system with the cut rule and attempt to prove regular completeness for an extended system using analytic cuts. As for \(\mathsf{ICK}\), we would attempt to prove regular completeness by directly considering a cyclic version of \(\mathrm{niLTL_e}\) (or \(\mathrm{niLTL_p}\)). However, the situation is considerably harder than for \(\mathsf{ICK}\). When defining a finite canonical model for a fragment of the language, the resulting structure does not preserve forward confluence. A similar issue will be encountered in Chapter 6 where a bi-intuitionistic version of temporal logic is studied. We were not able to solve this problem. In fact, it seems unlikely that regular completeness may be obtained by using analytic cuts, due to computational reasons. The precise complexity bound for checking validity for \(\mathsf{iLTL}\) is unknown. The best known upper bound is non-elementary [23], meaning that the algorithm cannot be bounded by any tower of exponentials. If we would obtain completeness for a cyclic version of \(\mathrm{niLTL_e}\) with analytic cuts, we would obtain an exponential upper bound by the same argument as presented in Chapter 4 for \(\mathsf{ICK}\) over S5 models. It seems at least unlikely that such an improvement is possible; though certainty will only be obtained once a precise complexity bound for \(\mathsf{iLTL}\) is established, which we leave as an open question. For \(\mathsf{iLTL}\) over persistent models it is unknown whether the validity problem is even recursively enumerable. Once again, a cyclic version of \(\mathrm{niLTL_p}\) with analytic cuts would lead to a decidability result and an exponential upper bound, which again seems rather unlikely.

A better solution was proposed by Menéndez Turata in his recent PhD thesis [24], who considered labeled instead of nested sequents. This change allows to write the right implication rule in invertible form, while structural rules manipulating labels guarantee that the monotonicity of the valuation of an induced countermodel is obtained in future time steps (a task that in our case the nesting fulfils). This change makes it possible to regularize non-wellfounded proofs: Menéndez Turata presents a non-wellfounded and a cyclic proof system for the language of \(\mathsf{iLTL}\) with the temporal operators \(\mathbin{{\bigcirc}}\), \(\mathbin{\mathsf{U}}\) and ‘release’ \(\mathsf{R}\). As for the cyclic proofs for \(\mathsf{IM}\), a specific annotation of formulas is used to detect good cycles. For details, the reader is refered to [24]. The method used by Menéndez Turata is perhaps adapable to our framework of using nested sequents. To that end we would need to add additional structure to sequents, namely a second type of nesting that allows for operating on formulas within the scope of implications. In that way a proof search algorithm could explore both the ‘future regions’ and the ‘intuitionistic regions’ in a proof search tree without getting stuck due to non-invertible rules. The details of such an adaptation are unknown to us and left for future work.

6 Bi-Intuitionistic Linear Temporal Logic↩︎

6.1 Introduction↩︎

The final contribution of this thesis is to present a sound and complete axiomatization for the language of intuitionistic linear temporal logic with the temporal operators ‘next’, ‘eventually’ and ‘henceforth’ evaluated over (total functional) expanding models. Recall the axiomatization \(\mathrm{iLTL_H}\) for \(\mathsf{iLTL}\) without ‘henceforth’ depicted in the introduction of Chapter 5, which was originally presented and proven sound and complete in [22]. It was shown in [22] that \(\mathrm{iLTL_H}\) is sound and complete with respect to topological semantics and with respect to expanding models, showing that the language without ‘henceforth’ cannot distinguish between these two classes. The problem of axiomatizing the full language including ‘henceforth’ has remained open for several years. A natural guess for obtaining a sound and complete system for \(\mathsf{iLTL}\) with henceforth would be to extend \(\mathsf{iLTL}_\mathrm{H}\) with a standard fixed point axiom for henceforth as well as rules for monotonicity and induction, i.e. extend \(\mathsf{iLTL}_\mathrm{H}\) with the following axioms and rules.

However, it was shown in [86] that the axioms and rules above are valid and validity preserving both over topological dynamic and expanding models. In the presence of ‘henceforth’, the sets of validities over these classes of models are not identical, as opposed to the language without ‘henceforth’. This can be seen, for example, from the Rodríguez–Vidal formula \(\mathbf{RV} \mathrel{\vcenter{:}}= \mathbin{\Box}(p \vee q) \rightarrow (\mathbin{\Box}p \vee \Diamond q)\), expressing that if \(p \vee q\) is true henceforth, then \(q\) is true eventually or henceforth \(p\) is true. Clearly, this formula is valid over expanding models: if \(\mathcal{M}, f^n(w) \models p \vee q\) for all \(n < \omega\), then either there is \(n < \omega\) such that \(\mathcal{M}, f^n(w) \models q\) or otherwise \(\mathcal{M}, f^n(w) \models p\) for all \(n < \omega\). Over topological models, the formula \(\mathbf{RV}\) is not valid, as shown in the following example.

This implies that the proposed axiomatization above cannot be complete for expanding models, as otherwise there would exist a derivation of \(\mathbf{RV}\) and since the axiomatization is sound with respect to topological models, \(\mathbf{RV}\) would be valid over topological models. Instead of extending \(\mathrm{IM_H}\) with different axioms, we present an alternative and perhaps surprising solution. When extending the language of \(\mathsf{iLTL}\) with the co-implication connective \(\mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\), the natural axiomatization becomes ‘magically’ complete. This is because the presence of \(\mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\) and temporal modalities creates implicit interaction, which can be used to derive formulas such as \(\mathbf{RV}\). Thus the derivation of \(\mathbf{RV}\) (see Example 6.3) features formulas with co-implications, even though \(\mathbf{RV}\) itself belongs to the \(\mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\)-free fragment. Thus, our axiomatization is not conservative over the \(\mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\)-free fragment. The resulting logic is called bi-intuitionistic linear temporal logic \(\mathsf{biLTL}\), which contains \(\mathsf{iLTL}\) as a fragment.

The next two sections introduce the syntax and semantics of \(\mathsf{biLTL}\), as well as the axiomatization \(\mathrm{biLTL_H}\). We will then establish soundness as well as completeness for the axiomatization obtained from \(\mathrm{biLTL_H}\) restricted to the language without \(\mathbin{\Box}\) and \(\Diamond\). The final sections then establish completeness for \(\mathrm{biLTL_H}\).

6.2 Syntax and Semantics↩︎

The language of bi-intuitionistic temporal logic \(\mathcal{L}_\mathsf{biLTL}\) extends \(\mathcal{L}_\mathsf{IPL}\) by the temporal operators \(\mathbin{{\bigcirc}}\), \(\Diamond\) and \(\mathbin{\Box}\), as well as by the binary connective \(\mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\). The operators \(\Diamond\) and \(\mathbin{\Box}\) are fixed point operators. \(\Diamond\varphi\) is characterized as the least fixed point of the propositional function \(x \mapsto \varphi \vee \mathbin{{\bigcirc}}x\). \(\mathbin{\Box}\varphi\) is characterized as the greatest fixed point of the propositional function \(x \mapsto \varphi \wedge \mathbin{{\bigcirc}}x\). Formulas are given by the following grammar in Backus–Naur form (where \(p \in \mathsf{Prop}\)): \[\varphi \mathrel{\vcenter{:}}= \bot \mid p \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid \varphi \rightarrow \varphi \mid \varphi \mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\varphi \mid \mathbin{{\bigcirc}}\varphi \mid \Diamond\varphi \mid \mathbin{\Box}\varphi\] As before, the connective \(\mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\) is called co-implication and the temporal operators \(\mathbin{{\bigcirc}}\), \(\Diamond\) and \(\mathbin{\Box}\) are read as ‘next’, ‘eventually’ and ‘henceforth’, respectively. The \(\Diamond\)- and \(\mathbin{\Box}\)-free fragment of \(\mathcal{L}_\mathsf{biLTL}\) is denoted by \(\mathcal{L}_{\mathbin{{\bigcirc}}}\). As for bi-intuitionistic modal logic in the previous chapter, the constant \(\bot\) can be defined in terms of \(\mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\) by setting \(\bot \mathrel{\vcenter{:}}= p \mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}p\) for \(p \in \mathsf{Prop}\) and we will treat \(\bot\) as a defined constant henceforth. Moreover, we also once again define weak negation \(\sim\) by \({\sim} \varphi \mathrel{\vcenter{:}}= \top \mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\varphi\). Formulas of \(\mathcal{L}_\mathsf{biLTL}\) are evaluated over (total functional) expanding models as used for \(\mathsf{iLTL}\) in Chapter 5. Let us briefly recall the definition.

Recall that \(f\) being forward confluent is equivalent to \(f\) being order-preserving.

A formula \(\varphi\) is satisfiable over the class of expanding models if there exists an expanding model \(\mathcal{M}\) and a world \(w\) with \(\mathcal{M}, w \models \varphi\) and unsatisfiable otherwise. Moreover, \(\varphi\) is valid if \(\mathcal{M}, w \models \varphi\) for all expanding models \(\mathcal{M}\) and all worlds \(w\) and falsifiable otherwise.

6.3 Axiomatization↩︎

This section introduces the axiomatization \(\mathrm{biLTL_H}\) that captures \(\mathcal{L}_\mathsf{biLTL}\)-validities over expanding models. As mentioned in the introduction, to obtain a sound and complete system in the presence of co-implication it suffices to expand \(\mathrm{iLTL_H}\) by standard rules for \(\mathbin{\Box}\). This implies that the system \(\mathrm{biLTL_H}\) does not contain any axioms or rules for the interaction between co-implication and the temporal modalities.

We also define the Hilbert-style axiomatization \(\mathrm{biLTL_H^{\mathbin{{\bigcirc}}}}\) which is obtained from \(\mathrm{biLTL_H}\) by restricting the language (and therefore the axioms and rules) to \(\mathcal{L}_{\mathbin{{\bigcirc}}}\). For example, a formula \(\varphi\) is an instance of an axiom scheme of \(\mathrm{biLTL_H^{\mathbin{{\bigcirc}}}}\) if \(\varphi \in \mathcal{L}_{\mathbin{{\bigcirc}}}\) and is an instance of an axiom scheme of \(\mathrm{biLTL_H}\).

We write \(\Gamma \vdash \varphi\) if \(\varphi\) has a derivation with assumptions in \(\Gamma\) and \(\vdash \varphi\) if \(\Gamma = \emptyset\). Furthermore, we write \(\Gamma \vdash \Delta\) where \(\Delta\) is any set of formulas if there exists a finite subset \(\Delta_0 \subseteq \Delta\) with \(\Gamma \vdash \bigvee \Delta_0\). Note that every \(\mathrm{biLTL_H^{\mathbin{{\bigcirc}}}}\)-derivation is a \(\mathrm{biLTL_H}\)-derivation. Similarly, every \(\mathrm{biLTL_H}\)-derivation in which only formulas of \(\mathcal{L}_{\mathbin{{\bigcirc}}}\) occur is a \(\mathrm{biLTL_H^{\mathbin{{\bigcirc}}}}\)-derivation. Thus we will not display in the notation \(\Gamma \vdash \varphi\) whether derivability is in \(\mathrm{biLTL_H}\) or \(\mathrm{biLTL_H^{\mathbin{{\bigcirc}}}}\), however, it will always be clear from context. The Deduction Theorem for \(\mathrm{biLTL_H}\) and \(\mathrm{biLTL_H^{\mathbin{{\bigcirc}}}}\) is proven as Theorem 3.3; the proof is omitted.

The following lemma is proven in [87].

We will now illustrate how (implicit) interaction between co-implication and temporal modalities arise in proofs of our calculus.

The rest of this section establishes that \(\mathrm{biLTL_H}\) (and hence also \(\mathrm{biLTL_H^{\mathbin{{\bigcirc}}}}\)) is sound with respect to expanding models.

From the previous lemma, soundness of \(\mathrm{biLTL_H}\) is inferred by a standard induction on the height of proofs.

6.4 Completeness for the Next-Fragment↩︎

This section establishes completeness of \(\mathrm{biLTL_H^{\mathbin{{\bigcirc}}}}\) by emplyoing a standard canonical model construction. As the canonical model is also used later on in the completeness proof of \(\mathrm{biLTL_H}\), the following definitions and lemmas apply to both \(\mathcal{L}_\mathsf{biLTL}\) and \(\mathcal{L}_{\mathbin{{\bigcirc}}}\). Write \(\mathcal{L}\) for \({\mathcal{L} \in \{ \mathcal{L}_\mathsf{biLTL},\mathcal{L}_{\mathbin{{\bigcirc}}}\}}\).

The following properties are readily checked for any prime theory \(\Gamma\) (see Lemma 3.16).

Given a set of formulas \(\Gamma\), define \(\mathbin{{\bigcirc}}^{-1} \Gamma \mathrel{\vcenter{:}}= \{\varphi \mid \mathbin{{\bigcirc}}\varphi \in \Gamma\}\).

Next, the standard Lindenbaum Lemma holds for \(\mathrm{biLTL_H}\) and \(\mathrm{biLTL_H^{\mathbin{{\bigcirc}}}}\). The proof is from [87].

We are now ready to define the canonical models for \(\mathcal{L}_\mathsf{biLTL}\) and \(\mathcal{L}_{\mathbin{{\bigcirc}}}\).

The proof of the first part of the following lemma is standard, while the second part was proven in [87].

For the remainder of this section we work exclusively in the language \(\mathcal{L}_{\mathbin{{\bigcirc}}}\) and show that \(\mathrm{biLTL_H^{\mathbin{{\bigcirc}}}}\) is complete.

6.5 Proof Strategy for the Full Language↩︎

The remainder of this chapter is devoted to prove that \(\mathrm{biLTL_H}\) is complete for the class of expanding models. Unlike for \(\mathrm{biLTL_H^{\mathbin{{\bigcirc}}}}\), the Truth Lemma for the canonical model does not hold, since it may be for example that \(\Diamond\varphi\in \Gamma\), but there is no \(n\) such that \(\varphi\in f^n_\mathrm{c}(\Gamma)\). This is because \(\Diamond\varphi \vdash \bigvee _{i<n} \mathbin{{\bigcirc}}^i \varphi\) is not derivable for any specific \(n\), and derivations are finite. Hence it is possible for \(\Diamond\varphi\) to hold but each individual \(\mathbin{{\bigcirc}}^n \varphi\) to fail in a prime theory.

A similar situation occurs for classical linear temporal logic (\(\mathsf{LTL}\)), but one can then pass to a filtration \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\) of \(\mathcal{M}_\mathrm{c}\), i.e. the quotient of \(\mathcal{M}_\mathrm{c}\) modulo the equivalence relation given by \[\Gamma\sim\Gamma' \text{ if and only if } \Gamma\cap \Sigma=\Gamma'\cap \Sigma.\] Assuming \(\Sigma\) is finite, the equivalence class of each prime theory \(\Gamma\) is determined by its characteristic formula \(\chi(\Gamma)\mathrel{\vcenter{:}}= \bigwedge ( \Gamma\cap \Sigma)\).²¹ The filtrated model does respect the semantics of \(\Diamond\). More precisely, \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\) satisfies a version of the Truth Lemma restricted to formulas of \(\Sigma\), which is sufficient as long as \(\Sigma\) contains enough formulas. The tradeoff is that \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\) is no longer equipped with a function, as the quotient may assign more than one temporal successor to each equivalence class of prime theories. To see why, recall that if \(\Gamma \sim \Gamma'\), then \(\Gamma \cap \Sigma = \Gamma' \cap \Sigma\). Since \(\Sigma\) is a finite set, it is possible that there exists a formula \(\varphi \in \Sigma\) such that \(\mathbin{{\bigcirc}}\varphi \not \in \Sigma\), and therefore that \(\mathbin{{\bigcirc}}\varphi \in \Gamma\) but \(\mathbin{{\bigcirc}}\varphi \not \in \Gamma'\). This implies that \(f_c(\Gamma) \not \sim f_c(\Gamma')\). Accordingly, the quotient model must relate the equivalence class of \(\Gamma\) with both equivalences of \(f_c(\Gamma)\) and of \(f_c(\Gamma')\).

However, this is not a problem, since in a later phase one can choose a path \(\Gamma_0,\Gamma_1,\Gamma_2,\dots\) that constitutes a genuine \(\mathsf{LTL}\)-model. In particular, if \(\varphi\) is not derivable, we can choose \(\Sigma\) to be the set of subformulas of \(\varphi\) and their negations and \(\Gamma_0\) so that \(\varphi\not\in \Gamma_0\), thereby obtaining a model falsifying \(\varphi\).

We wish to adapt this strategy, but there is an issue: filtration in general does not conserve order-preservation of the temporal dynamics (i.e. \(w \leq v\) implies \(f(w) \leq f(v)\)), so we must define \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\) differently. This structure should be a quasimodel, which is similar to a model except that the temporal transition function is replaced by a non-deterministic relation. Each point in a quasimodel is assigned a type, which is similar to a prime theory except that a type only decides a finite set of formulas; i.e., a type is a pair \(\Phi=(\Phi^+,\Phi^-)\) of (usually) finite sets of formulas for which a ‘Truth Lemma’ should hold. In other words, a quasimodel is essentially what was called a labelled model in Chapter [c: bi-int ml new]. Quasimodels are designed so that they can be ‘unwound’ into a genuine model, much like for the filtrated model of classical \(\mathsf{LTL}\).

To construct \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\) in the bi-intuitionistic setting, we use the tools and results from Chapter [c: bi-int ml new], where a finite labelled model \(\mathrm I_{ \Sigma }\) was constructed and related to any given model via a dynamic and strongly surjective simulation \(\check{E}_0\). The structure \(\mathrm I_{ \Sigma }\upharpoonright_{dom(\check{E}_0)}\) was shown to be a labelled model, and will play the role of \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\) here. These results were given in a general modal setting, however we will show how they can be readily applied to the specific case of \(\mathsf{biLTL}\).

Much as the characteristic formula \(\chi(\Gamma)\) determines the equivalence class of \(\Gamma\) in the classical setting, we can characterise which points of \(\mathrm I_{ \Sigma }\) are \(\check{E}_0\)-related to a given prime theory \(\Gamma\) using simulation formulas. Unlike the classical setting, we need two distinct formulas, \(\chi^+\) and \(\chi^-\), to capture respectively the ‘positive’ and ‘negative’ information determining a simulation. These simulation formulas enable us to prove that \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\) is indeed a quasimodel.

At the end of the chapter we put all the ingredients together to show that \(\mathrm{biLTL_H}\) is complete for the class of expanding models: the argument is that if \(\varphi\) is not derivable then we can find a prime theory \(\Gamma\) with \(\varphi\in \Gamma ^-\). By choosing a point \(w\) of \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\) with \(w\mathrel {\check{E}_0} \Gamma\), we see that \(\varphi\) is falsified on \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\). By applying the unwinding procedure to \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\), we obtain a genuine model falsifying \(\varphi\). Thus every formula that is not derivable can be falsified in some expanding model, implying that \(\mathrm{biLTL_H}\) is complete.

6.6 Types, Labelled Structures and Quasimodels↩︎

This section introduces the aforementioned relational structures called quasimodels. Many definitions are akin to the definitions of labelled models in Chapter [c: bi-int ml new], but adjusted to the case of \(\mathsf{biLTL}\). From now on, \(\Sigma\) denotes a set of \(\mathcal{L}_\mathsf{biLTL}\)-formulas closed under subformulas.

As before, it is not necessary that \(\Phi^+ \cup \Phi^- = \Sigma\). Thus types are once again ‘partial’. The set of all \(\Sigma\)-types is denoted by \(\mathrm{T}_\Sigma\). The partial orders \(\leq_{\mathrm{T}}\) and \(\subseteq_\mathrm{T}\) are defined as before. Moreover, the notion of a defect of a type is also defined as before, c.f. Definition [d: defects].

Recall the definition of a \(\Sigma\)-labelled poset \(\mathcal{X}=(X, \leq_{\mathcal{X}}, \ell_{\mathcal{X}})\) (c.f. Definition [d: labelled poset]). In Chapter [c: bi-int ml new] sensible relations were defined with respect to a sensibility condition to have a general argument for the multiple frame conditions considered. Here, we only consider one class of frames and therefore only require one specific sensibility condition.

One can easily check that the relation \(S \subseteq \mathrm{T}_\Sigma \times \mathrm{T}_\Sigma\) given by

is a sensibility condition. Therefore every sensible structure considered henceforth is \(S\)-sensible.

We may write simply labelled system or quasimodel when \(\Sigma\) is clear from context. A formula \(\varphi\) is falsified at world \(x\) of a \(\Sigma\)-labelled system \(\mathcal{X}=(X, {\leq}, \ell, R)\) if \(\varphi \in \ell(x)^-\), and satisfied if \(\varphi \in \ell(x)^+\). A formula \(\varphi\) is falsifiable over the class of \(\Sigma\)-quasimodels if there exists a \(\Sigma\)-quasimodel \(\mathcal{X}=(X, {\leq}, \ell, R)\) and a world \(x \in X\) such that \(\varphi\) is falsified at \(x\).

Observe that every expanding model can be regarded as a \(\Sigma\)-quasimodel by simply labelling each world with those formulas in \(\Sigma\) that are true or false respectively. Thus we obtain the following result.

The converse of Lemma 6.10 is also true, but establishing it requires some work. This will be done in the next section. However, we can already state the result for a particular subclass of quasimodels.

6.7 From Quasimodels to Expanding Models↩︎

This section establishes that if a formula in \(\mathcal{L}_\mathsf{biLTL}\) is falsifiable over the class of quasimodels, then it is falsifiable over the class of expanding models. Given a quasimodel falsifying a formula \(\varphi\), we will show how to construct a total functional quasimodel which falsifies \(\varphi\) as well. The construction is similar to the construction of a functional model from a dynamic model presented in Chapter 3, Section 3.3, however the confluence conditions complicate the argument. Applying Lemma 6.11 then yields an expanding model which falsifies \(\varphi\). For the construction it is useful to observe that forward confluence can be iterated, thereby yielding the following lemma for finite \(R\)-paths, which is a generalization of Lemma 5.2.

For the remainder of this section let \(\mathcal{X}=(X, {\leq}, \ell, R)\) be a fixed \(\Sigma\)-quasimodel. Suppose that \(\mathcal{X}\) falsifies some formula \(\varphi \in \Sigma\). We are now going to show how to construct from \(\mathcal{X}\) a total functional \(\Sigma\)-quasimodel falsifying \(\varphi\). Recall that \(\exists{f(x)}\) denotes that \(x \in dom(f)\) and \(\nexists{f(x)}\) that \(x \not \in dom(f)\) for \(f\) a partial function.

In view of [maximal] and the assumption that \(I\) is finite, there is a maximal \(k\) such that \(f^k(x)\) is defined for any \(x\in I\), and hence we may define \(W_{i}\) to be the set of \(x\in I\) such that \(f^{k-i}(x)\) is defined but \(f^{k-i+1}(x)\) is not. This partitions \(I\) into sets \(W_0,\ldots,W_k\), and it is easy to see that \(x \leq_I y\) implies that \(x,y\in W_i\) for some \(i\), and moreover \(f[W_i]\subseteq W_{i+1}\) for all \(i\).

A defect of an \(\mathcal{X}\)-induced structure records that a claim made by its labelling \(\ell_I\) lacks a witness.

Let \(x \in X\) be such that \(\varphi \in \ell(x)^-\). We build a total functional \(\Sigma\)-quasimodel falsifying \(\varphi\) in stages. We start with an \(\mathcal{X}\)-induced structure \(\mathcal{I}_0\) consisting of a single world and then construct in the step \(n+1\) an \(\mathcal{X}\)-induced structure \(\mathcal{I}_{n+1}\) extending \(\mathcal{I}_n\). We make use of a first-in-first-out queue \(D\) that stores the defects of the current \(\mathcal{X}\)-induced structure. Observe that for any \(\mathcal{X}\)-induced structure, the set of defects of said structure is always finite (since the structure and \(\Sigma\) are finite) and non-empty (due to \(\mathbin{{\bigcirc}}\)-defects). The \(\mathcal{X}\)-induced structure \(\mathcal{I}_n\) is defined by induction on \(n\) as follows.

Base case: Define \(\mathcal{I}_0=(I_0, {\leq_0}, \ell_0, f_0)\), where \(I_0 = \{x'\}\) (where \(x'\) is a fresh world not occurring in \(X\)), \({\leq_0} = \{(x',x')\}\), \(\ell_0(x') = \ell(x)\), \(f_0 = \emptyset\), and \(\pi_0(x') = x\). It is straightforward to check that \((\mathcal{I}_0, \pi_0)\) is an \(\mathcal{X}\)-induced structure. Initialise \(D\) with all defects of \(\mathcal{I}_0\) in arbitrary order.

Induction step: Suppose we have defined \(\mathcal{I}_{n}=(I_n, {\leq_n}, \ell_n, f_n)\) and \(\pi_n\), and shown that \((\mathcal{I}_{n},\pi_{n})\) is an \(\mathcal{X}\)-induced structure. By induction hypothesis, \(D\) currently stores all defects of \(\mathcal{I}_n\). We first show how to define \((\mathcal{I}_{n+1},\pi_{n+1})\) and then how to update the queue \(D\). We start by setting \(I_{n+1} = I_n\) and proceed by a case distinction on the defect at the head of the queue \(D\).

(\(\mathbin{{\bigcirc}}\)-defects) Suppose the defect at the head of \(D\) is a \(\mathbin{{\bigcirc}}\)-defect \(y \in I_n\). Choose any \(u \in X\) with \(\pi_n(y)\mathrel R u\). Add a new point \(u'\) to \(I_{n+1}\) and define \(f_{n+1}(y)= u'\), \(\ell_{n+1}(u') = \ell(u)\), and \(\pi_{n+1}(u')=u\). We extend \(f_{n+1}\) to the connected component of \(y\) by adding new worlds, working first ‘bottom up’ starting with worlds covering \(y\). If \(y'\) covers \(y\), use forth-up confluence to find \(z \in X\) with \(\pi_n(y')\mathrel R z\). Add a fresh node \(z'\) to \(\mathcal{I}_{n+1}\) and define \(f_{n+1}(y') = z'\), \(u' \leq_{n+1} z'\) and close \(\leq_{n+1}\) under transitivity and reflexivity,²², \(\pi_{n+1}(z')= z\), and \(\ell_{n+1}(z')=\ell(z)\). Then for \(y''\) covering such \(y'\), use forth-up confluence again (relative to \(y'\)) to define \(f_{n+1}(y'')\), and so on. Next repeat the process for those worlds below \(\{y' \mid y' \geq y\}\) where \(f_{n+1}\) is not yet defined, this time working ‘top down’ and using forth-down confluence. Continue alternating between ‘bottom up’ and ‘top down’ until \(f_{n+1}\) is defined on the connected component of \(y\).

This process terminates because the newly added points are not in the connected component of \(y\), which is finite. Thus if the connected component of \(y\) in \(\mathcal{I}_n\) is of size \(m\), then \(m\) new points are added.

(\(\rightarrow\)-defects) Suppose the defect at the head of \(D\) is a \(\rightarrow\)-defect \((y, \psi \rightarrow \chi)\). Then \(\psi \rightarrow \chi \in \ell_n(y)^-\), but there is no \(z' \in I_n\) with \(y \leq_n z'\), and \(\varphi \in \ell_n(z')^+\) and \(\psi \in \ell_n(z')^-\). As \(\mathcal{X}\) is a quasimodel, there exists \(\pi_n(y) \leq z \in X\) with \(\psi \in \ell(z)^+\) and \(\chi \in \ell(z)^-\). Let \(k\) be largest natural number such that \(f^k_n(y)\) is defined. Using Lemma 6.12, find \(z=z_0\mathrel R z_1\mathrel R\dots \mathrel R z_k\) with \(\pi_n(f^i_n(y)) \leq z_i\). Then add fresh points \(z'_0,\ldots,z'_k\) to \(I_{n+1}\) and extend \(\pi_n\), \(\leq_n\), \(f_n\) and \(\ell_n\) by setting \(\pi_{n+1}(z'_i)=z_i\), \(f^i_n(y) \leq_{n+1} z'_i\), \(f_{n+1}(z'_i)=z'_{i+1}\) and \(\ell_{n+1}(z'_i)=\ell(z_i)\).

This process terminates because there is a maximal number \(l\) such that every point in \(I_n\) has at most \(l\) temporal successors. Therefore \(k \leq l\) new points are added.

(\(\mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\)-defects) Suppose the defect at the head of \(D\) is a \(\mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\)-defect \((y, \psi \mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\chi)\). The construction of \((\mathcal{I}_{n+1}, \pi_{n+1})\) is then just as for \(\rightarrow\)-defects.

(\(\Diamond\)-defects) Suppose the defect at the head of \(D\) is a \(\Diamond\)-defect \((y, \Diamond\psi)\). Then \(\nexists{f_n(y)}\) and \(\Diamond\psi \in \ell_n(y)^+\), but \(\psi \not \in \ell_n(y)^+\). As \(\mathcal{X}\) is a quasimodel we find \(u_1, \ldots, u_n \in X\) with \(\pi_n(y)\mathrel R u_1\mathrel R u_2\mathrel R \ldots\mathrel R u_n\) and \(\psi \in \ell(u_n)^+\). We add worlds \(u'_1, \ldots, u'_n\) to \(I_{n+1}\) with \(\pi_{n+1}(u'_i) = u_i\), \(f_{n+1}(y) = u'_{1}\) and \(f_{n+1}(u'_i) = u'_{i+1}\), and \(\ell_{n+1}(u'_i) = \ell (u_i)\). Then we proceed as in the case of a \(\mathbin{{\bigcirc}}\)-defect to define \(f_{n+1}\) on the connected component of \(y\), and proceed inductively to define \(f_{n+1}\) on the connected component of each \(u'_i\). In this case, we must add \(n\)-many components for some natural number \(n\). Hence, the construction for ‘next’-defects must be repeated \(n\)-many times. Thus the termination of this process is proven by induction on \(n\), with a secondary induction on the number of worlds in a component as in the \(\mathbin{{\bigcirc}}\)-defect case.

(\(\mathbin{\Box}\)-defects) Suppose the defect at the head of \(D\) is a \(\mathbin{\Box}\)-defect \((y, \mathbin{\Box}\psi)\). The construction is then as for \(\Diamond\)-defects.

Updating D We have shown how to construct \((\mathcal{I}_{n+1}, \pi_{n+1})\) from \((\mathcal{I}_n, \pi_n)\). Next we show how to update the queue \(D\). First, delete every defect from \(D\) that has been resolved in the construction of \((\mathcal{I}_{n+1}, \pi_{n+1})\) (observe that in each of the above cases it is possible that multiple defects have been resolved at once). Then each remaining defect is rewritten as follows. Remaining \(\rightarrow\)- or \(\mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\)-defects are left unchanged. For an \(\Diamond\)-defect \((y, \Diamond\psi)\) if \(\nexists{f_{n+1}(y)}\) holds, then the defect is left unchanged. Otherwise there are \(u_1, \ldots, u_k\) with \(f_{n+1}(y)=u_1, f_{n+1}(u_1)=u_2, \ldots, f_{n+1}(u_{k-1}) = u_k\) and \(\nexists{f_{n+1}(u_k)}\). By assumption \(\Diamond\psi \in \ell_{n+1}(u_k)^+\) and \(\psi \not \in \ell_{n+1}(u_k)^+\). Thus overwrite \((y, \Diamond\psi)\) with \((u_k, \Diamond\psi)\). The \(\mathbin{\Box}\)-defects and \(\mathbin{{\bigcirc}}\)-defects are overwritten in the same way. Finally, add all new defects of \(\mathcal{I}_{n+1}\) to the tail of the queue.

Observe that by construction, each \(\mathcal{I}_{n+1}\) contains \(\mathcal{I}_n\) as a substructure. Define \((\mathcal{I}_\omega \mathrel{\vcenter{:}}= (I_\omega, {\leq_\omega}, \ell_\omega, f_\omega), \pi_\omega)\) where \[\lambda_\omega = \bigcup_{n < \omega} \lambda_n\] for \(\lambda \in \{I, {\leq}, \ell, f, \pi\}\). Observe that \(x' \in I_\omega\) with \(\pi_\omega(x') = x\) and therefore \(\varphi \in \ell_\omega(x')^-\). Thus \(\mathcal{I}_\omega\) falsifies \(\varphi\).

Combining these results we obtain the following lemma.

Finally, we obtain the main result of this section:

6.8 Simulations↩︎

A key ingredient in our completeness proof will be to relate worlds in a finite quasimodel to prime theories in the canonical model. As in chapter [c: bi-int ml new] dynamic simulations will be used to achieve this. Let us briefly recall the definitions.

The following result is crucial for the completeness argument, yet straighforward to prove. Given labelled systems \(\mathcal{X}=(X, \leq_\mathcal{X}, \ell_\mathcal{X}, R_\mathcal{X})\) and \(\mathcal{Y}=(Y, \leq_\mathcal{Y}, \ell_\mathcal{Y}, R_\mathcal{Y})\) and a simulation \(E \subseteq X \times Y\), let \(X{\upharpoonright_{dom(E)}}\) be the structure obtained from restricting \(\mathcal{X}\) to the domain of \(E\), as before.

Finally, let us briefly recall the definition of a dynamic simulation.

6.9 Finite Quasimodel Property↩︎

In this section, we show that every falsifiable formula is falsified on a finite quasimodel. We wish to apply the techniques and results from Chapter [c: bi-int ml new] to \(\mathsf{biLTL}\), where we proved that every \(\mathcal{L}_{\mathsf{bIM}}\)-formula falsified on an expanding model is falsified in a finite labelled model. The caveat is that the finite model property was proven for a language with two modalities, which here we denote \(\blacklozenge\) and \(\blacksquare\). These do not correspond to our own \(\Diamond\) and \(\mathbin{\Box}\), but rather both correspond to \(\mathbin{{\bigcirc}}\), which, being a functional modality, is self dual.

In order to apply the results from Chapter [c: bi-int ml new], let us start by considering only the language \(\mathcal{L}_{\mathbin{{\bigcirc}}}\). Recall the definition of a \(\Sigma\)-type for the language \(\mathcal{L}_{\mathsf{bIM}}\) (c.f. Definition [d: type]) and identify both \(\blacklozenge\) and \(\blacksquare\) with \(\mathbin{{\bigcirc}}\). To avoid confusion, we denote these types by \(\mathrm{T}_{\Sigma}^{\mathbin{{\bigcirc}}}\). Recall the definition of a sensibility condition (c.f. Definition [d: sensibility condition]). The following theorem combines the results proven in Chapter [c: bi-int ml new] and applied to \(\mathcal{L}_{\mathbin{{\bigcirc}}}\).

Note that the structure \(\mathbb{U}\) yields finite quasimodels for \(\mathcal{L}_{\mathbin{{\bigcirc}}}\). In order to apply Theorem 6.5 to the full language \(\mathcal{L}_\mathsf{biLTL}\), the idea is to regard each formula of the form \(\Diamond\varphi\) or \(\mathbin{\Box}\varphi\) as a proposition, but replace e.g. \(\mathbin{\Box}\varphi\) by \(\varphi\wedge\mathbin{\Box}\varphi\) in order to ensure that our types still satisfy the correct conditions for \(\mathbin{\Box}\) and \(\Diamond\). To that end we introduce the concept of a fleeting type. The intuition is that a fleeting type is a \(\Sigma\)-type which does not satisfy the conditions involving \(\Diamond\) and \(\mathbin{\Box}\). Therefore, when uniformly replacing instances of \(\Diamond\) and \(\mathbin{\Box}\) by fresh propositions, a fleeting type becomes simply a \(\mathrm{T}_\Sigma^{\mathbin{{\bigcirc}}}\)-type.

A fleetingly labelled poset is then a labelled poset, albeit labelled by fleeting types. The formal definition is as follows.

For a formula \(\varphi \in \mathcal{L}_\mathsf{biLTL}\), define \(\tau(\varphi)\) by recursively replacing instances of \(\mathbin{\Box}\varphi\) by \(\varphi\wedge{\mathbin{{\bigcirc}}\mathbin{\Box}}\varphi\), and instances of \(\Diamond\varphi\) by \(\varphi\vee\mathbin{{\bigcirc}}\Diamond\varphi\). Formally, \(\tau (\varphi)\) is definded inductively as follows.

Given a set of formulas \(\Sigma \subseteq \mathcal{L}_\mathsf{biLTL}\), define \(\tau(\Sigma)=\{\tau(\varphi) \mid \varphi\in \Sigma\}\). Similarly, if \(\Phi\) is a fleeting type then \(\tau (\Phi)=(\tau ({\Phi^+}),\tau ({\Phi^-}))\), and if \(\mathcal{X}\) is a fleetingly labelled poset then \(\tau({\mathcal{X}})\) is the same as \(\mathcal{X}\) but labelled by \(\tau ({\ell_\mathcal{X}})\). Finally, for a set of formulas \(\Theta\subseteq\tau(\Sigma)\) define \(\tau^{-1}(\Theta) = \{\varphi \in \Sigma \mid \tau(\varphi) \in \Theta\}\), and for a type \(\Phi\) define \(\tau^{-1} (\Phi) = (\tau^{-1} ({\Phi^+}),\tau^{-1}({\Phi^-}))\).

It remains to define a suitable sensibility condition in order to apply Theorem 6.5. To this end, let \(\Phi, \Psi\) be fleeting \(\tau(\Sigma)\)-types and define \(\Phi \mathrel{S} \Psi\) if and only if \((\tau^{-1}(\Phi), \tau^{-1}(\Psi))\) is sensible.

Recall that the canonical model for the full language \(\mathcal{L}_\mathsf{biLTL}\) is denoted by \(\mathcal{M}_c\).

Therefore if a formula \(\varphi \in \mathcal{L}_\mathsf{biLTL}\) is falsifiable, we have \(\not \vdash \varphi\) by soundness. By the Lindenbaum Lemma there exists a prime theory \(\Gamma \in W_c\) with \(\varphi \not \in \Gamma\). Thus there exists a world \(w \in J\) with \(\varphi \in \ell_{\frac{\mathcal{M}_\mathrm{c}}{\Sigma}}(w)^-\). To obtain completeness, in the presence of Theorem 6.4 it thus suffices to show that \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\) is not only a labelled system, but in fact a quasimodel. This is in no way trivial to establish, and will be done in the next sections using so called simulation formulas.

6.10 Simulation Formulas↩︎

As before, \(\Sigma \subseteq \mathcal{L}_\mathsf{biLTL}\) is assumed to be finite and closed under subformulas. Consider a \(\Sigma\)-labelled poset \(\mathcal{X}=(X, \leq_\mathcal{X}, \ell_\mathcal{X})\) and let \(x, y \in X\). Recall that a non-repeating path from \(x\) to \(y\) is a finite sequence \((\rho(i))_{i \leq n}\) of (pairwise) distinct worlds, such that \(\rho(0) = x\), \(\rho(n) = y\), and for all \(0 \leq i <n\) either \(\rho(i)\) covers \(\rho(i+1)\) or \(\rho(i+1)\) covers \(\rho(i)\). If \(\rho = (\rho(i))_{i \leq n}\), the length \(\lvert \rho \rvert\) of \(\rho\) is \(n\). Let \[\mathsf{ZZP}(x) \mathrel{\vcenter{:}}= \{ \rho \mid \rho \text{ is a non-repeating path starting at } x\}.\]

Observe that \(\mathsf{T}(x)\) is a finite tree with the path \((x)\) as root. As before, Given \(\rho \sqsubseteq \rho'\), we write \(\rho' - \rho\) for the final segment of \(\rho'\) after \(\rho\). Moreover, we write \({\uparrow}(\rho' - \rho)\) if each element in \(\rho' - \rho\) covers its predecessor in \(\rho'\), and \({\downarrow}(\rho' - \rho)\) if each element in \(\rho' - \rho\) is covered by its predecessor in \(\rho'\). For \(\rho \in \mathsf{ZZP}(x)\), the height of \(\rho\) is defined as \(h(\rho) \mathrel{\vcenter{:}}= \max\{\lvert \rho' - \rho \rvert \mid \rho \sqsubseteq \rho'\}\).

We now define, for \(x\) in a finite, acyclic labelled poset, the simulation formulas \(\chi^+(x)\) and \(\chi^-(x)\), which together encode all worlds accessible from \(x\) via a non-repeating path. Therefore, satisfying or falsifying \(\chi^+(x)\) or \(\chi^-(x)\) respectively at some world \(y\) of a labelled poset is equivalent to the existence of a simulation involving \(x\) and \(y\); see Proposition 6.7.

We define \(\chi^+(x)\) and \(\chi^-(x)\) by working ‘outside-in’ on \(\mathsf{T}(x)\), i.e. recursively from the leaves of \(\mathsf T(x)\) to the root, exploiting the following.

1. By asserting a formula \(\varphi \mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\psi\) we can express that there is a world below where \(\varphi\) holds and \(\psi\) does not.

2. By denying a formula \(\varphi \rightarrow \psi\) we can express that there is a world above where \(\varphi\) holds and \(\psi\) does not.

We begin by defining for each path \(\rho\) in \(\mathsf T(x)\) different from \((x)\) a formula \(\varphi_\rho\). The simulation formulas are then composed from these formulas \(\varphi_\rho\). Recall that by convention \(\bigwedge \emptyset \mathrel{\vcenter{:}}= \top\) and \(\bigvee \emptyset \mathrel{\vcenter{:}}= \bot\).

For a path \(\rho = (\rho(i))_{i\leq n}\) let \(\mathbf{f}(\rho) \mathrel{\vcenter{:}}= \rho(n)\), i.e. \(\mathbf{f}(\rho)\) denotes the final element of \(\rho\). Let \[\mathbf{f}[\mathsf{ZZP}(x)] = \{ \mathbf{f}(\rho) \mid \rho \in \mathsf{ZZP}(x)\}.\]

Recall that \(\mathcal{M}_\mathrm{c} = (W_\mathrm{c},{\leq_\mathrm{c}},f_\mathrm{c},V_\mathrm{c})\) is the canonical model. Moreover, recall that by Lemma 6.8 if \(\varphi \rightarrow \psi \not \in \Gamma\) for \(\Gamma \in W_c\), then there exists \(\Delta \in W_c\) with \(\Gamma \leq_c \Delta\) and \(\varphi \in \Delta\) and \(\psi \not \in \Delta\). Similarly, if \(\varphi \mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\psi \in \Gamma\), then there exists \(\Delta \in W_c\) with \(\Delta \leq_c \Gamma\) and \(\varphi \in \Delta\) and \(\psi \not \in \Delta\).

Next we establish some \(\mathsf{biLTL}\)-derivable properties of \(\chi^+\) and \(\chi^-\). We begin with the former. These properties are established by using Proposition 6.7 to see that they are present in every prime theory in the canonical model and so derivable. As before, \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}= (U ,{\leq},R,\ell)\); the reflexive transitive closure of \(R\) is denoted \(R^*\).

The formula \(\chi^-\) behaves ‘dually’, as follows.

6.11 Completeness↩︎

The simulation formulas \(\chi^+\) and \(\chi^-\) are fundamental in the completeness proof. Specifically, they will be used to show that \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\) is \(\omega\)-sensible and hence a quasimodel. Since validity over the class of quasimodels is equivalent to validity over the class of expanding models by Theorem 6.4, completeness will follow. The following lemma is the first step towards establishing \(\omega\)-sensibility. As above, we write \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}= (U,{\leq},R,\ell)\) and \(R^*\) for the reflexive transitive closure of \(R\), and \(E_* \subseteq U\times W_\mathrm{c}\) is the strongly surjective dynamic simulation between \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\) and \(\mathcal{M}_c\), where \(\mathcal{M}_c\) is the canonical model. As in the completeness proof for \(\mathrm{IM_{H}}\) in Chapter 3, let \(R^*(w)\) be the reachable component of \(w\), i.e. \(R^*(w) = \{ v \in U \mid w \mathrel{R}^* v\}\). In order to show that \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\) is \(\omega\)-sensible, we need to use formal induction over the reachable component of worlds. The following lemma will help us achieve this.

In order to complete our proof that \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\) is \(\omega\)-sensible, it suffices to apply the induction rules \(\mathsf{Ind}_{\mathbin{\Box}}\) and \(\mathsf{Ind}_{\Diamond}\) of our calculus to the formulas of Lemma 6.20.

We are now ready to prove that our calculus is complete.

This follows from the fact that \(\mathsf{biLTL}\) is axiomatisable and has a finite quasimodel property (with a computable bound on the ‘finite’).

6.12 Conclusion↩︎

The main contribution of this chapter is the presented sound and complete axiomatization for bi-intuitionistic linear temporal logic. This is the first finite axiomatization for a logic extending intuitionistic linear temporal logic over the full temporal language including ‘next’, ‘eventually’ and ‘henceforth’ and thus solves a long standing open problem. Our method of proving completeness was based on the finite model construction from Chapter [c: bi-int ml new] which was used to obtain a finite ‘filtrated’ model which embeds into the canonical model via a dynamic simulation. The proof is thereby an interesting adaptation of classical techniques for LTL to the intuitionistic realm, illustrating in particular the significant increase in the difficulty of the mathematical theory. The crucial ingredient for obtaining a complete axiomatization is the co-implication, whose presence is exploited to prove \(\mathsf{iLTL}\)-validites such as the \(\mathbf{RV}\)-formula. As a consequence we noted that the axiomatization is not conservative over the \(\mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\)-free fragment of the logic. In the completeness proof the co-implication is crucial in establishing that the modal accessibility relation of \(\frac{\mathcal{M}_\mathrm{c}}{\Sigma}\) is \(\omega\)-sensible for \(\mathbin{\Box}\) case (while implication was used to prove the \(\Diamond\) case). This leads us to the first question left open by our work:

We are optimistic that this is indeed possible, partly due to the fact that Menéndez Turata managed to obtain a sound and complete cyclic proof system for \(\mathsf{iLTL}\) over the full language [24], which might be used to extract a finite axiomatization. We leave this problem for future work.

An interesting corollary of this chapter is that \(\mathbin{\tikz[baseline=-.5ex] \draw[-to reversed] (0,0) -- (1em,0);}\) cannot be extended to the class of topological models while validating bi-intuitionistic logic, since as verified in [86], this would mean that the class of dynamic topological models would validate \(\mathsf{biLTL}\), and hence validate \(\mathbf{RV}\), which we know by Example 6.1 not to be the case.

A natural next step to extend our work would be to turn to proof theory with the aim of developing an analytic sequent calculus for bi-intuitionistic linear temporal logic. This is a follow up problem to Question [q: proof theory for biml]: an analytic sequent calculus for bi-intuitionistic modal logic could be extended by fixed point rules, admitting analytic non-wellfounded proofs. However, this would require to combine nested sequents with non-wellfounded branches, which is notoriously difficult to handle (see Question 4.1).

7 English Summary↩︎

This thesis develops the mathematical theory of intuitionistic dynamic logics - extensions of intuitionistic propositional logic with modalities and fixed point operators. Such systems provide formal tools for reasoning about change, such as encountered in mathematical systems evolving over time or in the knowledge state of an agent after an information update.

We investigate five intuitionistic dynamic logics: intuitionistic master modality, intuitionistic common knowledge logic, intuitionistic linear temporal logic, bi-intuitionistic modal logic and bi-intuitionistic linear temporal logic. On the proof theoretic side we develop sound and complete Hilbert-style axiomatizations as well as non-wellfounded and cyclic sequent calculi. On the semantic side we study these logics over various classes of dynamic models, which are birelational Kripke models satisfying confluence and frame conditions. We establish expressivity results, the finite model property, decidability, as well as complexity bounds.

The main contributions are threefold. First, we develop analytic cyclic sequent calculi for intuitionistic master modality and common knowledge logic, where completeness is obtained by a robust proof search argument. Second, we obtain the finite model property and decidability for bi-intuitionistic modal logic via an intricate combinatorial analysis of dynamic models. Third, we develop a sound and complete axiomatization for intuitionistic linear temporal logic featuring the temporal operators next, eventually and henceforth, thereby providing a positive answer to the long-standing open question concerning the existence of a finite axiomatization.

8 Nederlandstalige Samenvatting↩︎

Dit proefschrift ontwikkelt de wiskundige theorie van intuïtionistische dynamische logica’s — uitbreidingen van de intuïtionistische propositionele logica met modaliteiten en fixpunt-operatoren. Dergelijke systemen bieden formele instrumenten om te redeneren over verandering, zoals die optreedt in wiskundige systemen die in de tijd evolueren of in de kennis­toestand van een agent na een informatie-update.

We onderzoeken vijf intuïtionistische dynamische logica’s: intuïtionistische meester­modaliteit, intuïtionistische gemeenschappelijke-kennis­logica, intuïtionistische lineaire temporele logica, bi-intuïtionistische modale logica en bi-intuïtionistische lineaire temporele logica. Aan de bewijstheoretische kant ontwikkelen we correcte en volledige Hilbert-stijl-axiomatiseringen, evenals niet-welgegronde en cyclische sequent-calculi. Aan de semantische kant bestuderen we deze logica’s over verschillende klassen van dynamische modellen, dat wil zeggen birelationele Kripke-modellen die voldoen aan confluentie en framecondities. We bewijzen resultaten over expressiviteit, de eindig-model-eigenschap, beslisbaarheid en complexiteitsgrenzen.

De belangrijkste bijdragen zijn drievoudig. Ten eerste ontwikkelen we analytische cyclische sequent-calculi voor intuïtionistische meester­modaliteit en gemeenschappelijke-kennis­logica, waarbij volledigheid wordt verkregen via een robuust bewijszoek-argument. Ten tweede verkrijgen we de eindig-model-eigenschap en beslisbaarheid voor de bi-intuïtionistische modale logica door middel van een verfijnde combinatorische analyse van dynamische modellen. Ten derde ontwikkelen we een correcte en volledige axiomatisering voor de intuïtionistische lineaire temporele logica met de temporele operatoren next, eventually en henceforth, waarmee een positief antwoord wordt gegeven op de lang openstaande vraag naar het bestaan van een eindige axiomatisering.

References↩︎

---

1. We also use \(\leq\) for the standard smaller-equal relation on the set of natural numbers. Note that \(\leq\) is a well-order on \(\omega\).↩︎

2. Technically speaking, the displayed graph is a frame and not a model, since the valuation is not displayed. Since whenever a frame is depicted, the valuation is provided in the example, we do not make this distinction here.↩︎

3. However, there are some exceptions, for example the choice rules employed in Chapter 3.↩︎

4. Technically, since sequents are ordered pairs of sets of formulas, formulas can serve simultaneously as principal and as side formulas in a rule instance. In such an instance the principal formula also occurs in the premises. Thus it is possible to always continue the proof search even if only finitely many sequents occur; however, such strategy for proof search is hardly reasonable.↩︎

5. In that case one needs to be careful with the inductive definition of the language to guarantee that every formula induces a monotone function.↩︎

6. See Definition 2.19.↩︎

7. Observe that \(u_0\) might be identical to \(\pi_n(y)\). Nevertheless, we add a fresh world \(y_0\) to \(I_n\) which in this case would be a copy of \(y\).↩︎

8. It might be that at step \(m > n\) a \(\larger[-1.5]\square\)-defect situated at a world \(x\) in \(I_n\) is resolved. But in that case the construction first adds a new world above \(x\) and then a modal successor for that new world. The case for \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\)-defects is similar.↩︎

9. A semantic analysis immediately shows that the other direction, i.e. \(\vdash \larger[-1.5]\square(\varphi \vee \psi) \rightarrow (\larger[-1.5]\square\varphi \vee \larger[-1.5]\square\psi)\), should not* hold. The soundness theorem (c.f. Theorem 3.4) will confirm this intuition.*↩︎

10. This is a semantic notion of invertibility.↩︎

11. Although the calculus \(\mathrm{nIM}\) is only used to show completeness of \(\mathrm{cIM}\), let us note here that \(\mathrm{nIM}\) is also sound: this follows from soundness of \(\mathrm{cIM}\) and Lemma 3.32.↩︎

12. Since \(\mathcal{M}\) is a triangle model, we have \(w \mathrel{(R \circ {\leq})} v\). However, in the refutation \(v\) does not contain a node which is a modal premise of the same \(\mathsf{C_t}\)-rule instance of which \(t_w\) is a conclusion of. Therefore this additional case has to be considered.↩︎

13. If \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi\) is unfocused, then the saturation clause 7. guarantees this. Otherwise the saturation clause 8. guarantees it. In the second case, there exists a node \(s \in w\) with \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi^f \in \Delta_s\). Since \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi^f\) cannot occur in \(\Delta_{t_w}\), there must be a (non-preserving) application of \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\mathsf{R}\) with \(\ooalign{\larger[-1.5]\square\cr \hidewidth\raise.035ex* \mkern 1.12mu\cr}\varphi^f\) as principal formula.↩︎

14. This requires \(f\) to be a total function, as otherwise there could be maximal worlds in \(\leq\) which have no successor.↩︎

15. For the interested reader who is unwilling to try out the many possible and sensible candidates for a proof, let us remark here that both possible sequents in the premise are invalid. Thus the soundness result presented in the next section will provide an alternative and simpler proof.↩︎

16. We will close every canonical model under triangle confluence and not mention it in the next cases.↩︎

17. We use different names for the system and some of the rules than [22].↩︎

18. This will not be mentioned again henceforth.↩︎

19. Formally, a trace \((\varphi_i)_{i}\) passes degeneratively through \(\mathbin{\mathsf{U}}\mathrm{L}\) if there is a \(\varphi_j\) of the form \(\varphi\mathbin{\mathsf{U}}\psi^n\) such that \(\varphi_{j+1}\in\{\varphi^n,\psi^n\}\).↩︎

20. If the reader has skipped Chapter 3, it may be informative to go back and briefly review the key ideas presented there.↩︎

21. Note that this is essentially what was done in the completeness proof for \(\mathrm{IM_H}\), but we defined \(\frac{\mathcal{M}_c}{\sim}\) directly instead of via a filtration.↩︎

22. We will always close \(\leq_{n+1}\) under transitivity and reflexivity and will not mention it in the following items.↩︎