Applied Modal Logic

Temporal Logics

Equation form expr-003001ebf5867324

≺\prec

Read as: the precedes relation

Means: the precedes relation

6 occurrences in this chapter

Equation form expr-01208e159d2aec8c

∧\land

Read as: the conjunction connective

Means: the conjunction connective

1 occurrence in this chapter

Equation form expr-043a718774c572bd

ss

Read as: time point s

Means: time point s

2 occurrences in this chapter

Equation form expr-08b7bc944b8687b4

row label KGG(p→q)→(Gp→Gq)row label KHH(p→q)→(Hp→Hq)\tag{$K_{\Gtemp}$} \Gtemp (p \to q) & \to (\Gtemp p \to \Gtemp q)\\ \tag{$K_{\Htemp}$} \Htemp (p \to q) & \to (\Htemp p \to \Htemp q)

Read as: Two distribution schemas. K sub future always: if it will always be the case that p implies q, then if it will always be the case that p, it will always be the case that q. K sub past always: if it has always been the case that p implies q, then if it has always been the case that p, it has always been the case that q.

Means: Two distribution schemas. K sub future always: if it will always be the case that p implies q, then if it will always be the case that p, it will always be the case that q. K sub past always: if it has always been the case that p implies q, then if it has always been the case that p, it has always been the case that q.

1 occurrence in this chapter

Equation form expr-0bd4de2452d07287

(FPp∨PFp)→(Pp∨p∨Fp)(\Ftemp \Ptemp p \lor \Ptemp \Ftemp p) \lif (\Ptemp p \lor p \lor \Ftemp p)

Read as: if either it will sometime be the case that p was once the case, or it was once the case that p will sometime be the case, then either p was once the case, p is now the case, or p will sometime be the case

Means: if either it will sometime be the case that p was once the case, or it was once the case that p will sometime be the case, then either p was once the case, p is now the case, or p will sometime be the case

1 occurrence in this chapter

Equation form expr-148de9c5a7a44d19

pp

Read as: p

Means: p

7 occurrences in this chapter

Equation form expr-1a53000974926187

V(p)V(p)

Read as: valuation V of p

Means: valuation V of p

2 occurrences in this chapter

Equation form expr-1b293fe03d6e8856

Gp→Fp\Gtemp p \to \Ftemp p

Read as: if p will always be the case, then p will sometime be the case

Means: if p will always be the case, then p will sometime be the case

1 occurrence in this chapter

Equation form expr-1bb5f600fce6bc76

M⊩C[s]\mSat{M}{!C}[s]

Read as: model M satisfies formula C at time point s

Means: model M satisfies formula C at time point s

2 occurrences in this chapter

Equation form expr-22fcce974c4bdb33

M\mModel M

Read as: model M

Means: model M

4 occurrences in this chapter

Equation form expr-234ef32b30394a54

(A∨B)(!A \lor !B)

Read as: open scope, formula A or formula B, close scope

Means: open scope, formula A or formula B, close scope

1 occurrence in this chapter

Equation form expr-23fac266c08cc34b

pi\Obj p_i

Read as: propositional variable p subscript i

Means: propositional variable p subscript i

1 occurrence in this chapter

Equation form expr-284c47be48fb0c66

¬\lnot

Read as: the negation connective

Means: the negation connective

1 occurrence in this chapter

Equation form expr-2b77b28dbb5c188e

M⊩A[t]\mSat{M}{\indfrm}[t]

Read as: model M satisfies the formula in the current induction case at time point t

Means: model M satisfies the formula in the current induction case at time point t

10 occurrences in this chapter

Equation form expr-318f93b8c3835cd2

p1\Obj p_1

Read as: propositional variable p subscript one

Means: propositional variable p subscript one

1 occurrence in this chapter

Equation form expr-376d5037f2a5b8b0

p0\Obj p_0

Read as: propositional variable p subscript zero

Means: propositional variable p subscript zero

1 occurrence in this chapter

Equation form expr-3a09c19172018cbf

M⊩A[t]\mSat{M}{!A}[t]

Read as: model M satisfies formula A at time point t

Means: model M satisfies formula A at time point t

1 occurrence in this chapter

Equation form expr-402ae8731cd7c606

¬P¬A\lnot \Ptemp \lnot !A

Read as: there is no past time at which formula A is false

Means: there is no past time at which formula A is false

1 occurrence in this chapter

Equation form expr-4b5ff8fdbd09818b

M=⟨T,C,V⟩\mModel{M} = \tuple{T, C, V}

Read as: model M equals the ordered triple time domain T, then set C of possible histories, then valuation V

Means: model M equals the ordered triple time domain T, then set C of possible histories, then valuation V

1 occurrence in this chapter

Equation form expr-4e1647611e482b65

∀w¬(w≺w)\forall w \lnot (w \prec w)

Read as: for every w, w does not precede itself

Means: for every w, w does not precede itself

1 occurrence in this chapter

Equation form expr-5136fc4246e7d497

◇\Diamond

Read as: the ordinary possibility operator

Means: the ordinary possibility operator

2 occurrences in this chapter

Equation form expr-529ad2daacd7efcb

∨\lor

Read as: the disjunction connective

Means: the disjunction connective

1 occurrence in this chapter

Equation form expr-549ae8b0f114acc4

s2s_2

Read as: state s subscript two

Means: state s subscript two

3 occurrences in this chapter

Equation form expr-5bbc9d8cec1b5277

(UAB)(\Until !A !B)

Read as: open scope, until formula A will be the case, formula B will be the case, close scope

Means: open scope, until formula A will be the case, formula B will be the case, close scope

1 occurrence in this chapter

Equation form expr-5d00e1f7246d053f

si∈Ts_i \in T

Read as: state s subscript i belongs to time domain T

Means: state s subscript i belongs to time domain T

1 occurrence in this chapter

Equation form expr-5f0c3f95a653895f

t≺σt′t \prec_\sigma t'

Read as: time point t precedes time point t prime along history sigma

Means: time point t precedes time point t prime along history sigma

1 occurrence in this chapter

Equation form expr-6177007880d5a390

M⊩A[t,σ]\mSat{M}{\indfrm}[t, \sigma]

Read as: model M satisfies the formula in the current induction case at time point t and history sigma

Means: model M satisfies the formula in the current induction case at time point t and history sigma

2 occurrences in this chapter

Equation form expr-63d08ce0bacb83e5

FAF !A

Read as: the source's plain letter F followed by formula A

Means: the source's plain letter F followed by formula A

1 occurrence in this chapter

Equation form expr-656750bdeb902237

M⊩B[t′]\mSat{M}{!B}[t']

Read as: model M satisfies formula B at time point t prime

Means: model M satisfies formula B at time point t prime

6 occurrences in this chapter

Equation form expr-67396db9be90a326

U\Until

Read as: the until operator

Means: the until operator

2 occurrences in this chapter

Equation form expr-67d772866363ff3d

¬Fp∧◇Fp\lnot \Ftemp p \land \Diamond \Ftemp p

Read as: it is not the case that p will occur, and it is modally possible that p will occur

Means: it is not the case that p will occur, and it is modally possible that p will occur

1 occurrence in this chapter

Equation form expr-6b23c0d5f35d1b11

CC

Read as: set C of possible histories

Means: set C of possible histories

4 occurrences in this chapter

Equation form expr-6bdbe7ccb718e690

M=⟨T,≺,V⟩\mModel{M} = \tuple{T, \prec, V}

Read as: model M equals the ordered triple time domain T, then the precedes relation, then valuation V

Means: model M equals the ordered triple time domain T, then the precedes relation, then valuation V

1 occurrence in this chapter

Equation form expr-6ee3e646e1871b17

t′∈Tt' \in T

Read as: time point t prime belongs to time domain T

Means: time point t prime belongs to time domain T

7 occurrences in this chapter

Equation form expr-71b2181319b4569d

M⊩B[t′,σ]\mSat{M}{!B}[t', \sigma]

Read as: model M satisfies formula B at time point t prime and history sigma

Means: model M satisfies formula B at time point t prime and history sigma

1 occurrence in this chapter

Equation form expr-72050b0fea075850

PA\Ptemp !A

Read as: it was once the case that formula A

Means: it was once the case that formula A

1 occurrence in this chapter

Equation form expr-74df7b3a28f0d9fd

∀w∃v(v≺w)\forall w \exists v( v \prec w)

Read as: for every w there is a v that precedes w

Means: for every w there is a v that precedes w

1 occurrence in this chapter

Equation form expr-76b21a861143811d

si≺σsjs_i \prec_\sigma s_j

Read as: state s subscript i precedes state s subscript j along history sigma

Means: state s subscript i precedes state s subscript j along history sigma

1 occurrence in this chapter

Equation form expr-76b50eec37b7561e

Fp→FFp\Ftemp p \lif \Ftemp \Ftemp p

Read as: if p will sometime be the case, then it will sometime be the case that p will sometime be the case

Means: if p will sometime be the case, then it will sometime be the case that p will sometime be the case

1 occurrence in this chapter

Equation form expr-76de1512af277cbb

∀w∃v(w≺v)\forall w \exists v( w \prec v)

Read as: for every w there is a v such that w precedes v

Means: for every w there is a v such that w precedes v

1 occurrence in this chapter

Equation form expr-77970456be0eda56

t′t'

Read as: time point t prime

Means: time point t prime

1 occurrence in this chapter

Equation form expr-77ceec1a9c3f6d4a

s1s_1

Read as: state s subscript one

Means: state s subscript one

2 occurrences in this chapter

Equation form expr-7b8539d67beca0e3

s3s_3

Read as: state s subscript three

Means: state s subscript three

4 occurrences in this chapter

Equation form expr-7ef16dcbcb7f2372

M⊩A[t,σ]\mSat{M}{!A}[t, \sigma]

Read as: model M satisfies formula A at time point t and history sigma

Means: model M satisfies formula A at time point t and history sigma

1 occurrence in this chapter

Equation form expr-802ccb8a4a96feeb

t′≺s≺tt' \prec s \prec t

Read as: time point t prime precedes time point s precedes time point t

Means: time point t prime precedes time point s precedes time point t

1 occurrence in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: formula A

Means: formula A

10 occurrences in this chapter

Equation form expr-838a45d2d6d951ad

t′≺tt' \prec t

Read as: time point t prime precedes time point t

Means: time point t prime precedes time point t

3 occurrences in this chapter

Equation form expr-868b5ab9d57772a2

G\Gtemp

Read as: the future always operator G

Means: the future always operator G

3 occurrences in this chapter

Equation form expr-86be9a55762d316a

KK

Read as: axiom K

Means: axiom K

1 occurrence in this chapter

Equation form expr-86ceeed3000b96d6

sjs_j

Read as: state s subscript j

Means: state s subscript j

1 occurrence in this chapter

Equation form expr-8dbeff85f5af96b3

KGK_{\Gtemp}

Read as: axiom K sub future always

Means: axiom K sub future always

1 occurrence in this chapter

Equation form expr-8f5b7695b7dadd37

M⊩C[t]\mSat{M}{!C}[t]

Read as: model M satisfies formula C at time point t

Means: model M satisfies formula C at time point t

3 occurrences in this chapter

Equation form expr-966239b532b39e88

FFp→Fp\Ftemp \Ftemp p \lif \Ftemp p

Read as: if it will sometime be the case that p will sometime be the case, then p will sometime be the case

Means: if it will sometime be the case that p will sometime be the case, then p will sometime be the case

1 occurrence in this chapter

Equation form expr-992accb9917efeb5

C!C

Read as: formula C

Means: formula C

2 occurrences in this chapter

Equation form expr-9a1e4749a64f5c15

∀w∀v(w≺v∨w=v∨v≺w)\forall w \forall v (w \prec v \lor w = v \lor v \prec w)

Read as: for every w and v, either w precedes v, w equals v, or v precedes w

Means: for every w and v, either w precedes v, w equals v, or v precedes w

1 occurrence in this chapter

Equation form expr-9aa41499d9b0708d

t≺s≺t′t \prec s \prec t'

Read as: time point t precedes time point s precedes time point t prime

Means: time point t precedes time point s precedes time point t prime

1 occurrence in this chapter

Equation form expr-9ac5819d902073c6

KHK_{\Htemp}

Read as: axiom K sub past always

Means: axiom K sub past always

1 occurrence in this chapter

Equation form expr-9c3245dfb4ac54c1

σ\sigma

Read as: history sigma

Means: history sigma

4 occurrences in this chapter

Equation form expr-a4a51fbde8d39ce5

p2\Obj p_2

Read as: propositional variable p subscript two

Means: propositional variable p subscript two

1 occurrence in this chapter

Equation form expr-a742a700939c9424

H\Htemp

Read as: the past always operator H

Means: the past always operator H

2 occurrences in this chapter

Equation form expr-adb933e78ac0f3d1

M⊩p[t]\mSat{M}{p}[t]

Read as: model M satisfies p at time point t

Means: model M satisfies p at time point t

1 occurrence in this chapter

Equation form expr-b00a112c61cf02b6

HA\Htemp !A

Read as: it has always been the case that formula A

Means: it has always been the case that formula A

2 occurrences in this chapter

Equation form expr-b087bcd67df8f387

(SAB)(\Since !A !B)

Read as: open scope, since formula A was the case, formula B has been the case, close scope

Means: open scope, since formula A was the case, formula B has been the case, close scope

1 occurrence in this chapter

Equation form expr-b2bc2d231da5028c

M⊩⊥[t]\mSat{M}{\lfalse}[t]

Read as: model M satisfies falsity at time point t

Means: model M satisfies falsity at time point t

1 occurrence in this chapter

Equation form expr-b3c2d5fbc6f3663c

i<ji < j

Read as: i is less than j

Means: i is less than j

1 occurrence in this chapter

Equation form expr-bf4891680d1a9488

M⊮B[t]\mSat/{M}{!B}[t]

Read as: model M does not satisfy formula B at time point t

Means: model M does not satisfy formula B at time point t

2 occurrences in this chapter

Equation form expr-c2866c1fa4f5d144

∀w∀v(w≺v→∃u(w≺u∧u≺v))\forall w \forall v (w \prec v \to \exists u(w \prec u \land u \prec v))

Read as: for every w and v, if w precedes v, then there is a u such that w precedes u and u precedes v

Means: for every w and v, if w precedes v, then there is a u such that w precedes u and u precedes v

1 occurrence in this chapter

Equation form expr-c4c734e08584f69b

F\Ftemp

Read as: the future sometime operator F

Means: the future sometime operator F

4 occurrences in this chapter

Equation form expr-c63f9557f464c93a

¬A\lnot !A

Read as: not formula A

Means: not formula A

1 occurrence in this chapter

Equation form expr-c8ea458b12d6729a

sis_i

Read as: state s subscript i

Means: state s subscript i

1 occurrence in this chapter

Equation form expr-cdc2ed7d3b3d72c2

⊥\lfalse

Read as: falsity

Means: falsity

2 occurrences in this chapter

Equation form expr-cf26fe5bd7e6ea18

(A→B)(!A \lif !B)

Read as: open scope, formula A implies formula B, close scope

Means: open scope, formula A implies formula B, close scope

1 occurrence in this chapter

Equation form expr-d04ff80d9f6dc462

→\lif

Read as: the conditional connective

Means: the conditional connective

1 occurrence in this chapter

Equation form expr-d055ee4dbcdd0c8b

B!B

Read as: formula B

Means: formula B

6 occurrences in this chapter

Equation form expr-d0a2b90b3d18abd7

M\mModel{M}

Read as: model M

Means: model M

2 occurrences in this chapter

Equation form expr-d449db5a0a7ea9cb

P\Ptemp

Read as: the past sometime operator P

Means: the past sometime operator P

2 occurrences in this chapter

Equation form expr-de5a6f78116eca62

VV

Read as: valuation V

Means: valuation V

2 occurrences in this chapter

Equation form expr-e2c00aa28b367a62

σ′∈C\sigma' \in C

Read as: history sigma prime belongs to set C of possible histories

Means: history sigma prime belongs to set C of possible histories

1 occurrence in this chapter

Equation form expr-e3b98a4da31a127d

tt

Read as: time point t

Means: time point t

9 occurrences in this chapter

Equation form expr-e46160bd990de6d4

Hp→Pp\Htemp p \to \Ptemp p

Read as: if p has always been the case, then p was once the case

Means: if p has always been the case, then p was once the case

1 occurrence in this chapter

Equation form expr-e5abf72ebfa1a5c3

t≺t′t \prec t'

Read as: time point t precedes time point t prime

Means: time point t precedes time point t prime

4 occurrences in this chapter

Equation form expr-e632b7095b0bf32c

TT

Read as: time domain T

Means: time domain T

3 occurrences in this chapter

Equation form expr-e83e779d26d3b862

M⊩B[t,σ′]\mSat{M}{!B}[t, \sigma']

Read as: model M satisfies formula B at time point t and history sigma prime

Means: model M satisfies formula B at time point t and history sigma prime

1 occurrence in this chapter

Equation form expr-e8a30216faa64788

GA\Gtemp !A

Read as: it will always be the case that formula A

Means: it will always be the case that formula A

1 occurrence in this chapter

Equation form expr-f0a324946a8d33cd

t,σt, \sigma

Read as: time point t and history sigma

Means: time point t and history sigma

1 occurrence in this chapter

Equation form expr-f0ba94d80b651243

∀u∀v∀w((u≺v∧v≺w)→u≺w)\forall u \forall v \forall w ((u \prec v \land v \prec w) \lif u \prec w)

Read as: for every u, v, and w, if u precedes v and v precedes w, then u precedes w

Means: for every u, v, and w, if u precedes v and v precedes w, then u precedes w

1 occurrence in this chapter

Equation form expr-f157f71e0163a897

□\Box

Read as: the ordinary necessity operator

Means: the ordinary necessity operator

1 occurrence in this chapter

Equation form expr-f2867b48a643a819

t∈V(p)t \in V(p)

Read as: time point t belongs to valuation V of p

Means: time point t belongs to valuation V of p

3 occurrences in this chapter

Equation form expr-f584a5a51624537a

SBC\Since !B !C

Read as: since formula B was the case, formula C has been the case

Means: since formula B was the case, formula C has been the case

1 occurrence in this chapter

Equation form expr-f8c344f726d7064e

UBC\Until !B !C

Read as: until formula B will be the case, formula C will be the case

Means: until formula B will be the case, formula C will be the case

1 occurrence in this chapter

Equation form expr-fa8293778a68ee61

S\Since

Read as: the since operator

Means: the since operator

2 occurrences in this chapter

Equation form expr-fb6e90bc3a43f390

M⊩B[t]\mSat{M}{!B}[t]

Read as: model M satisfies formula B at time point t

Means: model M satisfies formula B at time point t

2 occurrences in this chapter

Equation form expr-ff9ba27416d63e9a

(A∧B)(!A \land !B)

Read as: open scope, formula A and formula B, close scope

Means: open scope, formula A and formula B, close scope

1 occurrence in this chapter

Definition of the basic temporal language

The source lists falsity, the selected propositional variables and connectives, the past operators P and H, and the future operators F and G.

Source

Inductive definition of temporal formulas

Atomic formulas and the selected truth-functional clauses are followed by the four temporal cases. The source's fourth case visibly uses a plain letter F rather than the future-operator macro; that notation is preserved and disclosed.

Source

Definition of a temporal model

A temporal model is an ordered triple consisting of a nonempty set T of time points, a binary precedes relation on T, and a valuation assigning each propositional variable the time points where it is true.

Source

Definition of truth in a temporal model

The source gives the selected propositional truth clauses, then truth conditions for past sometime, past always, future sometime, and future always. Every temporal clause preserves the direction of the strict precedes relation.

Source

Distribution schemas for future-always and past-always

Two displayed schemas state that each always operator distributes over implication: first future always, then past always.

Source

Temporal frame correspondence table

The outer table carries the caption and label for five frame conditions and their temporal formulas. Its inner tabular object supplies the unique ordered structural reading.

Source

Five temporal frame correspondence rows

Columns give a property of the precedes relation and a temporal formula true in the model. Rows are transitive, linear, dense, unbounded toward the past, and unbounded toward the future.

Source

Truth conditions for since and until

Since B C holds when B held at an earlier point and C holds strictly between that point and the present. Until B C holds when B holds at a later point and C holds strictly between the present and that point.

Source

Definition of a possible-histories model

A possible-histories model contains a state set T, a suffix-closed set C of state sequences, and a valuation V. The definition also introduces precedence along a history by comparing sequence indices.

Source

Truth relative to a possible history

Future sometime is evaluated later along the current history. Ordinary possibility is evaluated at the same state in some history in C that contains that state.

Source

Cross-reference reference-001126

the table of temporal frame correspondence properties

Source occurrence

Cross-reference reference-001127

the definition of truth at a point in a temporal model

Source occurrence

Source disclosures

Source-generated case expression tr057-source-macro-0001

A≡⊥!A \ident \lfalse

Read as: Case: A is falsity.

Read in context source

Source-generated case expression tr057-source-macro-0002

A≡¬B!A \ident \lnot !B

Read as: Case: A is the negation of B.

Read in context source

Source-generated case expression tr057-source-macro-0003

A≡(B∧C)!A \ident (!B \land !C)

Read as: Case: A is the conjunction of B and C.

Read in context source

Source-generated case expression tr057-source-macro-0004

A≡(B∨C)!A \ident (!B \lor !C)

Read as: Case: A is the disjunction of B and C.

Read in context source

Source-generated case expression tr057-source-macro-0005

A≡(B→C)!A \ident (!B \lif !C)

Read as: Case: A is the conditional from B to C.

Read in context source

Source-generated case expression tr057-source-macro-0006

A≡PB!A \ident \Ptemp !B

Read as: Case: A says that B was once the case.

Read in context source

Source-generated case expression tr057-source-macro-0007

A≡HB!A \ident \Htemp !B

Read as: Case: A says that B has always been the case.

Read in context source

Source-generated case expression tr057-source-macro-0008

A≡FB!A \ident \Ftemp !B

Read as: Case: A says that B will sometime be the case.

Read in context source

Source-generated case expression tr057-source-macro-0009

A≡GB!A \ident \Gtemp !B

Read as: Case: A says that B will always be the case.

Read in context source

Source-generated case expression tr057-source-macro-0010

A≡SBC!A \ident \Since !B !C

Read as: Case: A says that since B was the case, C has been the case.

Read in context source

Source-generated case expression tr057-source-macro-0011

A≡UBC!A \ident \Until !B !C

Read as: Case: A says that until B will be the case, C will be the case.

Read in context source

Source-generated case expression tr057-source-macro-0012

A≡FB!A \ident \Ftemp !B

Read as: Case: A says that B will sometime be the case.

Read in context source

Source-generated case expression tr057-source-macro-0013

A≡◇B!A \ident \Diamond !B

Read as: Case: A says that B is possible along an alternative history.

Read in context source

Ordered structures

Five temporal frame correspondence rows

Structure: table.

Temporal frame correspondence table. Column headers: if the precedes relation has the stated property; then the displayed formula is true in model M. Row one, transitive: for every u, v, and w, if u precedes v and v precedes w, then u precedes w; corresponding formula if it will sometime be the case that p will sometime be the case, then p will sometime be the case. Row two, linear: for every w and v, either w precedes v, w equals v, or v precedes w; corresponding formula if either it will sometime be the case that p was once the case, or it was once the case that p will sometime be the case, then either p was once the case, p is now the case, or p will sometime be the case. Row three, dense: for every w and v, if w precedes v, then there is a u such that w precedes u and u precedes v; corresponding formula if p will sometime be the case, then it will sometime be the case that p will sometime be the case. Row four, unbounded toward the past: for every w there is a v that precedes w; corresponding formula if p has always been the case, then p was once the case. Row five, unbounded toward the future: for every w there is a v such that w precedes v; corresponding formula if p will always be the case, then p will sometime be the case. End table.

Read the source-bound structure in context