#### Supplement to Temporal Logic

## Supplement: Transition Semantics

Transition semantics, introduced in Rumberg (2016), defines a branching
time temporal logic in which possible courses of events are modeled by
chains of local future possibilities, i.e. by linearly ordered sets
of *transitions*, rather than by histories. Whereas histories
represent complete possible courses of events, sets of transitions can
represent incomplete possible courses of events as well, which can then be
extended towards the future, thereby enabling a dynamic picture of the
interrelation of actuality, possibility, and time (for an intuitive
introduction to transition semantics along these lines, see Rumberg
2019).

The notion of a transition employed here generalizes the notion of a
transition prevalent in computer science. Intuitively, transitions
capture the immediate possible future continuations of a branching
point in a tree \(\mathcal{T} = \langle T,\prec\rangle\), and a
transition is formally defined as a pair \(\langle t,H\rangle\)
consisting of a branching point \(t\in T\) and an equivalence class
\(H \subseteq \mathcal{H}(t)\) of undivided histories at \(t\) (where
two histories \(h,h'\in \mathcal{H}(t)\) are said to be undivided at
\(t\) iff \(h,h' \in \mathcal{H}(t')\) for some time instant \(t'\)
such that \(t\prec t'\)). A backwards-linear strict partial ordering
between transitions is obtained along the following lines: \(\langle
t,H\rangle\) precedes \(\langle t',H'\rangle\) iff (\(t\prec t'\) and
\(H'\subset H\)), and a *possible course of events* \(C\) is
defined as a possibly non-maximal, downward-closed chain of
transitions ordered by that relation. Note that to every possible
course of events \(C\), there naturally corresponds a non-empty set of
histories, namely, the *set of histories allowed by \(C\)*,
defined by \(\mathcal{H}(C) := \bigcap_{\langle t,H\rangle\in C}
H\).

The transition language contains, in addition to temporal and modal operators, a so-called stability operator \(S\), which is interpreted as a universal quantifier over the possible future extensions of a given transition set. Given a set of atomic propositions \({PROP}\), the set of formulae of the transition language can be recursively defined as follows:

\[\varphi := p \in {PROP} \mid \bot \mid \neg\varphi \mid (\varphi \wedge \varphi) \mid P\varphi \mid F\varphi \mid G\varphi \mid \Diamond\varphi \mid S\varphi.\]
In transition semantics, formulae are evaluated in a model on a
tree \(\mathcal{T} = \langle T,\prec\rangle\) at pairs \((t,C)\)
consisting of a time instant \(t\in T\) and a possible course of
events \(C\) compatible with that instant, i.e. \(\mathcal{H}(C)
\cap \mathcal{H}(t) \neq \emptyset\). A *transition tree model*
is a triple \(\mathcal{M} = \langle T,\prec,V\rangle\) where
\(\mathcal{T} = \langle T,\prec\rangle\) is a tree and \(V\) is a
valuation that assigns to every atomic proposition \(p \in {PROP}\)
the set of pairs \((t,C)\) at which \(p\) is considered true. The
*truth of an arbitrary formula \(\varphi\) at an instant \(t\) with
respect to a possible course of events \(C\) in a transition tree
model \(\mathcal{M}\)* is defined inductively as follows:

- \(\mathcal{M},t,C \vDash p\) iff \((t,C) \in V(p)\), for \(p\in {PROP}\);
- \(\mathcal{M},t,C \not\vDash \bot\);
- \(\mathcal{M},t,C \vDash \neg\varphi\) iff \(\mathcal{M},t,C\not\vDash\varphi\);
- \(\mathcal{M},t,C \vDash \varphi \wedge \psi\) iff \(\mathcal{M},t,C \vDash \varphi\) and \(\mathcal{M},t,C \vDash \psi\);
- \(\mathcal{M},t,C \vDash P\varphi\) iff \(\mathcal{M},t',C \vDash\varphi\) for some time instant \(t'\) such that \(t'\prec t\);
- \(\mathcal{M},t,C \vDash F\varphi\) iff for all histories \(h\in \mathcal{H}(C) \cap \mathcal{H}(t)\), there is some time instant \(t' \in h\) such that \(t \prec t'\) and \(\mathcal{M},t',C \vDash \varphi\);
- \(\mathcal{M},t,C \vDash G\varphi\) iff for all histories \(h\in \mathcal{H}(C) \cap \mathcal{H}(t)\) and for all time instants \(t' \in h\) such that \(t \prec t'\), \(\mathcal{M},t',C \vDash \varphi\);
- \(\mathcal{M},t,C \vDash \Diamond\varphi\) iff \(\mathcal{M},t,C' \vDash \varphi\) for some possible course of events \(C'\) such that \(\mathcal{H}(C') \cap \mathcal{H}(t) \neq \emptyset\);
- \(\mathcal{M},t,C \vDash S\varphi\) iff \(\mathcal{M},t,C' \vDash \varphi\) for all possible courses of events \(C' \supseteq C\) such that \(\mathcal{H}(C') \cap \mathcal{H}(t) \neq \emptyset\).

Thus, a formula of the form \(F\varphi\) is true at an instant \(t\)
with respect to a possible course of events \(C\) iff every history
that passes through \(t\) and is allowed by \(C\) contains some later
instant \(t'\) at which \(\varphi\) is true relative to \(C\). Note
that, due to the relativization to the set of histories allowed by
\(C\), the truth values of formulae about the future can change under
extensions of the transition set \(C\), and the stability operator
\(S\) captures this behavior. A formula \(\varphi\) is said to be
*stably true* (*stably false*) at \((t,C)\) if it is
true (false) at \(t\) with respect to all possible extensions of
\(C\), i.e. no matter how the future unfolds later on. Formulae that
are neither stably true nor stably false are
*contingent*.

A formula of the transition language is *valid* iff it is true
at all pairs \((t,C)\) in all transition tree models. While transition
semantics validates the principle of excluded middle \(\varphi \vee
\neg \varphi\), it invalidates the principle of future excluded middle
\(F\varphi \vee F\neg\varphi\). However, the latter disjunction can
only be contingently false: the scheme \(\neg S\neg (F\varphi \vee
F\neg\varphi)\) is generally valid.

Both the Peircean and the Ockhamist branching time temporal logics can be obtained as limiting cases by restricting the range of possible courses of events to the empty set of transitions and maximal chains, respectively. To spell out the idea formally, we need to equip trees \(\mathcal{T} = \langle T,\prec\rangle\) with a primitive set of transition sets \(\mathit{TS}\) such that every time instant in \(\mathcal{T}\) belongs to a history allowed by some set of transitions in \(\mathit{TS}\). Peirceanism amounts to the case where \(\mathit{TS} = \{\emptyset\}\), whereas Ockhamism results if \(\mathit{TS} = \{C\mid C \text{ maximal linear}\}\). The corresponding classes of frames are definable by the formulae \(\varphi \leftrightarrow \Box \varphi\) and \(F\varphi \vee F\neg\varphi\), respectively.

Note that transition semantics is not a genuine Kripke-style
semantics, i.e., formulae are not solely evaluated at time instants,
which form the primitive elements of a tree, and the language contains
intensional operators which are not interpreted along the temporal
precedence relation between time instants. Rather, transition
semantics makes use of a second, defined parameter of truth, and the
transition sets employed as that second parameter are
set-theoretically rather complex. In Rumberg and Zanardo (2019) it is
shown that the set-theoretic complexity can be evaded: based on a
one-to-one correspondence between transition sets and certain tree
substructures, called *prunings*, a class of first-order
definable Kripke structures with a genuine Kripke-style semantics is
provided that preserves validity, which then naturally leads to
axiomatizability results.