Topological modal logics satisfying finite chain conditions (Q5937828)

This paper investigates some interesting modifications of the semantics of topological modal logic (TML). Originally introduced by L. S. Moss and R. Parikh (1992), TML is a modal language with two modal operators, \(K\) (knowledge) and \(\square\) (effort), whose semantics differs from that of ordinary modal operators to a large extent: their underlying frames consist of a non-empty set \(X\) and a distinguished set \(O\) of subsets of \(X\), called the opens (although they are not necessarily open in the topological sense). The systems of TMLs may provide a suitable framework for reasoning about the behaviour of effective approximations to infinite objects, such as classes of subset spaces, tree-like spaces, computer programs, etc. The main purpose of the paper is to examine TML when finite descent conditions on the \(O\) of opens (or finiteness conditions on the trees modelling the program executions) are imposed. Within the newly defined TML framework, the author studies two appropriate logics; (1) The first TML system, denoted D1, corresponds to frames sharing the following property of \(O\), called weak bounded chain condition (WBCC): every descending chain containing a given point \(x\) is of bounded length, with the bound depending on \(x\). An axiom system for D1 is given in order to satisfy the WBCC for topological model theory of spaces, and a corresponding soundness and completeness result for D1 is proved. (2) The second TML proposed system, denoted D2, is characterized by the class of spaces fulfilling the bounded chain condition (BCC), viz. every chain of opens is of bounded length by definition. The class of finite irreflexive computation tree appears to be a particular case. A sound and complete axiomatization system for D2 is proposed. The finite model property (FMP) is examined for TML systems D1 and D2. While FMP does not hold for D1, for the system D2 not only FMP is proved to be valid but also a certain small model property. Finally, since in both systems D1 and D2 the class of semantical structures coincides with a class of trees that satisfy a certain finiteness condition, D1 and D2 represent generalizations of the well-known modal system G to the context of TMLs.