Completeness by construction for tense logics of linear time
Dick H. J. de Jongh, Frank Veltman, Rineke Verbrugge · UvA-DARE (University of Amsterdam) · 2004
It is rather unusual for the recipient of a Liber Amicorum to be the co-author of one of the contributions. With this article such a strange situation does occur, but hopefully without the recipient knowing anything about it until he received this Liber Amicorum. The present article is based on a manuscript written by the three of us in the mid-eighties, when Rineke Verbrugge, then an undergraduate student, took a course on intensional logics by Dick de Jongh and Frank Veltman, and tried to apply their “constructive” method to tense logics for linear discrete structures consisting of a number of consecutive copies of Z. This constructive method had been developed in the seventies and was in wide use in Amsterdam, where several researchers contributed to it. The method was used to prove completeness of many tense logics (see e.g. [1, Theorem II.2.3.18] for a completeness proof of the logic for the rationals using “construction by finite stages” and [4] for many examples that also appear in this paper), of conditional logics, and of interpretability logics [5]. Even though the standard way to prove completeness for tense logics is the one pioneered by Segerberg [6], using filtration and transformations like bulldozing on canonical models, Burgess has always been a proponent of the constructive method [3], which has lately found its way into standard modal logic texts as the step-by-step-method [2]. In the mid-eighties, we were rather ambitious and wanted to characterize all complete tense logics of discrete and dense time. In the second edition of The Logic of Time, Van Benthem even announced that we had succeeded to do so in our unpublished “All logics for dense and discrete linear time” [1, Addenda and corrigenda]. The manuscript was promptly hidden in a deep drawer. In the present version, composed by Rineke Verbrugge and Frank Veltman, the goal of the paper is more modest: simply to present some short and elegant stepby-step completeness proofs for some interesting tense logics for dense and discrete linear time.