Editing Temporal logic (section)

=== 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.