Editing Temporal logic (section)

== Prior's tense logic (TL) ==
The sentential tense logic introduced in ''Time and Modality'' has four (non-[[Truth function|truth-functional]]) [[modal operator]]s (in addition to all usual truth-functional operators in [[Propositional calculus|first-order propositional logic]]).<ref>{{Cite book|title=Time and modality: the John Locke lectures for 1955–6, delivered at the University of Oxford|last=Prior|first=Arthur Norman|publisher=The Clarendon Press|year=2003|isbn=9780198241584|location=Oxford|oclc=905630146|author-link=Arthur Prior}}</ref>
* ''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:<ref>{{Cite web|url=https://www.cas.mcmaster.ca/~lawford/2F03/Notes/model.pdf|title=An Introduction to Temporal Logics|last=Lawford|first=M.|date=2004|website=Department of Computer Science McMaster University}}</ref>

* <math>\pi \vDash F G \phi</math>: "At a certain point, <math>\phi</math> is true at all future states of the path"
* <math>\pi \vDash G F \phi</math>: "<math>\phi</math> is true at infinitely many states on the path"

From ''P'' and ''F'' one can define ''G'' and ''H'', and vice versa:

:<math>\begin{align}
  F &\equiv \lnot G\lnot \\
  P &\equiv \lnot H\lnot
\end{align}</math>

=== Syntax and semantics ===

A minimal syntax for TL is specified with the following [[Backus–Naur form|BNF grammar]]:

:<math>\phi ::= a \;|\; \bot \;|\; \lnot\phi \;|\; \phi\lor\phi \;|\; G\phi \;|\; H\phi</math>

where ''a'' is some [[atomic formula]].<ref>{{Cite book|url=https://plato.stanford.edu/archives/win2015/entries/logic-temporal/|title=The Stanford Encyclopedia of Philosophy|last1=Goranko|first1=Valentin|last2=Galton|first2=Antony|chapter=Temporal Logic |date=2015|publisher=Metaphysics Research Lab, Stanford University|editor-last=Zalta|editor-first=Edward N.|edition=Winter 2015}}</ref>

[[Kripke model]]s are used to evaluate the truth of [[Sentence (mathematical logic)|sentences]] in TL. A pair ({{Var|T}}, <) of a set {{Var|T}} and a [[binary relation]] < on {{Var|T}} (called "precedence") is called a '''frame'''. A '''model''' is given by triple ({{Var|T}}, <, {{Var|V}}) of a frame and a function {{Var|V}} called a '''valuation''' that assigns to each pair ({{Var|a}}, {{Var|u}}) of an atomic formula and a time value some truth value. The notion "{{Var|ϕ}} is true in a model {{Var|U}}=({{Var|T}}, <, {{Var|V}}) at time {{Var|u}}" is abbreviated {{var|U}}[[Double turnstile|⊨]]{{var|ϕ}}[{{var|u}}]. With this notation,<ref>{{Cite book|title=The continuum companion to philosophical logic|last=Müller|first=Thomas|publisher=A&C Black|year=2011|editor-last=Horsten|editor-first=Leon|pages=329|chapter=Tense or temporal logic|chapter-url=http://kops.uni-konstanz.de/bitstream/handle/123456789/27232/Mueller_272322.pdf?sequence=2}}</ref>

{| class="wikitable"
|+
! Statement 
! ... is true just when
|-
| {{var|U}}⊨{{var|a}}[{{var|u}}]
| {{var|V}}({{var|a}},{{var|u}})=true
|-
| {{var|U}}⊨¬{{var|ϕ}}[{{var|u}}]
| not {{var|U}}⊨{{var|ϕ}}[{{var|u}}]
|-
| {{var|U}}⊨({{var|ϕ}}∧{{var|ψ}})[{{var|u}}]
| {{var|U}}⊨{{var|ϕ}}[{{var|u}}] and {{var|U}}⊨{{var|ψ}}[{{var|u}}]
|-
| {{var|U}}⊨({{var|ϕ}}∨{{var|ψ}})[{{var|u}}]
| {{var|U}}⊨{{var|ϕ}}[{{var|u}}] or {{var|U}}⊨{{var|ψ}}[{{var|u}}]
|-
| {{var|U}}⊨({{var|ϕ}}→{{var|ψ}})[{{var|u}}]
| {{var|U}}⊨{{var|ψ}}[{{var|u}}] if {{var|U}}⊨{{var|ϕ}}[{{var|u}}]
|-
| {{var|U}}⊨G{{var|ϕ}}[{{var|u}}]
| {{var|U}}⊨{{var|ϕ}}[{{var|v}}] for all {{var|v}} with {{var|u}}<{{var|v}}
|-
| {{var|U}}⊨H{{var|ϕ}}[{{var|u}}]
| {{var|U}}⊨{{var|ϕ}}[{{var|v}}] for all {{var|v}} with {{var|v}}<{{var|u}}
|}

Given a class {{var|F}} of frames, a sentence {{var|ϕ}} of TL is
* '''valid''' with respect to {{var|F}} if for every model {{var|U}}=({{var|T}},<,{{var|V}}) with ({{var|T}},<) in {{var|F}} and for every {{var|u}} in {{var|T}}, {{var|U}}⊨{{var|ϕ}}[{{var|u}}]
* '''satisfiable''' with respect to {{var|F}} if there is a model {{var|U}}=({{var|T}},<,{{var|V}}) with ({{var|T}},<) in {{var|F}} such that for some {{var|u}} in {{var|T}}, {{var|U}}⊨{{var|ϕ}}[{{var|u}}]
* a '''consequence''' of a sentence {{var|ψ}} with respect to {{var|F}} if for every model {{var|U}}=({{var|T}},<,{{var|V}}) with ({{var|T}},<) in {{var|F}} and for every {{var|u}} in {{var|T}}, if {{var|U}}⊨{{var|ψ}}[{{var|u}}], then {{var|U}}⊨{{var|ϕ}}[{{var|u}}]

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 reduction|transitive]], [[Antisymmetric relation|antisymmetric]], [[Reflexive relation|reflexive]], [[Trichotomy (mathematics)|trichotomic]], [[irreflexive]], [[Total order|total]], [[Dense order|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:<ref>{{Cite book|title=Philosophical logic|last=Burgess|first=John P.|publisher=Princeton University Press|year=2009|isbn=9781400830497|location=Princeton, New Jersey|page=21|oclc=777375659|author-link=John P. Burgess}}</ref>
# {{var|A}} where {{var|A}} is a [[Tautology (logic)|tautology]] of [[first-order logic]]
# G({{var|A}}→{{var|B}})→(G{{var|A}}→G{{var|B}})
# H({{var|A}}→{{var|B}})→(H{{var|A}}→H{{var|B}})
# {{var|A}}→GP{{var|A}}
# {{var|A}}→HF{{var|A}}
with the following rules of deduction:
# given {{var|A}}→{{var|B}} and {{var|A}}, deduce {{var|B}} ([[modus ponens]])
# given ''a tautology'' {{var|A}}, infer G{{var|A}}
# given ''a tautology'' {{var|A}}, infer H{{var|A}}

One can derive the following rules:
# '''Becker's rule''': given {{var|A}}→{{var|B}}, deduce T{{var|A}}→T{{var|B}} where T is a '''tense''', any sequence made of G, H, F, and P.
# '''Mirroring''': given a theorem {{var|A}}, deduce its '''mirror statement''' {{var|A}}<sup>§</sup>, which is obtained by replacing G by H (and so F by P) and vice versa.
# '''Duality''': given a theorem {{var|A}}, deduce its '''dual statement''' {{var|A}}*, 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]] with one free variable {{Var|x}}<sub>0</sub> (representing the present moment). This translation {{Var|M}} is defined recursively as follows:<ref>{{Cite book|title=Philosophical logic|last=Burgess|first=John P.|publisher=Princeton University Press|year=2009|isbn=9781400830497|location=Princeton, New Jersey|page=17|oclc=777375659|author-link=John P. Burgess}}</ref>

:<math>\begin{align}
  & M(a)              &&= a^*x_0  \\
  & M(\lnot \phi)     &&= \lnot M(\phi) \\
  & M(\phi\land\psi)  &&= M(\phi)\land M(\psi) \\
  & M(\mathsf{G}\phi) &&= \forall x_1 (x_0<x_1\rightarrow M(A^+)) \\ 
  & M(\mathsf{H}\phi) &&= \forall x_1 (x_1<x_0\rightarrow M(A^+))
\end{align}</math>

where <math>A^+</math> is the sentence {{mvar|A}} with all variable indices incremented by 1 and <math>a^*</math> is a one-place predicate defined by <math>x \mapsto V(a, x)</math>.