Lattices of Tense Logics: Tabularity, Completeness and Decidability
Qian Chen

Abstract:
This thesis investigates the lattices of tense logics. A tense logic is a normal bimodal logic equipped with a future-looking necessity modality $\Box$ and a past-looking possibility modality $\blacklozenge$, with the modalities $\Box$ and $\blacklozenge$ forming an adjoint pair. For each tense logic $L$, the set $\mathsf{NExt}(L)$ of all tense logics extending $L$ forms a lattice. Tense logics $\mathsf{K}_{t}$, $\mathsf{K4}_{t}$ and $\mathsf{S4}_{t}$ are analogues of the well-known modal logics $\mathsf{K}$, $\mathsf{K4}$ and $\mathsf{S4}$, respectively. In this thesis, we study the following topics: (1) Post-completeness in the lattice $\mathsf{NExt}(\mathsf{K}_{t})$; (2) tabularity in the lattice $\mathsf{NExt}(\mathsf{K}_{t})$; (3) pretabularity in the lattice $\mathsf{NExt}(\mathsf{S4}_{t})$; (4) the degree of Kripke incompleteness in $\mathsf{NExt}(\mathsf{K}_{t})$, $\mathsf{NExt}(\mathsf{K4}_{t})$ and $\mathsf{NExt}(\mathsf{S4}_{t})$; and (5) (un)decidability of logical properties in $\mathsf{NExt}(\mathsf{K}_{t})$, $\mathsf{NExt}(\mathsf{K4}_{t})$ and $\mathsf{NExt}(\mathsf{S4}_{t})$.

The first part of the thesis studies logics near the top of the lattices of tense logics, focusing on tabularity and Post-completeness. A tense logic is tabular if it is the logic of a finite tense algebra. We give a new characterization of tabular tense logics based on a family of formulas $\mathsf{tab}^T_n$. A tense logic is Post-complete if it is consistent and has no consistent proper extension. We provide full characterizations of Post-complete tabular tense logics and Post-complete tense logics, respectively. Moreover, we study the Post-number of tense logics. We show that for each cardinal $\alpha$, if $1 \leq \alpha \leq \aleph_0$ or $\alpha = 2^{\aleph_0}$, then there exists a tense logic with Post-number $\alpha$.

Next, we study pretabular tense logics in $\mathsf{NExt}(\mathsf{S4}_{t})$, which form the boundary of tabular tense logics, in the sense that a pretabular logic $L$ is non-tabular while every proper extension of $L$ is tabular. We introduce tense logics with bounded parameters and give a full characterization of pretabular fully bounded tense logics. Then, we give full characterizations for pretabular logics extending $\mathsf{S4{.}3}_{t}$ and $\mathsf{S4BP}_{2,2}^{2,\omega}$, respectively. Finally, we show that there are continuum many pretabular extensions of $\mathsf{S4BP}^{2,\omega}_{2,3}$, which answers the open problem about the cardinality of pretabular extensions of $\mathsf{S4}_{t}$.

The second part of the thesis focuses on the structure of lattices of tense logics as a whole. To this end, we begin by studying the degree of Kripke incompleteness of tense logics. A celebrated result in this area is Blok's dichotomy theorem of the degree of Kripke incompleteness for $\mathsf{NExt}(\mathsf{K})$, which states that every logic $L\in\mathsf{NExt}(\mathsf{K})$ is of the degree of Kripke incompleteness either $1$ or $2^{\aleph_0}$. We generalize this dichotomy theorem to the lattices $\mathsf{NExt}(\mathsf{K}_{t})$, $\mathsf{NExt}(\mathsf{K4}_{t})$ and $\mathsf{NExt}(\mathsf{S4}_{t})$. Moreover, we discuss the relation between union-splittings, iterated splittings and the degree of Kripke incompleteness.

Finally, we investigate the decidability of logical properties of tense logics. A central theme of the study of modal logic is to determine whether a logic has a certain logical property. In this thesis, we prove that strict Kripke completeness is decidable in $\mathsf{NExt}(\mathsf{K4}_{t})$. Also, we give a general criterion for a logical property to be undecidable in $\mathsf{NExt}(\mathsf{K4}_{t})$. Finally, we show that in $\mathsf{NExt}(\mathsf{S4}_{t})$, strictly Kripke completeness is decidable, while tabularity, Kripke completeness and decidability are undecidable.