Temporal logic has found an important application in formal verification, where it is used to state requirements of hardware or software systems.
[1] There was little development for millennia, Charles Sanders Peirce noted in the 19th century:[2] Time has usually been considered by logicians to be what is called 'extralogical' matter.
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 Peirce, the first system of temporal logic was constructed, as far as we know, in the first half of 20th century.
Thus, to reach his goal, he had to create a logic that could provide means for formalization of temporal functions.
In Łoś' work this considered context was only temporal, thus expressions were bound with specific moments or intervals of time.
Prior published his most mature work on the topic, the book Past, Present, and Future in 1967.
The binary temporal operators Since and Until were introduced by Hans Kamp in his 1968 Ph.D. thesis,[7] which also contains an important result relating temporal logic to first-order logic—a result now known as Kamp's theorem.
Łoś’s logic was published as his 1947 master’s thesis Podstawy Analizy Metodologicznej Kanonów Milla (The Foundations of a Methodological Analysis of Mill’s Methods).
[10] His philosophical and formal concepts could be seen as continuations of those of the Lviv–Warsaw School of Logic, as his supervisor was Jerzy Słupecki, disciple of Jan Łukasiewicz.
The paper was not translated into English until 1977, although Henryk Hiż presented in 1951 a brief, but informative, review in the Journal of Symbolic Logic.
This review contained core concepts of Łoś’s work and was enough to popularize his results among the logical community.
The main aim of this work was to present Mill's canons in the framework of formal logic.
To achieve this goal the author researched the importance of temporal functions in the structure of Mill's concept.
Having that, he provided his axiomatic system of logic that would fit as a framework for Mill's canons along with their temporal aspects.
The language of the logic first published in Podstawy Analizy Metodologicznej Kanonów Milla (The Foundations of a Methodological Analysis of Mill’s Methods) consisted of:[3] The set of terms (denoted by S) is constructed as follows: The set of formulas (denoted by For) is constructed as follows:[10] The sentential tense logic introduced in Time and Modality has four (non-truth-functional) modal operators (in addition to all usual truth-functional operators in first-order propositional logic).
[11] These can be combined if we let π be an infinite path:[12] From P and F one can define G and H, and vice versa: A minimal syntax for TL is specified with the following BNF grammar: where a is some atomic formula.
It is common to restrict the class of frames to those with a relation < that is transitive, antisymmetric, reflexive, trichotomic, irreflexive, total, dense, or some combination of these.
Burgess outlines a logic that makes no assumptions on the relation <, but allows for meaningful deductions, based on the following axiom schema:[15] with the following rules of deduction: One can derive the following rules: Burgess gives a Meredith translation from statements in TL into statements in first-order logic with one free variable x0 (representing the present moment).