×

Axiomatising first-order temporal logic: Until and since over linear time. (English) Zbl 0864.03015

The author presents a complete axiomatisation for first-order temporal logic with the connectives \(U\) (Until) and \(S\) (Since) over all linear time flows. Adding two more axioms, he obtains also a complete axiomatisation over the rational numbers flow of time. The result extends the corresponding one of Burgess for propositional logic, as well as Scott’s result for first-order temporal logic with the connectives \(F\) and \(P\), but the proof is by no means a straightforward generalization of them. In fact, he avoids “datings” for reducing \(U\), \(S\) to \(F\) and \(P\), and unnatural rules. For the construction of the model of a consistent set of formulas, he uses subtle and nice techniques in order to cope with completeness of quantified formulas (“omega completeness”). The model is constructed a the limit of finite pieces in countably many steps over a subset of the rationals.

MSC:

03B45 Modal logic (including the logic of norms)
Full Text: DOI

References:

[1] Andréka, H., V. Goranko, S. Mikulás, I. Németi, and I. Sain, 1995, ?Effective temporal logics of programs?, In [3].
[2] Bell, J., and M. Machover, 1977, A course in Mathematical Logic, North-Holland. · Zbl 0359.02001
[3] Bolc, L., and A. Szalas, 1995, editors. Time and Logic, UCL Press, London.
[4] Burgess, J. P., 1982, ?Axioms for tense logic I: ?since? and ?until? Notre Dame J. Formal Logic, 23, 367-374. · doi:10.1305/ndjfl/1093870149
[5] Gabbay, D., I. Hodkinson, and M. Reynolds, 1994, Temporal Logic: Mathematical Foundations and Computational Aspects, Vol. 1, Oxford University Press. · Zbl 0921.03023
[6] Gabbay, D. M., 1975, ?Model theory for tense logics?, Ann. Math. Logic 8, 185-235. · Zbl 0307.02014 · doi:10.1016/0003-4843(75)90003-0
[7] Gabbay, D. M., and I. M. Hodkinson, 1990, ?An axiomatisation of the temporal logic with until and since over the real numbers?, Journal of Logic and Computation 1, 229-260. · Zbl 0744.03018 · doi:10.1093/logcom/1.2.229
[8] Gabbay, D. M., A. Pnueli, S. Shelah, and J. Stavi, 1980, ?On the temporal analysis of fairness?, In 7th ACM Symposium on Principles of Programming Languages, Las Vegas, 163-173.
[9] Garson, J. W., 1984, ?Quantification in modal logic?, In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, D. Reidel, Dordrecht. · Zbl 0875.03050
[10] Hodges, W., 1984, ?Elementary predicate logic?, In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, D. Reidel, Dordrecht. · Zbl 0875.03035
[11] Manna, Z., and A. Pnueli, 1992, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, New York. · Zbl 0753.68003
[12] Reynolds, M., 1992, ?An axiomatization for Until and Since over the reals without the IRR rule?, Studia Logica 51, 165-194. · Zbl 0785.03006 · doi:10.1007/BF00370112
[13] Szalas, A., 1987, ?Arithmetical axiomatization of first-order temporal logic?, Information Processing Letters 26. · Zbl 0642.03018
[14] Szalas, A., 1987, ?A complete axiomatic characterization of first-order temporal logic of linear time?, Theoretical Computer Science 54, 199-214. · Zbl 0645.03020 · doi:10.1016/0304-3975(87)90129-0
[15] van Benthem, J. F. g200A. K., 1982, The logic of time, Reidel, Dordrecht.
[16] Venema, Y., 1991, ?Completeness via completeness?, In M. de Rijke, editor, Colloquium on Modal Logic, 1991, ITLI-Network Publication, Instit. for Lang., Logic and Information, University of Amsterdam. · Zbl 0821.03011
[17] Xu, M., 1988, ?On some U, S-tense logics?, J. of Philosophical Logic 17, 181-202. · Zbl 0648.03010
[18] Zanardo, A., 1991, ?A complete deductive system for since-until branching time logic?, J. Philosophical Logic. · Zbl 0724.03015
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.