Algebraic approach to tense operators

Propositional logics, both classical and non-classical, usually do not incorporate the dimension of time. However, even Aristotle already mentioned that time plays an important role in the evaluation of truth values of propositions. His well-known example was the statement „There will be a sea battle tomorrow“. Certainly, tomorrow it will be clear if this proposition is true or false, but today we cannot assign one of these values. Therefore, he accepted that two-valued logic cannot capture the entire human thinking. After Aristotle's time, a lot was created by men and, nowadays, logic is not an exceptional area for human reasoning. From the 1940's on, computers were built and the era of the Artificial Intelligence gently started. Nowadays, practically any more advanced product contains some kind of processor which decides situations in a way similar to that of a human being. However, for such technical devices the forecast for truth values of propositions in the future is not only a speculation. Due to the constructions and the technical possibilities, we can often compute these values, and propositions concerning the near future are of great importance for the control of these systems. This has motivated many authors to investigate the so-called temporal logic, i. e., the logic where time is considered as a variable of the propositional formula. Tense logic was introduced by Arthur Prior in the late 1950's as a result of his interest in the relationship between tense and modality. The logical language of tense logic contains, in addition to the ususal truth-functional operators, four the so-called modal operators. The aim of this monograph is not to present tense logic in full detail. As Aristotle's logic was useful for two millennia in science, but for computer programming only its formalization via Boolean algebras is applied, we will present only an algebraic axiomatization of tense logic and tense operators here. Classical propositional logic was axiomatized by George Boole via Boolean algebras, but this was only a starting point for the formalization of logic. In 1930 intuitionistic logic was formalized by the use of Heyting algebras, in the late 1950's the many-valued Lukasiewicz logic was axiomatized by C. C. Chang by the so-called MV-algebras, many-valued Post logic by Post algebras and in recent decades fuzzy logic, relevance logic, Hájek's basic logic and linear logic by residuated lattices. Hence, we will use algebraic tools for the axiomatization of tense operators. Using the fact that these are modal operators, we will axiomatize also modal operators in this way. Since all of these operators can be considered as quantifiers, we will start with the axiomatization of quantifiers developed by P. Halmos and J. D. Rutledge. Our algebraic methods and tools will be described in full detail, without taking into account whether the reader is or is not a specialist in lattice theory. The authors hope that their monograph will not be the final attempt at the field of modal and tense operators and the development of corresponding algebraic tools and methods but, on the contrary, it will serve as a compendium and, possibly, a motivation for the readers for their future research.