In
logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from prem ...
, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of
time
Time is the continued sequence of existence and event (philosophy), events that occurs in an apparently irreversible process, irreversible succession from the past, through the present, into the future. It is a component quantity of various me ...
(for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I eat something"). It is sometimes also used to refer to tense logic, a
modal logic
Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend ot ...
-based system of temporal logic introduced by
Arthur Prior
Arthur Norman Prior (4 December 1914 – 6 October 1969), usually cited as A. N. Prior, was a New Zealand–born logician and philosopher. Prior (1957) founded tense logic, now also known as temporal logic, and made important contributi ...
in the late 1950s, with important contributions by
Hans Kamp. It has been further developed by
computer scientists
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (including ...
, notably
Amir Pnueli
Amir Pnueli ( he, אמיר פנואלי; April 22, 1941 – November 2, 2009) was an Israeli computer scientist and the 1996 Turing Award recipient.
Biography
Pnueli was born in Nahalal, in the British Mandate of Palestine (now in Israel) and re ...
, and
logician
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
s.
Temporal logic has found an important application in
formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal met ...
, where it is used to state requirements of hardware or software systems. For instance, one may wish to say that ''whenever'' a request is made, access to a resource is ''eventually'' granted, but it is ''never'' granted to two requestors simultaneously. Such a statement can conveniently be expressed in a temporal logic.
Motivation
Consider the statement "I am hungry". Though its meaning is constant in time, the statement's truth value can vary in time. Sometimes it is true, and sometimes false, but never simultaneously true ''and'' false. In a temporal logic, a statement can have a truth value that varies in time—in contrast with an atemporal logic, which applies only to statements whose truth values are constant in time. This treatment of truth-value over time differentiates temporal logic from
computational verb logic.
Temporal logic always has the ability to reason about a timeline. So-called "linear-time" logics are restricted to this type of reasoning. Branching-time logics, however, can reason about multiple timelines. This permits in particular treatment of environments that may act unpredictably.
To continue the example, in a branching-time logic we may state that "there is a possibility that I will stay hungry forever", and that "there is a possibility that eventually I am no longer hungry". If we do not know whether or not I will ever be fed, these statements can both be true.
History
Although
Aristotle
Aristotle (; grc-gre, Ἀριστοτέλης ''Aristotélēs'', ; 384–322 BC) was a Greek philosopher and polymath during the Classical period in Ancient Greece. Taught by Plato, he was the founder of the Peripatetic school of ...
's logic is almost entirely concerned with the theory of the
categorical syllogism
A syllogism ( grc-gre, συλλογισμός, ''syllogismos'', 'conclusion, inference') is a kind of logical argument that applies deductive reasoning to arrive at a conclusion based on two propositions that are asserted or assumed to be true ...
, 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
In mathematics and other formal sciences, first-order or first order most often means either:
* "linear" (a polynomial of degree at most one), as in first-order approximation and other calculus uses, where it is contrasted with "polynomials of hig ...
temporal modal
bivalent Bivalent may refer to:
* Bivalent (chemistry), a molecule formed from two or more atoms bound together
*Bivalent (engine), an engine that can operate on two different types of fuel
*Bivalent (genetics), a pair of homologous chromosomes
*Bivalent log ...
logic. Aristotle was particularly concerned with the
problem of future contingents
Future contingent propositions (or simply, future contingents) are statements about states of affairs in the future that are '' contingent:'' neither necessarily true nor necessarily false.
The problem of future contingents seems to have been fi ...
, where he could not accept that the
principle of bivalence
In logic, the semantic principle (or law) of bivalence states that every declarative sentence expressing a proposition (of a theory under inspection) has exactly one truth value, either true or false. A logic satisfying this principle is called ...
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".
There was little development for millennia,
Charles Sanders Peirce
Charles Sanders Peirce ( ; September 10, 1839 – April 19, 1914) was an American philosopher, logician, mathematician and scientist who is sometimes known as "the father of pragmatism".
Educated as a chemist and employed as a scientist for ...
noted in the 19th century:
[Vardi 2008, p. 154]
Surprisingly for
Peirce, the first system of temporal logic was constructed, as far as we know, in the first half of 20th century. Although
Arthur Prior
Arthur Norman Prior (4 December 1914 – 6 October 1969), usually cited as A. N. Prior, was a New Zealand–born logician and philosopher. Prior (1957) founded tense logic, now also known as temporal logic, and made important contributi ...
is widely known as a founder of temporal logic, the first formalization of such logic was provided in 1947 by Polish logician,
Jerzy Łoś.
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
Ł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
Łoś' main aim,
albeit it was the first positional logic that, as a framework, was used later for
Łoś' inventions in
epistemic logic. The logic itself has syntax very different than Prior's tense logic, which uses modal operators. The language of
Ł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
Łoś' work this considered context was only temporal, thus expressions were binded with specific moments or intervals of time.
In the following years, research of temporal logic by
Arthur Prior
Arthur Norman Prior (4 December 1914 – 6 October 1969), usually cited as A. N. Prior, was a New Zealand–born logician and philosopher. Prior (1957) founded tense logic, now also known as temporal logic, and made important contributi ...
began.
He was concerned with the philosophical implications of
free will
Free will is the capacity of agents to choose between different possible courses of action unimpeded.
Free will is closely linked to the concepts of moral responsibility, praise, culpability, sin, and other judgements which apply only to ac ...
and
predestination
Predestination, in theology, is the doctrine that all events have been willed by God, usually with reference to the eventual fate of the individual soul. Explanations of predestination often seek to address the paradox of free will, whereby ...
. According to his wife, he first considered formalizing temporal logic in 1953. Results of his research were firstly presented at the conference in
Wellington
Wellington ( mi, Te Whanganui-a-Tara or ) is the capital city of New Zealand. It is located at the south-western tip of the North Island, between Cook Strait and the Remutaka Range. Wellington is the second-largest city in New Zealand by ...
in 1954.
The system Prior presented, was similar syntactically to
Łoś' logic, although not until 1955 did he explicitly refer to
Łoś' work, in the last section of Appendix 1 in Prior’s ''Formal Logic''.
Prior
Prior (or prioress) is an ecclesiastical title for a superior in some religious orders. The word is derived from the Latin for "earlier" or "first". Its earlier generic usage referred to any monastic superior. In abbeys, a prior would be low ...
gave lectures on the topic at the
University of Oxford
, mottoeng = The Lord is my light
, established =
, endowment = £6.1 billion (including colleges) (2019)
, budget = £2.145 billion (2019–20)
, chancellor ...
in 1955–6, and in 1957 published a book, ''Time and Modality'', in which he introduced a
propositional modal logic with two temporal connectives (
modal operators), 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
Saul Aaron Kripke (; November 13, 1940 – September 15, 2022) was an American philosopher and logician in the analytic tradition. He was a Distinguished Professor of Philosophy at the Graduate Center of the City University of New York and e ...
, 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".
Between 1958 and 1965 Prior also corresponded with
Charles Leonard Hamblin
Charles Leonard Hamblin (20 November 1922 – 14 May 1985) was an Australian philosopher, logician, and computer pioneer, as well as a professor of philosophy at the New South Wales University of Technology (now the University of New South Wales) ...
, and a number of early developments in the field can be traced to this correspondence, for example
Hamblin implications Hamblin may refer to: People
* Hamblin (surname)
* Thomas Sowerby Hamblin, British actor and theatre manager
* Henry Thomas Hamblin, British author
* Robert W. Hamblin, professor and author
* Hamblin González, Nicaraguan cyclist
Places
* Hambl ...
. Prior published his most mature work on the topic, the book ''Past, Present, and Future'' in 1967. He died two years later.
Along with tense logic,
Prior
Prior (or prioress) is an ecclesiastical title for a superior in some religious orders. The word is derived from the Latin for "earlier" or "first". Its earlier generic usage referred to any monastic superior. In abbeys, a prior would be low ...
constructed a few systems of positional logic, which inherited their main ideas from
Łoś.
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
Łoś' and
Prior
Prior (or prioress) is an ecclesiastical title for a superior in some religious orders. The word is derived from the Latin for "earlier" or "first". Its earlier generic usage referred to any monastic superior. In abbeys, a prior would be low ...
's systems. Moreover he proved that
Prior
Prior (or prioress) is an ecclesiastical title for a superior in some religious orders. The word is derived from the Latin for "earlier" or "first". Its earlier generic usage referred to any monastic superior. In abbeys, a prior would be low ...
's tense operators could be defined using a realization operator in specific positional logics.
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, which also contains an important result relating temporal logic to
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
—a result now known as
Kamp's theorem.
[Vardi 2008, p. 154]
Two early contenders in formal verifications were
linear temporal logic In logic, linear temporal logic or linear-time temporal logic (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths, e.g., a condition will eventually be true, a condition wil ...
, a linear-time logic by
Amir Pnueli
Amir Pnueli ( he, אמיר פנואלי; April 22, 1941 – November 2, 2009) was an Israeli computer scientist and the 1996 Turing Award recipient.
Biography
Pnueli was born in Nahalal, in the British Mandate of Palestine (now in Israel) and re ...
, and
computation tree logic
Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realiz ...
(CLT), a branching-time logic by
Mordechai Ben-Ari,
Zohar Manna
Zohar Manna (1939 – 30 August 2018) was an Israeli-American computer scientist who was a professor of computer science at Stanford University.
Biography
He was born in Haifa, Israel. He earned his Bachelor of Science (BS) and Master of Scienc ...
and Amir Pnueli. An almost equivalent formalism to CTL was suggested around the same time by
E. M. Clarke and
E. A. Emerson. The fact that the second logic can be
decided 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.
Łoś' positional logic
Łoś’ 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'').
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
Jerzy Słupecki (1904–1987) was a Polish mathematician and logician.
Life
He attended the seminar of, and wrote a 1938 doctorate under, Jan Łukasiewicz.
During WWII he was active in Żegota.
In 1963, when at Wroclaw University, where he had ...
, disciple of
Jan Łukasiewicz
Jan Łukasiewicz (; 21 December 1878 – 13 February 1956) was a Polish logician and philosopher who is best known for Polish notation and Łukasiewicz logic His work centred on philosophical logic, mathematical logic and history of logic. ...
. The paper was not translated into English until 1977, although
Henryk Hiż
Henryk Hiż (8 October 1917 – 19 December 2006) was a Polish analytical philosopher specializing in linguistics, philosophy of language, logic, mathematics and ethics, active for most of his life in the United States, one of the youngest repre ...
presented in 1951 a brief, but informative, review in the ''
Journal of Symbolic Logic
The '' Journal of Symbolic Logic'' is a peer-reviewed mathematics journal published quarterly by Association for Symbolic Logic. It was established in 1936 and covers mathematical logic. The journal is indexed by ''Mathematical Reviews'', Zentralb ...
''. This review contained core concepts of
Łoś’ 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.
Syntax
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:
* first-order logic operators ‘¬’, ‘∧’, ‘∨’, ‘→’, ‘≡’, ‘∀’ and ‘∃’
* realization operator U
* functional symbol δ
* propositional variables p
1,p
2,p
3,...
* variables denoting time moments t
1,t
2,t
3,...
* variables denoting time intervals n
1,n
2,n
3,...
The set of terms (denoted by S) is constructed as follows:
* variables denoting time moments or intervals are terms
* if
and
is a time interval variable, then
The set of formulas (denoted by For) is constructed as follows:
* all first-order logic formulas are valid
* if
and
is a propositional variable, then
* if
, then
* if
and
, then
* if
and
and υ is a propositional, moment or interval variable, then
Original Axiomatic System
#
#
#
#
#
#
#
#
#
Prior's tense logic (TL)
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.
* ''P'': "It was the case that..." (P stands for "past")
* ''F'': "It will be the case that..." (F stands for "future")
* ''G'': "It always will be the case that..."
* ''H'': "It always was the case that..."
These can be combined if we let ''π'' be an infinite path:
*
: "At a certain point,
is true at all future states of the path"
*
: "
is true at infinitely many states on the path"
From ''P'' and ''F'' one can define ''G'' and ''H'', and vice versa:
Syntax and semantics
A minimal syntax for TL is specified with the following
BNF grammar:
where ''a'' is some
atomic formula
In mathematical logic, an atomic formula (also known as an atom or a prime formula) is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformu ...
.
Kripke models are used to evaluate the truth of
sentences
''The Four Books of Sentences'' (''Libri Quattuor Sententiarum'') is a book of theology written by Peter Lombard in the 12th century. It is a systematic compilation of theology, written around 1150; it derives its name from the '' sententiae'' ...
in TL. A pair (, <) of a set and a
binary relation
In mathematics, a binary relation associates elements of one set, called the ''domain'', with elements of another set, called the ''codomain''. A binary relation over sets and is a new set of ordered pairs consisting of elements in and in ...
< on (called "precedence") is called a frame. A model is given by triple (, <, ) of a frame and a function called a valuation that assigns to each pair (, ) of an atomic formula and a time value some truth value. The notion " is true in a model =(, <, ) at time " is abbreviated
⊨[]. With this notation,
Given a class of frames, a sentence of TL is
* valid with respect to if for every model =(,<,) with (,<) in and for every in , ⊨[]
* satisfiable with respect to if there is a model =(,<,) with (,<) in such that for some in , ⊨[]
* a consequence of a sentence with respect to if for every model =(,<,) with (,<) in and for every in , if ⊨[], then ⊨[]
Many sentences are only valid for a limited class of frames. It is common to restrict the class of frames to those with a relation < that is
transitive,
antisymmetric,
reflexive,
trichotomic,
irreflexive
In mathematics, a binary relation ''R'' on a set ''X'' is reflexive if it relates every element of ''X'' to itself.
An example of a reflexive relation is the relation " is equal to" on the set of real numbers, since every real number is equal ...
,
total,
dense, or some combination of these.
A minimal axiomatic logic
Burgess outlines a logic that makes no assumptions on the relation <, but allows for meaningful deductions, based on the following axiom schema:
# where is a
tautology of
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
# G(→)→(G→G)
# H(→)→(H→H)
# →GP
# →HF
with the following rules of deduction:
# given → and , deduce (
modus ponens
In propositional logic, ''modus ponens'' (; MP), also known as ''modus ponendo ponens'' (Latin for "method of putting by placing") or implication elimination or affirming the antecedent, is a deductive argument form and rule of inference ...
)
# given ''a tautology'' , infer G
# given ''a tautology'' , infer H
One can derive the following rules:
# Becker's rule: given →, deduce T→T where T is a tense, any sequence made of G, H, F, and P.
# Mirroring: given a theorem , deduce its mirror statement
§, which is obtained by replacing G by H (and so F by P) and vice versa.
# Duality: given a theorem , deduce its dual statement *, which is obtained by interchanging ∧ with ∨, G with F, and H with P.
Translation to predicate logic
Burgess gives a ''Meredith translation'' from statements in TL into statements in
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
with one free variable
0 (representing the present moment). This translation is defined recursively as follows: