#### 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 transitions rather than 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, a transition captures one of the immediate future possibilities at a branching
point in a tree \(\mathcal{T} = \langle T,\prec\rangle\) and is formally defined as a pair \(\langle t,H\rangle\)
consisting of a branching point \(t\in T\) and a set
\(H \subseteq \mathcal{H}(t)\) of locally undivided histories (where
two histories \(h,h'\in \mathcal{H}(t)\) are said to be undivided at
\(t\) iff there is some time instant \(t' \in h \cap h'\)
such that \(t\prec t'\)). A backward-linear strict partial ordering
between transitions is defined (\(\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
taken to be a possibly non-maximal, downward-closed chain in that ordering. 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 the relevant 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 \neg\varphi \mid (\varphi \wedge \varphi) \mid P\varphi \mid F\varphi \mid G\varphi \mid \Diamond\varphi \mid S\varphi.\]
In transition semantics, these formulae will be 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 admissible pairs \((t,C)\) at which \(p\) is considered true. The
*truth of an arbitrary formula \(\varphi\) at a pair \((t,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) \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\). The truth values of formulae about the future at an instant can change under
extensions of the given transition set, and the stability operator
\(S\) captures this behavior. A formula \(\varphi\) is said to be
*stably true* (*stably false*) at \((t,C)\) if it remains
true (false) at \(t\) with respect to all possible extensions of
\(C\). 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 admissible 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 be false
only contingently: the scheme \(\neg S\neg (F\varphi \vee
F\neg\varphi)\) is generally valid.

The Peircean and the Ockhamist branching time temporal logics can be obtained as limiting cases by restricting the range of admissible courses of events to the empty set of transitions and maximal chains, respectively. To spell this out 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{ is maximal linear}\}\). The corresponding classes of frames are definable by the formulae \(\varphi \leftrightarrow \Box \varphi\) and \(F\varphi \vee F\neg\varphi\), respectively.

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 is
provided that preserves validity, which naturally leads to
axiomatizability results.