Editing Temporal logic (section)

==History==
Although [[Aristotle]]'s logic is almost entirely concerned with the theory of the [[categorical syllogism]], there are passages in his work that are now seen as anticipations of temporal logic, and may imply an early, partially developed form of [[first-order logic|first-order]] temporal modal [[bivalent logic|bivalent]] logic. Aristotle was particularly concerned with the [[problem of future contingents]], where he could not accept that the [[principle of bivalence]] applies to statements about future events, i.e. that we can presently decide if a statement about a future event is true or false, such as "there will be a sea battle tomorrow".<ref>Vardi 2008, p. 153</ref>

There was little development for millennia, [[Charles Sanders Peirce]] noted in the 19th century:<ref name=v154>Vardi 2008, p. 154</ref>
{{cquote|Time has usually been considered by logicians to be what is called 'extralogical' matter. I have never shared this opinion. But I have thought that logic had not yet reached the state of development at which the introduction of temporal modifications of its forms would not result in great confusion; and I am much of that way of thinking yet.}}

Surprisingly for [[Charles Sanders Peirce|Peirce]], the first system of temporal logic was constructed, as far as we know, in the first half of 20th century. Although [[Arthur Prior]] is widely known as a founder of temporal logic, the first formalization of such logic was provided in 1947 by Polish logician, [[Jerzy Łoś]].<ref name=":0">{{Cite journal|last=Łoś|first=Jerzy |url=http://dlibra.umcs.lublin.pl/dlibra/doccontent?id=4085|title=Podstawy analizy metodologicznej kanonów Milla |journal=Zasoby Biblioteki Głównej Umcs |date=1947|publisher=nakł. Uniwersytetu Marii Curie-Skłodowskiej |language=pl}}</ref> In his work ''Podstawy Analizy Metodologicznej Kanonów Milla'' (''The Foundations of a Methodological Analysis of Mill’s Methods'') he presented a formalization of [[Mill's canons]]. In [[Jerzy Łoś|Łoś]]' approach, emphasis was placed on the time factor. Thus, to reach his goal, he had to create a logic that could provide means for formalization of temporal functions. The logic could be seen as a byproduct of [[Jerzy Łoś|Łoś]]' main aim,<ref name=":1">{{Cite journal|last=Øhrstrøm|first=Peter|date=2019|title=The Significance of the Contributions of A.N.Prior and Jerzy Łoś in the Early History of Modern Temporal Logic|url=https://vbn.aau.dk/en/publications/the-significance-of-the-contributions-of-anprior-and-jerzy-%C5%82o%C5%9B-in|journal=Logic and Philosophy of Time: Further Themes from Prior, Volume 2|series=Logic and Philosophy of Time |isbn=9788772102658 |language=English}}</ref> albeit it was the first positional logic that, as a framework, was used later for [[Jerzy Łoś|Łoś]]' inventions in [[epistemic logic]]. The logic itself has syntax very different than Prior's tense logic, which uses modal operators. The language of [[Jerzy Łoś|Łoś]]' logic rather uses a realization operator, specific to positional logic, which binds the expression with the specific context in which its truth-value is considered. In [[Jerzy Łoś|Łoś]]' work this considered context was only temporal, thus expressions were bound with specific moments or intervals of time.

In the following years, research of temporal logic by [[Arthur Prior]] began.<ref name=":1" /> He was concerned with the philosophical implications of [[free will]] and [[predestination]]. According to his wife, he first considered formalizing temporal logic in 1953. Results of his research were first presented at the conference in [[Wellington]] in 1954.<ref name=":1" /> The system Prior presented, was similar syntactically to [[Jerzy Łoś|Łoś]]' logic, although not until 1955 did he explicitly refer to [[Jerzy Łoś|Łoś]]' work, in the last section of Appendix 1 in Prior’s ''Formal Logic''.<ref name=":1" />

[[Arthur Prior|Prior]] gave lectures on the topic at the [[University of Oxford]] in 1955–6, and in 1957 published a book, ''Time and Modality'', in which he introduced a [[propositional logic|propositional]] modal logic with two temporal connectives ([[modal operator]]s), F and P, corresponding to "sometime in the future" and "sometime in the past". In this early work, Prior considered time to be linear. In 1958 however, he received a letter from [[Saul Kripke]], who pointed out that this assumption is perhaps unwarranted. In a development that foreshadowed a similar one in computer science, Prior took this under advisement, and developed two theories of branching time, which he called "Ockhamist" and "Peircean".<ref name="v154" />{{Clarify|date=April 2011}} Between 1958 and 1965 Prior also corresponded with [[Charles Leonard Hamblin]], and a number of early developments in the field can be traced to this correspondence, for example [[Hamblin implications]]. Prior published his most mature work on the topic, the book ''Past, Present, and Future'' in 1967. He died two years later.<ref>{{cite book|author1=Peter Øhrstrøm|author2=Per F. V. Hasle|title=Temporal logic: from ancient ideas to artificial intelligence|year=1995|publisher=Springer|isbn=978-0-7923-3586-3}} pp.&nbsp;176–178, 210</ref>

Along with '''tense logic,''' [[Arthur Prior|Prior]] constructed a few systems of positional logic, which inherited their main ideas from [[Jerzy Łoś|Łoś]].<ref name=":2">{{Cite journal|last1=Rescher|first1=Nicholas|last2=Garson|first2=James|date=January 1969|title=Topological Logic|url=https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/topological-logic/5ADE3A9CA7CE00FBD8D69E4DDA8B1BC8|journal=The Journal of Symbolic Logic|language=en|volume=33|issue=4|pages=537–548|doi=10.2307/2271360|jstor=2271360 |s2cid=2110963 |issn=0022-4812}}</ref> Work in positional temporal logics was continued by [[Nicholas Rescher]] in the 60s and 70s. In such works as ''Note on Chronological Logic'' (1966), ''On the Logic of Chronological  Propositions'' (1968)'', Topological Logic'' (1968), and ''Temporal Logic'' (1971) he researched connections between [[Jerzy Łoś|Łoś]]' and [[Arthur Prior|Prior]]'s systems. Moreover, he proved that [[Arthur Prior|Prior]]'s tense operators could be defined using a realization operator in specific positional logics.<ref name=":2" /> [[Nicholas Rescher|Rescher]], in his work, also created more general systems of positional logics. Although the first ones were constructed for purely temporal uses, he proposed the term '''topological logics''' for logics that were meant to contain a realization operator but had no specific temporal axioms—like the clock axiom.

The binary temporal operators ''Since'' and ''Until'' were introduced by [[Hans Kamp]] in his 1968 Ph.D. thesis,<ref>{{cite web|url=https://plato.stanford.edu/entries/logic-temporal/#AddSinUnt |title=Temporal Logic (Stanford Encyclopedia of Philosophy) |publisher=Plato.stanford.edu |access-date=2014-07-30}}</ref> which also contains an important result relating temporal logic to [[first-order logic]]—a result now known as [[Kamp's theorem]].<ref name="CarnielliPizzi2008">{{cite book|author1=Walter Carnielli|author2=Claudio Pizzi|title=Modalities and Multimodalities|url=https://books.google.com/books?id=XpAFM04G6BAC&pg=PA181|year=2008|publisher=Springer|isbn=978-1-4020-8589-5|page=181}}</ref><ref name=v154>Vardi 2008, p. 154</ref><ref name="TessarisFranconi2009">{{cite book|author1=Sergio Tessaris|author2=Enrico Franconi|author3=Thomas Eiter|title=Reasoning Web. Semantic Technologies for Information Systems: 5th International Summer School 2009, Brixen-Bressanone, Italy, August 30 – September 4, 2009, Tutorial Lectures|url=https://books.google.com/books?id=JdyeU7zs4-AC&pg=PA112|year=2009|publisher=Springer|isbn=978-3-642-03753-5|page=112}}</ref>

Two early contenders in formal verifications were [[linear temporal logic]], a linear-time logic by [[Amir Pnueli]], and [[computation tree logic]] (CTL), a branching-time logic by [[Mordechai Ben-Ari]], [[Zohar Manna]] and Amir Pnueli. An almost equivalent formalism to CTL was suggested around the same time by [[Edmund M. Clarke|E. M. Clarke]] and [[E. Allen Emerson|E. A. Emerson]]. The fact that the second logic can be [[Decision problem|decided]] [[computational complexity|more efficiently]] than the first does not reflect on branching- and linear-time logics in general, as has sometimes been argued. Rather, Emerson and Lei show that any linear-time logic can be extended to a branching-time logic that can be decided with the same complexity.