The Open Logic Text

en · official · sha256:d6ba5785678631e07b45ac15a5d101cd6a44758375617b5bee97067fbe625599EN

% 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, temporal logics 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 adding the 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}

Ссылаются нормы: TENSE_SINCE, TENSE_UNTIL

en · official · sha256:1b3e3a25b580b71525421afe08b29e9a0dc1305b81469de5ed6e498f6b44e084EN

% 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 been the case. Arthur Prior is credited as the originator of temporal logic, which he called \emph{tense logic}. Our treatment of temporal logic here will largely follow Prior's original modal treatment of introducing temporal operators into the basic framework of propositional logic, which treats claims as generally lacking in tense. 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 is sitting and also that Beezie is not sitting. But obviously both can be true, just not at the same time; adding temporal operators to the language can allow us to express that claim relatively easily. The addition of temporal operators also allows us to account for the validity of inferences like the one from ``Beezie will get a treat or a ball" to ``Beezie will get a treat or Beezie will get a ball." However, a lot of philosophical issues arise with temporal logic that might lead us to adopt one framework of temporal logic over another. For example, a future contingent is a statement about the future that is neither necessary nor impossible. If we say ``Richard will go to the grocery store tomorrow," we are expressing a claim about something that has not yet happened, and whose truth value is contestable. In fact, it is contestable whether that claim can even be \emph{assigned} a truth value in the first place. If we are strict determinists, then perhaps we can be comfortable with the idea that this sentence is in fact true or false, even before the event in question is supposed to take 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 the truth values of future contingents are undetermined. As it turns out, a lot of these commitments about the structure and nature of time are built in to our choices of models and frameworks of temporal logics. For example, we might ask ourselves whether we should construct models in which time is linear, branching or even circular. We might have to make decisions about whether our temporal models will have beginning and end points, and whether time is to be represented using discrete instants or as a continuum. \end{document}

en · official · sha256:174f124b596a7b0190458a70c68f56616d3f9121ecfec4e46a4169ace1a1f9a0EN

% 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 are extremely flexible, since we do not have to place any restrictions on the accessibility relation. This means that temporal models can branch in the past and in the future, but we might want to consider a more ``modal'' conception of branching, in which we consider sequences of events as possible histories. This does not necessarily require changing our language, though we might also add our ``ordinary'' modal operators $\Box$ and~$\Diamond$, and we could also consider adding epistemic 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 so relative to a history~$\sigma$, in which $t$ appears as a state. We do not need to change any of the semantics for !!{propositional variable}s or for truth-functional connectives, though. All of those are exactly as they were in \olref[sem]{defn:tmodels}, since none of those will make reference to~$\sigma$. However, we now redefine our future operator~$\Ftemp$ and add our~$\Diamond$ operator with respect to 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. For example, we might symbolize ``$p$~will not occur, but it might have occurred'' using the formula $\lnot \Ftemp p \land \Diamond \Ftemp p$. This would hold at a point and a history at which $p$ does not become true at a successor state, but there is an alternative history at which $p$ will become true. \end{document}

Ссылаются нормы: POSSIBLE_HISTORY

en · official · sha256:675d4938e8429c448c164c1691519b181fb9b3ae329cc289d25383ae48dddf8aEN

% 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 same notation ``model $\mModel{M}$ makes !!{formula}~$!A$ true at point~$t$'' for the basic notion of relational semantics. The relation is defined inductively and is identical to the normal modal case for all 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 the operators $\Ftemp$ and $\Gtemp$, such that we could define $\Htemp !A$ as $\lnot \Ptemp \lnot !A$, and the same with $\Gtemp$ and~$\Ftemp$. \end{document}

Ссылаются нормы: L_TENSE, TENSE_F, TENSE_G, TENSE_H, TENSE_MODEL, TENSE_P