Completeness of S4 with respect to the real line: revisited (Q705542)

This is a proof of topological completeness of S4 for the real interval \((0,1)\), simplifying the original proof by \textit{J. C. C. McKinsey} and \textit{A. Tarski} [Ann. Math. (2) 45, 141--191 (1944; Zbl 0060.06206)]. It provides a continuous and open mapping of \((0,1)\) onto an arbitrary finite rooted Kripke model \(K\), which is sufficient for topological bisimulation. First, a subcase of the intuitionistic subcase is treated, when \(K\) is a tree. The embedding \(f:(0,1)\to K\) is defined by recursion of the height of the tree. Then the full intuitionistic subcase is handled by operation of the disjoint sum of trees with identification of some nodes. After that, the general case of S4 is redone using a similar construction interleaved at each step with certain embeddings into more and more complicated subsets of the Cantor set. Analysis of this construction allows the authors to prove that S4 is complete for valuations \(V\) where \(V(p)\) for each propositional variable \(p\) belongs to a Boolean algebra generated by countable unions of intervals and points. The results are extended to a system containing S5 and a certain connecting axiom. Another simplification (allowing a further simplification using ideas of this paper) was obtained by \textit{M. Aiello, J. van Benthem} and the first author [J. Log. Comput. 13, 889--920 (2003; Zbl 1054.03015)] and independently by the reviewer and \textit{T. Zhang} [``A proof of topological completeness for S4 in \((0,1)\)'', Ann. Pure Appl. Logic 133, 231--245 (2005; Zbl 1133.03009)].