Applied Modal Logic

Temporal Logics

content/applied-modal-logic/temporal-logic/temporal-logic.tex

% Part: applied-modal-logics% Chapter: temporal-logic\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{aml}{tl}{Temporal Logics}\begin{editorial}  This chapter covers temporal logics.\end{editorial}\olimport{introduction}\olimport{temporal-logic-semantics}\olimport{properties-accessibility}\olimport{extra-temporal-operators}\olimport{possible-histories}\OLEndPartHook\end{document}

content/applied-modal-logic/temporal-logic/introduction.tex

% Part: applied-modal-logics% Chapter: temporal-logic% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{aml}{tl}{int}\olsection{Introduction}Temporal logics deal with claims about things that will or have beenthe case. Arthur Prior is credited as the originator of temporallogic, which he called \emph{tense logic}. Our treatment of temporallogic here will largely follow Prior's original modal treatment ofintroducing temporal operators into the basic framework ofpropositional logic, which treats claims as generally lacking intense.For example, in propositional logic, I might talk about a dog, Beezie,who sometimes sits and sometimes doesn't sit, as dogs are wont to do.It would be contradictory in classical logic to claim that Beezie issitting and also that Beezie is not sitting. But obviously both can betrue, just not at the same time; adding temporal operators to thelanguage can allow us to express that claim relatively easily. Theaddition of temporal operators also allows us to account for thevalidity of inferences like the one from ``Beezie will get a treat ora ball" to ``Beezie will get a treat or Beezie will get a ball." However, a lot of philosophical issues arise with temporal logic thatmight lead us to adopt one framework of temporal logic over another.For example, a future contingent is a statement about the future thatis neither necessary nor impossible. If we say ``Richard will go to thegrocery store tomorrow," we are expressing a claim about something thathas not yet happened, and whose truth value is contestable. In fact,it is contestable whether that claim can even be \emph{assigned} atruth value in the first place. If we are strict determinists, thenperhaps we can be comfortable with the idea that this sentence is infact true or false, even before the event in question is supposed totake place---it just may be that we do not know its truth value yet.In contrast, we might believe in a genuinely open future, in which thetruth values of future contingents are undetermined. As it turns out, a lot of these commitments about the structure andnature of time are built in to our choices of models and frameworks oftemporal logics. For example, we might ask ourselves whether we shouldconstruct models in which time is linear, branching or even circular.We might have to make decisions about whether our temporal models willhave beginning and end points, and whether time is to be representedusing discrete instants or as a continuum. \end{document}

content/applied-modal-logic/temporal-logic/temporal-logic-semantics.tex

% Part: applied-modal-logics% Chapter: temporal-logic% Section: language-epistemic-logic\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{aml}{tl}{sem}\olsection{Semantics for Temporal Logic}\begin{defn}The basic language of temporal logic contains\begin{enumerate}  \tagitem{prvFalse}{The propositional constant for !!{falsity}~$\lfalse$.}{}  \tagitem{prvTrue}{The propositional constant for !!{truth}~$\ltrue$.}{}  \item A !!{denumerable}s set of !!{propositional variable}s: $\Obj    p_0$, $\Obj p_1$, $\Obj p_2$, \dots  \item The propositional connectives: \startycommalist  \iftag{prvNot}{\ycomma $\lnot$ (negation)}{}%  \iftag{prvAnd}{\ycomma $\land$ (conjunction)}{}%  \iftag{prvOr}{\ycomma $\lor$ (disjunction)}{}%  \iftag{prvIf}{\ycomma $\lif$ (!!{conditional})}{}%  \iftag{prvIff}{\ycomma $\liff$ (!!{biconditional})}{}.  \item Past operators $\Ptemp$ and $\Htemp$.  \item Future operators $\Ftemp$ and $\Gtemp$.\end{enumerate}\end{defn}Later on, we will discuss the potential addition of other kinds of modal operators.\begin{defn}\emph{!!^{formula}s} of the temporal language are inductively  defined as follows:\begin{enumerate}\tagitem{prvFalse}{$\lfalse$ is an atomic !!{formula}.}{}\tagitem{prvTrue}{$\ltrue$ is an atomic !!{formula}.}{}\item Every propositional variable $\Obj p_i$ is an (atomic) !!{formula}.\tagitem{prvNot}{If $!A$ is !!a{formula}, then $\lnot !A$ is  !!a{formula}.}{}\tagitem{prvAnd}{If $!A$ and $!B$ are !!{formula}s, then $(!A \land  !B)$ is !!a{formula}.}{}\tagitem{prvOr}{If $!A$ and $!B$ are !!{formula}s, then $(!A \lor !B)$  is !!a{formula}.}{}\tagitem{prvIf}{If $!A$ and $!B$ are !!{formula}s, then $(!A \lif !B)$  is !!a{formula}.}{}\tagitem{prvIff}{If $!A$ and $!B$ are !!{formula}s, then $(!A \liff !B)$  is !!a{formula}.}{}\item If $!A$ is !!a{formula}, then $\Ptemp  !A$, $\Htemp  !A$, $F !A$, $\Gtemp  !A$ are all  !!{formula}s.\tagitem{limitClause}{Nothing else is !!a{formula}.}{}\end{enumerate}\end{defn}The semantics of temporal logics are given in terms of relational models, as with other kinds of intensional logics. \begin{defn}  A \emph{model} for temporal language is a triple  $\mModel{M} = \tuple{T, \prec, V}$, where  \begin{enumerate}  \item $T$ is a nonempty set, interpreted as points in time.  \item $\prec$ is a binary relation on $T$.  \item $V$ is a function assigning to each !!{propositional    variable}~$p$ a set $V(p)$ of points in time.  \end{enumerate}  When $t \prec t'$ holds, we say that $t$ \emph{precedes}~$t'$.   When $t \in V(p)$ we say $p$ is \emph{true at}~$t$.\end{defn}For now, you will notice that we do not impose any conditions on our precedence relation $\prec$. This means that at present, there are no restrictions on the structure of our temporal models, so we could have models in which time is linear, branching, circular, or has any structure whatsoever. Just as with normal modal logic, every temporal model determines which!!{formula}s count as true at which points in it. We use the samenotation ``model $\mModel{M}$ makes !!{formula}~$!A$ true atpoint~$t$'' for the basic notion of relational semantics. The relationis defined inductively and is identical to the normal modal case forall non-modal operators.\begin{defn}\ollabel{defn:tmodels}  \emph{Truth of !!a{formula}~$!A$ at~$t$} in a~$\mModel M$, in symbols:  $\mSat{M}{!A}[t]$, is defined inductively as follows:  \begin{enumerate}  \tagitem{prvFalse}{\indcase{!A}{\lfalse}{Never $\mSat{M}{\lfalse}[t]$}.}{}  \tagitem{prvTrue}{\indcase{!A}{\ltrue}{Always $\mSat{M}{\ltrue}[t]$}.}{}  \item $\mSat{M}{p}[t]$ iff $t \in V(p)$  \tagitem{prvNot}{\indcase{!A}{\lnot !B}{$\mSat{M}{\indfrm}[t]$ iff    $\mSat/{M}{!B}[t]$}.}{}  \tagitem{prvAnd}{\indcase{!A}{(!B \land !C)}{$\mSat{M}{\indfrm}[t]$ iff    $\mSat{M}{!B}[t]$ and $\mSat{M}{!C}[t]$}.}{}  \tagitem{prvOr}{\indcase{!A}{(!B \lor !C)}{$\mSat{M}{\indfrm}[t]$ iff    $\mSat{M}{!B}[t]$ or $\mSat{M}{!C}[t]$} (or both).}{}  \tagitem{prvIf}{\indcase{!A}{(!B \lif !C)}{$\mSat{M}{\indfrm}[t]$ iff    $\mSat/{M}{!B}[t]$ or $\mSat{M}{!C}[t]$}.}{}  \tagitem{prvIff}{\indcase{!A}{(!B \liff !C)}{$\mSat{M}{\indfrm}[t]$ iff    either both $\mSat{M}{!B}[t]$ and $\mSat{M}{!C}[t]$ or    neither $\mSat{M}{!B}[t]$ nor $\mSat{M}{!C}[t]$}.}{}  \item\ollabel{defn:sub:mmodels-p}    \indcase{!A}{\Ptemp  !B}{$\mSat{M}{\indfrm}[t]$ iff    $\mSat{M}{!B}[t']$ for some $t' \in T$ with $t' \prec t$}\item\ollabel{defn:sub:mmodels-h}    \indcase{!A}{\Htemp  !B}{$\mSat{M}{\indfrm}[t]$ iff    $\mSat{M}{!B}[t']$ for every $t' \in T$ with $t' \prec t$}   \item\ollabel{defn:sub:mmodels-f}    \indcase{!A}{\Ftemp  !B}{$\mSat{M}{\indfrm}[t]$ iff    $\mSat{M}{!B}[t']$ for some $t' \in T$ with $t \prec t'$}\item\ollabel{defn:sub:mmodels-g}    \indcase{!A}{\Gtemp  !B}{$\mSat{M}{\indfrm}[t]$ iff    $\mSat{M}{!B}[t']$ for every $t' \in T$ with $t \prec t'$}  \end{enumerate} \end{defn}Based on the semantics, you might be able to see that the operators $\Ptemp$ and~$\Htemp$ are duals, as well as theoperators $\Ftemp$ and $\Gtemp$, such that we could define $\Htemp  !A$ as $\lnot \Ptemp \lnot !A$, and the same with $\Gtemp$ and~$\Ftemp$.\end{document}

content/applied-modal-logic/temporal-logic/properties-accessibility.tex

% Part: applied-modal-logics% Chapter: temporal-logic% Section: properties-accessibility\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{aml}{tl}{acc}\olsection{Properties of Temporal Frames}Given that our temporal models do not impose any conditions on therelation~$\prec$, the only one of our familiar axioms that holds inall models is~$K$, or its analogues $K_{\Gtemp}$ and~$K_{\Htemp}$:\begin{align*}\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)\end{align*}However, if we want our models to impose stricter conditions on howtime is represented, for instance by ensuring that $\prec$ is a linearorder, then we will end up with other validities in our models.\begin{table}[t]  \begin{tabular}{| p{.48\textwidth} || p{.48\textwidth} |}    \hline    {\emph{If $\prec$ is \dots}} & {\emph{then \dots is true in~$\mModel{M}$:}} \\    \hline \hline    \emph{transitive}: \newline    $\forall u \forall v \forall w ((u \prec v \land v \prec w) \lif u \prec w)$ &     $\Ftemp \Ftemp p \lif \Ftemp p$  \\    \hline     \emph{linear}: \newline    $\forall w \forall v (w \prec v \lor w = v \lor v \prec w)$ &      $(\Ftemp \Ptemp  p \lor \Ptemp \Ftemp p) \lif (\Ptemp p \lor p \lor \Ftemp p)$\\    \hline    \emph{dense}: \newline    $\forall w \forall v (w \prec v \to \exists u(w \prec u \land u \prec v))$ &      $\Ftemp p \lif \Ftemp \Ftemp p$ \\    \hline    \emph{unbounded (past)}: \newline    $\forall w \exists v( v \prec w)$ &      $\Htemp p \to \Ptemp p$ \\    \hline    \emph{unbounded (future)}: \newline    $\forall w \exists v( w \prec v)$ &      $\Gtemp p \to \Ftemp p$ \\    \hline  \end{tabular}  \caption{Some temporal frame correspondence properties.}  \ollabel{tab:correspondence}\end{table} Several of the properties from \olref{tab:correspondence} might seemlike desirable features for a model that is intended to representtime. However, it is worth noting that, even though we can imposewhichever conditions we like on the $\prec$ relation, not allconditions correspond to !!{formula}s that can be expressed in thelanguage of temporal logic. For example, irreflexivity, or the ideathat $\forall w \lnot (w \prec w)$, does not have a correspondingformula in temporal logic. \end{document}

content/applied-modal-logic/temporal-logic/extra-temporal-operators.tex

% Part: applied-modal-logics% Chapter: temporal-logic% Section: extra-operators\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{aml}{tl}{ext}\olsection{Additional Operators for Temporal Logic}In addition to the unary operators for past and future, temporallogics also sometimes include binary operators $\Since $ and~$\Until$,intended to symbolize ``since'' and ``until''. This means adding$\Since $ and~$\Until$ into the language of temporal logic and addingthe following clause into the definition of a temporal !!{formula}:\begin{itemize}\item[] If $!A$ and $!B$ are !!{formula}s, then $(\Since  !A !B)$ and  $(\Until !A !B)$ are both !!{formula}s.\end{itemize}The semantics for these operators are then given as follows:\begin{defn}\ollabel{defn:since-until}  \emph{Truth of !!a{formula}~$!A$ at~$t$} in a~$\mModel M$:  \begin{enumerate}  \item\ollabel{defn:sub:mmodels-since} \indcase{!A}{\Since  !B    !C}{$\mSat{M}{\indfrm}[t]$ iff $\mSat{M}{!B}[t']$ for some $t' \in    T$ with $t' \prec t$, and for all $s$ with $t' \prec s \prec t$,    $\mSat{M}{!C}[s]$}   \item\ollabel{defn:sub:mmodels-until} \indcase{!A}{\Until !B    !C}{$\mSat{M}{\indfrm}[t]$ iff $\mSat{M}{!B}[t']$ for some $t' \in    T$ with $t \prec t'$, and for all $s$ with $t \prec s \prec t'$,    $\mSat{M}{!C}[s]$}  \end{enumerate} \end{defn}The intuitive reading of $\Since  !B !C$ is ``Since $!B$ was the case,$!C$~has been the case.'' And the intuitive reading of $\Until !B !C$is ``Until $!B$ will be the case, $!C$~will be the case.''\end{document}

content/applied-modal-logic/temporal-logic/possible-histories.tex

% Part: applied-modal-logics% Chapter: temporal-logic% Section: possible-histories\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{aml}{tl}{poss}\olsection{Possible Histories}The relational models of temporal logic that we have been using areextremely flexible, since we do not have to place any restrictions onthe accessibility relation. This means that temporal models can branchin the past and in the future, but we might want to consider a more``modal'' conception of branching, in which we consider sequences ofevents as possible histories. This does not necessarily requirechanging our language, though we might also add our ``ordinary'' modaloperators $\Box$ and~$\Diamond$, and we could also consider addingepistemic accessibility relations to represent changes in agents'knowledge over time.\begin{defn}  A \emph{possible histories model} for the temporal language is a triple  $\mModel{M} = \tuple{T, C, V}$, where  \begin{enumerate}    \item $T$ is a nonempty set, interpreted as states in time.    \item $C$ is a set of computational paths, or \emph{possible      histories} of a system. In other words, $C$~is a set of      sequences~$\sigma$ of states $s_1$, $s_2$,~$s_3$, \dots, where      every $s_i \in T$.    \item $V$ is a function assigning to each !!{propositional      variable}~$p$ a set~$V(p)$ of points in time.  \end{enumerate}  To make things simpler, we will also generally assume that when a  history is in~$C$, then so are all of its suffixes. For example, if  $s_1$, $s_2$,~$s_3$ is a sequence in~$C$, then so are $s_2$, $s_3$  and~$s_3$. Also, when two states $s_i$ and~$s_j$ appear in a  sequence~$\sigma$, we say that $s_i \prec_\sigma s_j$ when $i < j$.  When $t \in V(p)$ we say $p$~is \emph{true at}~$t$.\end{defn}The one relevant change is that when we evaluate the truth of!!a{formula} at a point in time~$t$ in a model~$\mModel M$, we do sorelative to a history~$\sigma$, in which $t$ appears as a state. We donot need to change any of the semantics for !!{propositionalvariable}s or for truth-functional connectives, though. All of thoseare exactly as they were in \olref[sem]{defn:tmodels}, since none ofthose will make reference to~$\sigma$. However, we now redefine ourfuture operator~$\Ftemp$ and add our~$\Diamond$ operator with respectto these histories. \begin{defn}\ollabel{defn:phmodels}  \emph{Truth of !!a{formula}~$!A$ at~$t, \sigma$} in~$\mModel M$, in symbols:  $\mSat{M}{!A}[t, \sigma]$:  \begin{enumerate}  \item\ollabel{defn:sub:phmodels-f} \indcase{!A}{\Ftemp    !B}{$\mSat{M}{\indfrm}[t, \sigma]$ iff $\mSat{M}{!B}[t', \sigma]$    for some $t' \in T$ such that $t \prec_\sigma t'$.}  \item\ollabel{defn:sub:phmodels-diamond} \indcase{!A}{\Diamond    !B}{$\mSat{M}{\indfrm}[t, \sigma]$ iff $\mSat{M}{!B}[t, \sigma']$    for some $\sigma' \in C$ in which $t$ occurs.}  \end{enumerate} \end{defn}Other temporal and modal operators can be defined similarly. However,we can now represent claims that combine tense and modality. Forexample, we might symbolize ``$p$~will not occur, but it might haveoccurred'' using the formula $\lnot \Ftemp p \land \Diamond \Ftemp p$.This would hold at a point and a history at which $p$ does not becometrue at a successor state, but there is an alternative history atwhich $p$ will become true. \end{document}