---
abstract: 'This paper argues that a combined treatment of probabilities, time and actions is essential for an appropriate logical account of the notion of probability; and, based on this intuition, describes an expressive probabilistic temporal logic for reasoning about actions with uncertain outcomes. The logic is *modal* and *higher-order*: modalities annotated by actions are used to express possibility and necessity of propositions in the next states resulting from the actions, and a higher-order function is needed to express the probability operator. The proposed logic is shown to be an adequate extension of classical mathematical probability theory, and its expressiveness is illustrated through the formalization of the Monty Hall problem.'
author:
- Bruno Woltzenlogel Paleo
bibliography:
- 'bibliography.bib'
title: An Expressive Probabilistic Temporal Logic
---

Higher-Order Modal Logics, Probability Theory

Introduction
============

In order to reason about probabilistic knowledge, we must reason about time and actions as well. When we say, for example, that “the probability of ‘heads’ after a coin toss is 50% and that of ‘tails’ is 50%”, we implicitly assume that there is an action (in this example, tossing a coin) which can bring the world to different states in the next moment in time. The uncertainty lies in the state transition: the world may end up in a state where the coin shows heads or in a state where it shows tails.

Despite the evident dependence of our informal notion of probability on the notions of action and time, the formal mathematical languages that we use to talk about probabilities rarely support mentioning action and time explicitly. Kolmogorov’s probability theory, for example, merely defines probability as the measure function in a measure space with total measure 1 [@Kolmogorov]. The task of modeling time-dependent actions and their possible outcomes in terms of events in a probabilistic space remains informal. While this informality is not problematic in the simplest situations (e.g. when we are interested in the possible outcomes of a single action, or when multiple actions are independent of each other), slightly more complex situations may already lead to confusion and difficulty. A famous example is the Monty Hall problem [@MontyHall].

Another inconvenience of dealing with probabilities just in terms of a measure space is that its set-theoretic language (where events are represented as subsets of the sample space) is rather limited. There are obvious parallels between, for instance, set intersection and conjunction or set union and disjunction, which allow us to represent *propositional* probabilistic knowledge easily (e.g. the event of a randomly picked coin showing heads *and* the same coin being made of silver can be represented as the *intersection* of the event of showing heads with the event of being made of silver). However, it is not clear how this analogy could be extended to more expressive logics with quantifiers.

The main contribution of this paper, addressing the above mentioned issues, is the development of the syntax (in Section \[sec:Syntax\]) and the semantics (in Section \[sec:Semantics\]) of an expressive probabilistic temporal logic ([**PTL**]{}) for reasoning about actions with uncertain outcomes. [**PTL**]{}is an adequate extension of classical probability theory (as demonstrated in Section \[sec:Adequacy\]), and its greater expressiveness allows us to reason explicitly about event independence (as discussed in Section \[sec:Independence\]) and to avoid typical ambiguities of natural language discourse about probabilities (as shown in Section \[sec:Disambiguation\]). This capacity of [**PTL**]{}to avoid ambiguities related to outcomes and events is one of its main conceptual novelties in comparison to related work (cf. Section \[sec:RelatedWork\]). [**PTL**]{}’s convenience and expressive power are illustrated through the formalization of the Monty Hall problem (in Section \[sec:MontyHall\]).

Syntax {#sec:Syntax}
======

The aim of [**PTL**]{}’s language is to be sufficiently expressive to capture typical probabilistic statements, conveniently similar to natural language, and yet more precise than natural language in cases when the latter is ambiguous. Intuitively, probability is an inherently higher-order function, since it takes a proposition (representing an event) as an argument. Therefore, if a probabilistic logical language is to include a probability operator in the syntactic level, it is only natural that it should be a higher-order language. Furthermore, because thinking probabilistically involves numerical computation and reasoning about states and actions, it is convenient to have a typed language, with distinct basic types for numbers, states and actions. The types used here are mostly the well-known simple types, but a list type constructor is included as well, in order to allow the representation of temporal sequences of actions and propositions.

*Types* are freely generated from the set of basic types $\{ \beta, \iota, \eta, \mu \}$, the right-associative function type constructor ${\rightarrow}$ and the list type constructor ${\texttt{list}}$. $\mu$ is the type for *states*, $\beta$ is the type for *booleans*, $\iota$ is the type for *objects* and $\eta$ is the type for *real numbers*. The set of all types is denoted $T$. The type of (local) *propositions* $o$ is defined to be an abbreviation for $\mu {\rightarrow}\beta$ and the type of actions $\alpha$ is defined to be an abbreviation for $\mu {\rightarrow}{\texttt{list}}[\mu]$.

The definition of $o$ ensures that the truth of a proposition depends on states. The definition of $\alpha$ follows the intuition that an action can be seen as a function that maps a state to a list of possible next states.

As shown in Definition \[def:Symbols\], [**PTL**]{}contains, besides the usual logical symbols, also symbols for arithmetical functions and relations, the hybrid logic symbols for explicitly referring to states, list constructors and functions, and a probability operator. As modal operators (${\Box}$ and ${\Diamond}$) implicitly bind states, they have a more fundamental role, which reminds that of the $\lambda$ binder. Therefore, they are treated separately in Definition \[def:Expressions\].

\[def:Symbols\] For every type $\tau$, $S_{\tau}$ is a countably infinite set of uninterpreted symbols of type $\tau$. The set of arithmetic function symbols $S_{AF}$ is the set $\{ 0_{\eta}, 1_{\eta}, +_{\eta {\rightarrow}\eta {\rightarrow}\eta}, *_{\eta {\rightarrow}\eta {\rightarrow}\eta} \}$. The set of arithmetic relation symbols $S_{AR}$ is $\{ =_{\eta {\rightarrow}\eta {\rightarrow}o}, <_{\eta {\rightarrow}\eta {\rightarrow}o} \}$. The set of propositional logical symbols $S_L$ is $\{ \top_o, \bot_o, \vee_{o {\rightarrow}o {\rightarrow}o}, \wedge_{o {\rightarrow}o {\rightarrow}o}, {\rightarrow}_{o {\rightarrow}o {\rightarrow}o}, {\leftrightarrow}_{o {\rightarrow}o {\rightarrow}o}, \neg_{o {\rightarrow}o} \}$. The set of hybrid logical symbols $S_H$ is $\{ @_{\mu {\rightarrow}o {\rightarrow}o}, {\texttt{in}}_{\mu {\rightarrow}o} \}$. The set of quantifiers $S_Q$ is $\bigcup_{\tau \in T} \{{\forall}_{(\tau {\rightarrow}o) {\rightarrow}o}, {\exists}_{(\tau {\rightarrow}o) {\rightarrow}o}, =_{o {\rightarrow}o {\rightarrow}o}  \}$. The symbol ${\texttt{nil}}^\tau$ has type ${\texttt{list}}[\tau]$, ${::}^\tau$ has type $\tau {\rightarrow}{\texttt{list}}[\tau] {\rightarrow}{\texttt{list}}[\tau]$, $\in^{\tau}$ has type $\tau {\rightarrow}{\texttt{list}}[\tau] {\rightarrow}o$ and the length operator $|.|^{\tau}$ has type ${\texttt{list}}[\tau] {\rightarrow}\mu$. The probability operator ${\mathcal{P}}$ has type ${\texttt{list}}[\alpha] {\rightarrow}o {\rightarrow}\eta$. The set of all symbols $S$ is defined as $S_\tau \cup S_{AF} \cup S_{AR} \cup S_L \cup S_H \cup S_Q \cup \bigcup_{\tau \in T} \{{\texttt{nil}}^{\tau}, {::}^{\tau}, |.|^{\tau}, \in^{\tau}\} \cup \{ {\mathcal{P}}\}$.

Expressions are constructed as in the lambda calculus, using the symbols from $S$, application, abstraction and modalities.

\[def:Expressions\] *Expressions* are constructed according to the following rules:

-   if $s_{\tau} \in S$, then $s_{\tau}$ is an expression of type $\tau$.

-   if $t_1$ is an expression of type ${\tau {\rightarrow}\tau'}$ and $t_2$ is an expression of type $\tau$, then $(t_1~t_2)$ is an expression of type $\tau'$.

-   if $x_{\tau} \in S_{\tau}$ and $t$ is an expression of type $\tau'$, then $\lambda x_{\tau}. t$ is an expression of type $\tau {\rightarrow}\tau'$.

-   if $\varphi$ is an expression of type $o$, $p$ is an expression of type $\eta$ and $a$ is an expression of type $\alpha$, then ${\Diamond}^p_a \varphi$ are ${\Box}_a \varphi$ expressions of type $o$.

*Formulas* are expressions of type $o$. *Actions* are expressions of type $\alpha$. The set of expressions of type $\tau$ is denoted $E_{\tau}$. ${\mathcal{L}}= \bigcup_{\tau \in T} E_{\tau}$.

Types are omitted when they can be inferred from the context. The usual parenthesis conventions are followed. Numerals are occasionally written in decimal notation. Infix notation is employed as usual for logical connectives, arithmetical functions and relations and the list constructor ${::}$. Binding notation is used for quantifiers. Additionally, the following notation conventions and abbreviations are used:

-   ${\Diamond}_a \varphi \equiv {\exists}x_{\eta}. {\Diamond}^{x}_a \varphi$

-   ${\mathcal{P}}_l(\varphi) \equiv (({\mathcal{P}}~l)~\varphi)$

-   ${\forall}x:G.~H(x) \equiv {\forall}x.~G(x) {\rightarrow}H(x)$

-   ${\exists}x:G.~H(x) \equiv {\exists}x.~G(x) \wedge H(x)$

-   ${\forall}x_{\tau} \in \ell_{{\texttt{list}}[\tau]}.~H(x) \equiv {\forall}x.~ (x \in \ell) {\rightarrow}H(x)$

-   ${\exists}x_{\tau} \in \ell_{{\texttt{list}}[\tau]}.~H(x) \equiv {\exists}x.~ (x \in \ell) \wedge H(x)$

-   ${\mathcal{P}}_{a{::}l}(\varphi {::}L) \equiv {\mathcal{P}}_{a{::}l}(\varphi) \wedge {\mathcal{P}}_{l}(L)$ (with ${\mathcal{P}}_{{\texttt{nil}}}({\texttt{nil}}) \equiv \top$)

Probabilities appear in the logical language in two ways: firstly, as annotations on the diamond modal operator, in order to indicate how probable the corresponding state transition is; and secondly, through the higher-order probability function ${\mathcal{P}}$, which takes a list of actions and a proposition as arguments and returns the probability that the proposition will hold after the execution of the listed actions.

The following are some simple examples of probabilistic statements and their corresponding formalizations in [**PTL**]{}:

1.  Tossing a coin has a transition with probability $0.5$ to a state where the coin shows heads: $
    {\forall}x:\mathit{Coin}. {\Diamond}^{0.5}_{\mathit{toss}(x)} \mathit{heads}(x)
    $

2.  The probability of a coin showing heads after it is tossed is $0.5$: $${\forall}x:\mathit{Coin}. {\mathcal{P}}_{\mathit{toss}(x){::}{\texttt{nil}}}(\mathit{heads}(x)) = 0.5$$

3.  The probability of a coin showing heads twice after it is tossed twice is less than $0.5$: $
    {\forall}x:\mathit{Coin}. {\mathcal{P}}_{\mathit{t}(x){::}\mathit{t}(x){::}{\texttt{nil}}}(\mathit{h}(x){::}\mathit{h}(x){::}{\texttt{nil}}) < 0.5
    $ , where $t = \mathit{toss}$ and $h = \mathit{heads}$.

4.  After a coin is tossed it is necessarily either heads or tails: $${\forall}x:\mathit{Coin}. {\Box}_{\mathit{toss}(x)} (\mathit{heads}(x) \vee \mathit{tails}(x))$$

5.  After a coin is tossed it is possibly tails: $
    {\forall}x:\mathit{Coin}. {\Diamond}_{\mathit{toss}(x)} (\mathit{tails}(x))
    $

Semantics {#sec:Semantics}
=========

For each type $\tau$, we need a domain $D_{\tau}$ of elements on which expressions of type $\tau$ are interpreted. For numerical expressions, we assume the domain to be a real closed field. For booleans, we assume the set with the usual two truth values. For function types, we require *all* functions to be present in the type’s domain. This effectively results in a *standard* higher-order semantics. For *Henkin* semantics, it would suffice to drop this last condition.

A *domain* $D_{\tau}$ for a type $\tau$ is a non-empty set such that $D_{\tau' {\rightarrow}\tau}$ is the set of all functions from $D_{\tau'}$ to $D_{\tau}$ (for every $\tau'$ and $\tau$), $D_o = \{ {\mathbf{T}}, {\mathbf{F}}\}$, $D_{\eta} = {\mathbb{R}}$ and $D_{{\texttt{list}}[\tau]}$ is the set of all lists of elements from $D_{\tau}$.

As in the most common modal logics [@Blackburn], we use *frames* as the foundation for the modal aspects of the semantics. A frame is essentially a set of states and a relation for the transitions between states. What is different here is that transitions are labeled by actions and by probabilities, and the transition relation and actions must be mutually consistent.

\[def:Frame\] A *probabilistic labeled frame* is a triple $(W,R,{P})$ such that $W$ is a non-empty set of *states*, $R \subseteq W \times W \times D_{\alpha}$ satisfying the condition that if $(w, w', \ell) \in R$ then $(w, w'', \ell) \in R$ for every $w'' \in \ell(w)$, and ${P}: R {\rightarrow}[0,1]$ is a probability function satisfying the condition that for all $w \in W$ and for all $\ell \in D_{\alpha}$ such that there exists $w' \in W$ with $(w, w', \ell) \in R$, $$\sum_{w' ~ | ~ (w, w', \ell) \in R } {P}((w,w',\ell)) = 1$$

The relation $R$ in definition \[def:Frame\] may be cyclic. This is convenient, for instance, when specifying Markov chains.

A model extends a frame with an interpretation function that assigns denotations to expressions. The denotation of an expression may generally vary with the state. In such cases, we say that the interpretation is *flexible*; otherwise, it is *rigid* [@Fitting]. In the examples considered in this paper, boolean expressions and probabilistic expressions are always flexibly interpreted, whereas other expressions are always rigidly interpreted.

\[def:Model\] A *model* is a tuple $(W, R, {P}, \{ D_{\tau} \}_{\tau \in T}, I)$ where $(W, R, {P})$ is a probabilistic labelled frame, $\{ D_{\tau} \}_{\tau \in T}$ is a domain, $W = D_{\mu}$ and $I$ is an interpretation function that maps states and expressions of any type $\tau$ to elements in $D_{\tau}$. It is assumed that any interpretation $I$ maps arithmetic symbols, list constructors and functions, and logical constants to their usual fixed denotations. Therefore (as usual, non-exhaustively):

-   $I_w(A \wedge B) = {\mathbf{T}}$ iff $I_w(A) = {\mathbf{T}}$ and $I_w(B) = {\mathbf{T}}$

-   $I_w(A \vee B) = {\mathbf{T}}$ iff $I_w(A) = {\mathbf{T}}$ or $I_w(B) = {\mathbf{T}}$

-   $I_w(A {\rightarrow}B) = {\mathbf{T}}$ iff $I_w(A) = {\mathbf{F}}$ or $I_w(B) = {\mathbf{T}}$

-   $I_w(\neg A) = {\mathbf{T}}$ iff $I_w(A) = {\mathbf{F}}$

-   $I_w({\forall}x_{\tau}. \varphi) = {\mathbf{T}}$ iff $I_w[x \mapsto e](\varphi) = {\mathbf{T}}$ for every $e \in D_{\tau}$

-   $I_w({\exists}x_{\tau}. \varphi) = {\mathbf{T}}$ iff $I_w[x \mapsto e](\varphi) = {\mathbf{T}}$ for some $e \in D_{\tau}$

-   $I_w( (t_1~t_2) ) = (I_w(t_1)~I_w(t_2))$

-   $I_w(\lambda x_{\tau}. t)$ is the function taking an element $e \in D_{\tau}$ and returning $I_w[x \mapsto e](t)$.

-   $I_w({\texttt{in}}(s)) = {\mathbf{T}}$ iff $w = I_w(s)$

-   $I_w(@_s \varphi) = {\mathbf{T}}$ iff $I_{I_w(s)}(\varphi) = {\mathbf{T}}$

where $I_w[x \mapsto e](x) = e$ and $I_w[x \mapsto e](t) = I[t]$ for any $t$ distinct from $x$.

Furthermore, and most importantly, the interpretations of expressions formed with modal and probabilistic operators are defined as follows:

-   $I_w({\Box}_a \varphi) = {\mathbf{T}}$ iff $I_{w'}(\varphi) = {\mathbf{T}}$\
    for every $w'$ such that $(w, w', I_w(a)) \in R$

-   $I_w({\Diamond}_a^p \varphi) = {\mathbf{T}}$ iff ${P}((w,w',I_w(a))) = I_w(p)$ and $I_{w'}(\varphi) = {\mathbf{T}}$\
    for some $w'$ such that $(w, w', I_w(a)) \in R$

-   $I_w({\mathcal{P}}_{\texttt{nil}}(\varphi)) = \begin{cases}
                                1, & \text{if } I_w(\varphi) = {\mathbf{T}}\\
                                0, & \text{if } I_w(\varphi) = {\mathbf{F}}\end{cases} $

-   $I_w({\mathcal{P}}_{a{::}l}(\varphi)) = \sum\limits_{w' | (w, w', I_w(a)) \in R } {P}((w,w',I_w(a))) . I_{w'}({\mathcal{P}}_l(\varphi)) $

In the probabilistic logic [**PTL**]{}, validity and satisfaction of a formula by a model are standard non-probabilistic notions, as defined below. The logic handles probabilities explicitly in its language; not at the semantic level.

\[def:Satisfaction\] A formula $\varphi$ is *satisfied* in a model $M \equiv (W, R, {P}, \{ D_{\tau} \}_{\tau \in T}, I)$ in a state $w$, denoted $M, w \vDash \varphi$ iff $I_w(\varphi) = {\mathbf{T}}$. A formula $\varphi$ is *globally satisfied* in a model $M$, denoted $M \vDash \varphi$ iff $M, w \vDash \varphi$ for all $w \in W$. A formula $\varphi$ is *valid*, denoted $\vDash \varphi$ iff $M \vDash \varphi$ for every model $M$. A set of formulas $T$ entails a formula $\varphi$, denoted $T \vDash \varphi$, iff $M \vDash \varphi$ for every model $M$ such that $M \vDash \bigwedge_{G \in T} G$.

Adequacy {#sec:Adequacy}
========

This section shows how the usual mathematical presentation of probability theory, as recalled in Definition \[def:ProbabilitySpace\], can be considered a special case of the probabilistic logic presented here. This is done by showing (in Theorem \[theorem:Adequacy\]) how to translate probability spaces into models and the usual set-theoretic language for probabilistic events into [**PTL**]{}’s language.

*Set expressions* over a set $\Omega$ are expressions freely generated from singleton subsets of $\Omega$ and operators for complementation ($\overline{\phantom{\{ \}}}$), union ($\cup$) and intersection ($\cap$).

As usual, by abuse of notation, set expressions and the sets they denote are not explicitly distinguished.

If $\Omega = \{ w_1, w_2 \}$ then the following are examples of set expressions: $\{w_1\}$, $\{w_2\}$, $\overline{\{w_2\}}$ (denoting the set $\{ w_1 \}$), $\{w_1\} \cup \{w_2\}$ (denoting the set $\{w_1, w_2\}$), $\{w_1\} \cap \{w_2\}$ (denoting the empty set), …

\[def:ProbabilitySpace\] A *probability space* is a triple $(\Omega, \Sigma, Q)$ where $\Omega$ is the *sample space* (whose elements are *outcomes*), $\Sigma$ is a *$\sigma$-algebra* on $\Omega$ (i.e. a collection of subsets of $\Omega$ (*events*) closed under complementation, countable union and countable intersection) and $Q: \Sigma {\rightarrow}[0,1]$ is a probability function satisfying Kolmogorov’s axioms:

1.  $Q(E) \geq 0$, for all $E \in \Sigma$

2.  $Q(\Omega) = 1$

3.  For any countable collection $C$ of mutually disjoint events $$Q(\bigcup_{E \in C} E) = \sum_{E \in C} Q(E)$$

\[theorem:Adequacy\] For every probability space $(\Omega, \Sigma, Q)$, there is a model $M$ and a language translation function $g$ from set expressions over $\Omega$ to formulas such that $Q(E) = p$ iff $M, w \vDash {\mathcal{P}}_a(g(E)) = p$, for some $w$ and some $a$.

Let $W$ be $\{ w \} \cup \Omega$. For each $w_k \in \Omega$, let $F_k$ be a distinct atomic proposition. Let $I$ be any interpretation such that $I_{w_i}(F_j) = {\mathbf{T}}$ iff $i = j$. Let $R$ be $\{ (w, w_k, I_w(a)) | w_k \in \Omega \}$. Let the probabilistic transition function be defined such that ${P}((w, w_k, I_w(a))) = Q(\{w_k\})$. Since $\Omega = \bigcup_k \{w_k\}$, all $\{w_k\}$ are mutually disjoint and $Q(\Omega) = 1$, the condition (from Definition \[def:Frame\]) that $$\sum_{w_k ~ | ~ (w, w_k, I_w(a)) \in R } {P}((w,w_k,I_w(a))) = 1$$ holds. Finally let $M$ be the model $(W,R,{P},\{D_{\tau}\}_{\tau \in T},I)$. The translation function $g$ is defined recursively: $$g(E) = \begin{cases}
           F_k, & \text{if } E = \{ w_k \} \\
           g(E') \vee g(E''), & \text{if } E = E' \cup E'' \\
           g(E') \wedge g(E''), & \text{if } E = E' \cap E'' \\
           \neg g(E'), & \text{if } E = \overline{E'}
        \end{cases}$$ Now the fact that $Q(E) = p$ iff $M, w \vDash {\mathcal{P}}_a(g(E)) = p$ must be proven. First notice that, by Definition \[def:Satisfaction\], $M, w \vDash {\mathcal{P}}_a(g(E)) = p$ iff $I_w({\mathcal{P}}_a(g(E)) = p)$, and by Definition \[def:Model\], $I_w({\mathcal{P}}_a(g(E)) = p)$ iff $$\sum_{w' ~ | ~ (w, w', I_w(a)) \in R } {P}((w,w',I_w(a))). I_{w'}({\mathcal{P}}_{{\texttt{nil}}}(g(E))) = p$$ By Definition \[def:Model\] again and the definition of $R$, the summation above can be simplified, resulting in the following equation: $$\sum_{w' | w' \in \Omega \text{ and } I_{w'}(g(E)) = {\mathbf{T}}\}} {P}((w,w',I_w(a))) = p$$ Furthermore, unfolding the definition of ${P}$, the equation above reduces to: $$\sum_{w' | w' \in \Omega \text{ and } I_{w'}(g(E)) = {\mathbf{T}}\}} Q(\{w'\}) = p$$ Therefore, it suffices to prove that the equation above holds iff $Q(E) = p$, or equivalently, that: $$\sum_{w' | w' \in \Omega \text{ and } I_{w'}(g(E)) = {\mathbf{T}}\}} Q(\{w'\}) = Q(E)$$ By Kolmogorov’s third axiom, $Q(E) = \sum_{w' \in E} Q(\{w'\}$. Hence, letting $X$ be the following set: $$\{ x | x \in \Omega \text{ and } I_x(g(E)) = {\mathbf{T}}\}$$ A sufficient condition for the equation above to hold is that $X = E$. This is proven below by induction on the structure of $E$:

-   **Base case** ($E = \{w_k\}$): then $g(E_k) = F_k$ and, by definition of $I$, $I_x(F_k) = {\mathbf{T}}$ iff $x = w_k$.

-   **Induction cases**:

    -   ($E = \overline{E'}$): then $g(E) = \neg g(E')$ and hence: $$X = \{ x | x \in \Omega \text{ and not } I_x(g(E')) = {\mathbf{T}}\}$$ Let $$Y = \{ x | x \in \Omega \text{ and } I_x(g(E')) = {\mathbf{T}}\}$$ By induction hypothesis, $Y = E'$. Therefore, $X = \Omega \setminus Y = \Omega \setminus E' = E$.

    -   ($E = E' \cap E''$): then $g(E) = g(E') \wedge g(E'')$ and hence: $$X = \{ x | x \in \Omega \text{ and } I_x(g(E') \wedge g(E'')) = {\mathbf{T}}\}$$ and so: $$X = \{ x | x \in \Omega \text{ and } I_x(g(E')) = {\mathbf{T}}\text{ and } I_x(g(E'')) = {\mathbf{T}}\}$$ Let: $$Y = \{ x | x \in \Omega \text{ and } I_x(g(E')) = {\mathbf{T}}\}$$ $$Z = \{ x | x \in \Omega \text{ and } I_x(g(E'')) = {\mathbf{T}}\}$$ By induction hypothesis, $Y = E'$ and $Z = E''$. Therefore, $X = Y \cap Z = E' \cap E'' = E$.

    -   ($E = E' \cup E''$): this case is analogous to the case above.

Informally, the idea of the proof of Theorem \[theorem:Adequacy\] is to translate a probability space into a model with a distinguished initial state and a future state for each possible outcome in the space. Any set expression (specifying an event) has a corresponding logical formula. The correspondence is as expected: union corresponds to disjunction, intersection to conjunction and complementation to negation. The translation is *adequate* in the sense that the probability of an event in the space is equal to the probability of the corresponding formula in the model.

Expressiveness {#sec:Expressiveness}
==============

A corollary of Theorem \[theorem:Adequacy\] is that the probabilistic logic [**PTL**]{}is more expressive than classical probability theory, in two distinct informal senses. The first one is syntactical: whereas the usual language of classical probability theory (which relies on set expressions) can naturally express formulas containing propositional connectives such as negation, conjunction and disjunction (through the inverse of the translation function $g$ defined in the proof of the theorem), there are formulas in [**PTL**]{}’s language (e.g. formulas containing quantifiers or nested probability operators) which have no (natural) counterpart in the language of classical probability theory. The second one is semantical: the proof of Theorem \[theorem:Adequacy\] shows that probability spaces correspond to models with a very simple frame; it would be inconvenient to express models with more complex frames in terms of probability spaces, because the frame structure would have to be flattened.

Independence {#sec:Independence}
------------

Shortcomings and limitations of probability spaces for knowledge representation become apparent in situations where a sequence of independent actions is performed over time. Suppose that a fair coin is tossed twice. Representing this as a probability space requires a sample space with four outcomes $\{ h_1h_2, h_1t_2, t_1h_2, t_1t_2 \}$. Saying that, for instance, $P(\{h_1h_2\}) = P(H_1 \cap H_2) = P(H_1) P(H_2) = 0.25$ (where $H_1 = \{h_1t_2,h_1h_2\}$ and $H_2 = \{h_1h_2,t_1h_2\}$) requires the assumption of independence for the tosses. Two events $E_1$ and $E_2$ are often defined to be *independent* if and only if $P(H_1 \cap H_2) = P(H_1) P(H_2)$. But this definition is epistemologically unsatisfactory. How do we actually come to know that $H_1$ and $H_2$ are independent? According to this definition, we must know $P(H_1 \cap H_2)$ in advance. But that is precisely what, in practice, we do *not* know and would like to compute (based on our knowledge of $P(H_1)$ and $P(H_2)$)! We can easily get trapped in circular reasoning, trying to justify, for instance, our claim that $P(H_1 \cap H_2) = 0.25$ by saying that $H_1$ and $H_2$ are independent and then trying to justify that they are independent by saying that $P(H_1 \cap H_2) = 0.25$. Of course, we tend to escape from such cases of fallacious circular reasoning by simply assuming that the events are independent. However, the assumption is *tacit*. Classical probability theory provides no way to represent knowledge of the independence and any reason that we might have for justifying the assumption of independence of the events remains at an informal level, external to the representation.

In the [**PTL**]{}, on the other hand, the possibility to represent independence comes naturally and for free. For instance, when the axiom ${\forall}x:Coin. {\Diamond}_{t(x)}^{0.5}. H(x) \wedge {\Diamond}^{0.5}_{t(x)}T(x)$ is assumed, it follows from the semantics of the logic that it holds in any state of the model. And since the axiom states the equal probabilities for heads and tails in a way that does not depend on anything except the action of the toss itself, it is clear that tossing a coin at a state $s$ has no effect on tossing the coin at another state $s'$. Therefore, the two tosses must be independent, and consequently it follows that: $${\forall}x:Coin. {\Diamond}_{t(x)}^{0.5}. H(x) \wedge {\Diamond}^{0.5}_{t(x)}T(x) \vDash {\mathcal{P}}_{t(x){::}t(x){::}{\texttt{nil}}}(H(x){::}H(x) {::}{\texttt{nil}}) = 0.25$$

Also dependence can be easily represented. For example, consider a magical coin $c_m$ that behaves as a fair coin in an initial state, but when tossed in any other state always gives the opposite result of the previous toss. This may be represented by the following axioms:

-   $@_s {\Diamond}_{t(c_m)}^{0.5}. H(c_m) \wedge {\Diamond}^{0.5}_{t(c_m)}T(c_m)$

-   $T(c_m) {\rightarrow}{\Diamond}_{t(c_m)}^{1}. H(c_m)$

-   $H(c_m) {\rightarrow}{\Diamond}_{t(c_m)}^{1}. T(c_m)$

-   ${\Box}\neg {\texttt{in}}(s)$ (no state is a predecessor of $s$)

The inadequacy of classical probability theory’s usual definition of independence can be further illustrated in a situation where we have to randomly get an object from a bag with four objects: a black sphere, a white sphere, a black cube and a white cube. For simplicity, we assume tacitly that we put the object back in the bag after the action. This can be represented by the following axioms: **A1:** $S(s_b) \wedge B(s_b)$; **A2:** $S(s_w) \wedge W(s_w)$; **A3:** $C(c_b) \wedge B(c_b)$; **A4:** $C(c_w) \wedge W(c_w)$; **A5:** $\mathit{Bag} = s_b {::}s_w {::}c_b {::}c_w {::}{\texttt{nil}}$; and **A6:** ${\forall}x \in \mathit{Bag}. {\Diamond}_{a}^{1/|\mathit{Bag}|} G(x)$. It then follows, by the semantics, that: $$\textrm{A1}, \textrm{A2}, \textrm{A3}, \textrm{A4}, \textrm{A5}, \textrm{A6} \vDash {\forall}x \in \mathit{Bag}. {\mathcal{P}}_a(S(x) \wedge B(x)) = {\mathcal{P}}_a(S(x)) . {\mathcal{P}}_a(B(x))$$ Nevertheless, we should not be willing to conclude from this result, as classical probability theory does, that the event of getting a spherical object and the event of getting a black object are independent. It is merely coincidental that ${\mathcal{P}}_a(S(x) \wedge B(x)) = {\mathcal{P}}_a(S(x)) . {\mathcal{P}}_a(B(x))$. If the bag had an additional black tetrahedral, for instance, the two sides of this equation would not be equal anymore. In the formalization above, it is evident that both events are correlated, because they consist of outcomes from a single action.

A simple formal theory $T_{\mathit{indep}}$ of (in)dependence of actions could provide the following definition for *independence* of an action $a$ from an action $b$:

-   $ \mathit{Independent}(a,b) \equiv ({\forall}s. @_s (({\forall}\varphi. {\forall}p. {\mathcal{P}}_a(\varphi) = p {\rightarrow}{\Box}_b ({\mathcal{P}}_a(\varphi) = p))) $

It follows from the semantics that $T_{\mathit{indep}}$ entails the following *shortcut* theorem:

$$\bigwedge_{1\leq i < j \leq n} \mathit{Independent}(a_i,a_j) {\rightarrow}{\mathcal{P}}_{a_1{::}\ldots{::}a_n {::}{\texttt{nil}}}(E_1{::}\ldots{::}E_n {::}{\texttt{nil}}) = {\mathcal{P}}_{a_1}(E_1)\ldots{\mathcal{P}}_{a_n}(E_n)$$

The notion of independence defined in $T_{\mathit{indep}}$ is non-circular. We may, from the logical specification of a system in the [**PTL**]{}’s language, explicitly reason about the actions of the system, conclude that some of them are mutually independent and use the general theorem above as a shortcut for computing probabilities of sequences of actions. This is arguably more satisfactory than the teleological definition of independence from classical probability theory, which depends on the very shortcut theorem that we would have liked to derive.

It is not an aim of this paper to discuss $T_{\mathit{indep}}$ or other theories of independence in detail. $T_{\mathit{indep}}$ is just a (very simple) example showing that [**PTL**]{}is expressive enough to allow explicit reasoning about concepts that are very relevant in a probabilistic context.

Disambiguation {#sec:Disambiguation}
--------------

Informal statements about probabilities are sometimes imprecise and ambiguous. Their intended meanings are not always clear. If a person $A$ tried to describe to a person $B$ the random effects of an action $a$, her description might include a sentence such as: “the probability of $\varphi$ after $a$ is $p$”. The most straightforward and literal logical meaning for this sentence would be ${\mathcal{P}}_a(\varphi) = p$. However, it is often the case that the meaning intended by $A$ is actually ${\Diamond}_a^p \varphi$. $B$ must guess, from the context of the conversation and the common knowledge, which of the two alternatives is actually meant.

A formula such as ${\Diamond}_a^p \varphi$ provides fine-grained information about one particular state transition that is made possible by the action, whereas ${\mathcal{P}}_a(\varphi) = p$ provides coarse-grained aggregated information about transitions to all states where $\varphi$ holds. The aggregated information is incomplete, because it doesn’t say how many such states there are and it doesn’t specify the transition probability to each of these states.

The power to disambiguate is an interesting qualitative criterium to estimate the usefulness of a formal language. The formal probabilistic logical language proposed here is expressive enough to precisely disambiguate between ${\Diamond}$ and ${\mathcal{P}}$, which are subtly but importantly different in meaning, even though they are often expressed indistinguishably in natural language. It is important to note that neither ${\Diamond}_a^p \varphi {\rightarrow}{\mathcal{P}}_a(\varphi) = p$ nor ${\mathcal{P}}_a(\varphi) = p {\rightarrow}{\Diamond}_a^p \varphi$ is valid. Understanding the difference between ${\Diamond}_a^p \varphi$ and ${\mathcal{P}}_a(\varphi) = p$ is crucial for a correct use of [**PTL**]{}. Furthermore, the difference in the meanings of ${\Diamond}$ and ${\mathcal{P}}$ is essential to a semantics for probabilities that is compatible with our intuition about probabilities. Therefore, any sufficiently rich probabilistic logic should strive to distinguish between these important notions. [**PTL**]{}does so explicitly and syntactically.

In natural language dialogues, $B$ tends to cope with the ambiguity by subconsciously attempting to presuppose that $\varphi$ fully specifies a single outcome of $a$, in which case $A$ means ${\Diamond}_a^p \varphi$. If this presupposition is incompatible with pre-existing knowledge or even with knowledge acquired later during the dialogue, the presupposition is canceled and the meaning falls back to ${\mathcal{P}}_a(\varphi) = p$. Fully understanding the dynamics of presuppositions is an open linguistic challenge, and probabilities bring yet another dimension of complexity to this difficult problem.

Consider the following statement:

-   “the probability of picking number $n$ (for $1 \leq n \leq 6$) is $1/6$”

Upon hearing this sentence, we tend to presuppose that there are six outcomes (i.e. ${\Diamond}_{\mathrm{pick}}^{1/6} \mathrm{Picked}(n)$). However, if we are later told that:

-   “the number is picked by throwing a 12-faced fair dice where each $n$ (for $1 \leq n \leq 6$) occurs in two distinct faces.”

we are forced to cancel our presupposition and revise our logical interpretation of the previous sentence.

Implementation and Automation {#sec:Implementation}
=============================

A preliminary implementation of [**PTL**]{}in `Coq` is available in <https://github.com/Paradoxika/ProbLogic>. It follows the embedding methodology used in [@ECAI; @CSR], which is based on a higher-order and typed version of the standard translation of modal logics into predicate logic, with three important differences. Firstly, whereas in the standard translation the accessibility relation is a primitive constant, in the embedding of [**PTL**]{}it is derived from the primitive notion of action. Secondly, the higher-order modal logics used in [@ECAI] were *rigid*, while [**PTL**]{}includes a flexible probability function ${\mathcal{P}}$ (which is simulated by a flexible predicate in the implementation). Finally, in contrast to the logics from [@ECAI], [**PTL**]{}requires numerical reasoning. It is this last point that makes the embedding of [**PTL**]{}significantly harder than previous embeddings and justifies its preliminary status. The current implementation still does not provide convenient modal tactics (as those described in [@CSR]) and numerical reasoning is done with `Coq`’s standard `QArith` library for rationals (instead of real-closed fields). Decidability (of the satisfiability, validity and entailment problems) is indeed, of course, hopeless for the proposed *higher-order* logic. But even for logics with undecidability issues, automated theorem provers are occasionaly sufficiently efficient for practical applications [@ECAI]. It is also important to note that, even if arithmetical expressions (of type $\eta$) are restricted to be ground (i.e. by forbidding quantifiers of type $(\eta {\rightarrow}o) {\rightarrow}o$), [**PTL**]{}thus restricted would still be expressive enough to formalize all the examples shown in this paper. In this restricted logic, the only automation of arithmetic needed is simplification/computation of arithmetic expressions and reduction of ground simplified arithmetic propositions to $\top$ or $\bot$. With the recent progress in SMT-solving and automated theorem proving modulo arithmetic (even with quantifiers), it is reasonable to hope that automated provers will soon be able to cope with [**PTL**]{}problems. In the meanwhile, the current implementation in `Coq` has already proven to be sufficient for a fully interactive formalization of the Monty Hall problem, as described in the next section.

The Monty Hall Problem {#sec:MontyHall}
======================

[**PTL**]{}is used here in the formalization of vos Savant’s famous *Monty Hall problem* [@MontyHall], whose description is reproduced below:

*Suppose you’re on a game show, and you’re given the choice of three doors: Behind one door is a car; behind the others, goats. You pick a door, say No. 1, and the host, who knows what’s behind the doors, opens another door, say No. 3, which has a goat. He then says to you, ‘Do you want to pick door No. 2?’ Is it to your advantage to switch your choice?*

This probabilistic puzzle is seemingly paradoxical, because people very often make mistakes when they reason *informally* about the problem, as they tend to wrongly compute the probabilities. Therefore, despite its apparent simplicity, this problem is an interesting benchmark for evaluating *formal* probabilistic logics. A good probabilistic logic should allow a sufficiently natural and unambiguous formal representation of the problem and should entail correct probability values. From the player’s point of view, the Monty Hall problem can be formalized in [**PTL**]{}by the following axioms:

-   **Axiom 1:** “you’re given the choice of three doors”: $
    {D}= d_1 {::}d_2 {::}d_3 {::}{\texttt{nil}}$

-   **Axiom 2:** “behind one door is a car”: $
    {\exists}d \in {D}. C(d)
    $

-   **Axiom 3:** “behind the others, goats”: $
    {\forall}d \in {D}. \neg C(d) {\leftrightarrow}G(d)
    $

-   **Axiom 4:** “you pick a door, say No. 1, and the host, who knows what’s behind the doors, opens another door, say No. 3, which has a goat.”: $${\exists}s_c. ((@_{s_0} {\Diamond}_{{h}} {\Diamond}_{{p}(d_1)} {\Diamond}_{{o}} {\texttt{in}}(s_c)) \wedge @_{s_c} (O(d_3) \wedge G(d_3)) )$$

A more literal reading of Axiom 4 would be that “there exists a state (the current state), reachable from the initial state by the sequence of actions in which the host hides the car (${h}$), the player picks the first door (${p}(d_1)$), and the host opens a door (${o}$), where the third door is open and has a goat.”. It is fair to say that the axioms shown above capture the intended meanings of their corresponding informal natural language sentences. As desired, the axioms are reasonably similar to the corresponding sentences, although there are interesting differences worth discussing, particularly in relation to Axiom 4. Firstly, it illustrates the need for the hybrid logic operators $@$ and ${\texttt{in}}$ in situations where it is important to declare *local* conditions, which hold only in a single given state. Secondly, it shows the convenience of having a versatile approach to actions. The $\mathit{pick}$ ($p$) action, for instance, takes the picked door as an argument whereas the $\mathit{open}$ ($o$) action takes no argument. This allows us to express that, from the point of view of the player, the action of picking a door is an action of the player and he can choose which door to pick, while opening a door is an action performed by the host, with uncertain outcomes to the player. The opening of the third door is represented as a random event of the action, through the proposition $O(d_3)$. These subtle differences between Axiom 4 and its corresponding sentence in the informal description of the problem are evidence that, as expected from a formal language, [**PTL**]{}offers a higher degree of precision than what we are used to in natural language.

There are many assumptions that are not explicitly mentioned in the description of the problem. But they must be formalized as well. We list below only some of them. Other axioms (e.g. stating what remains unchanged when actions are excuted) can be see in the `Coq` formalization discussed in Section \[sec:Implementation\].

-   **Axiom 5:** Each door has equal probability of having the car after the $\mathit{hide}$ ($h$) action: $
    {\forall}d \in {D}. {\Diamond}_{{h}}^{1/|{D}|} C(d)
    $

-   **Axiom 6:** The $\mathit{pick}$ ($p$) action marks the picked door: $
    {\forall}d \in {D}. {\Diamond}_{{p}(d)}^1 P(d)
    $

-   **Axiom 7:** The host opens a door containing a goat with uniform probability among the doors that are neither picked nor contain a car:

    $${\forall}d^c. {\forall}d^p. (C(d^c) {\rightarrow}P(d^p) {\rightarrow}{\forall}d \in (({D}- d^c) - d^p). {\Diamond}_{{o}}^{1/|(({D}- d^c) - d^p)|} O(d) )$$

-   **Axiom 8:** When the player does the *switch* (${s}$) action, the newly picked door is different from the previously picked door and from the open door:

    $${\forall}d^o. {\forall}d^p. (O(d^o) {\rightarrow}P(d^p) {\rightarrow}{\exists}d. (d \neq d^o \wedge d \neq d^p \wedge {\Diamond}_{{s}}^1 P(d) ) )$$

-   **Axiom 9:** When the player does the *no switch* (${\bar{s}}$) action, the newly picked door is the same as the previously picked door: $
    {\forall}d. (P(d) {\rightarrow}{\Diamond}^1_{{\bar{s}}} P(d) ) )  
    $

-   **Axiom 10:** A state is a victorious state if and only if the car is behind the picked door: $
    V \leftrightarrow ({\exists}d. C(d) \wedge P(d))
    $

The next step is the formalization of (the intended meaning of) the question (“Do you want to pick door No. 2? Is it to your advantage to switch your choice?”) as a conjecture. However, this is significantly less straightforward than the formalization of the axioms. A naive and literal reading of the question could result in the following tentative conjecture: $${\mathcal{P}}_{{s}}(V) > {\mathcal{P}}_{{\bar{s}}}(V)$$ But the formula above is only satisfied in models where the probability of victory by switching is greater than the probability of victory by not switching in *all* states, whereas the question is interested in a few states only, namely those reachable by a given sequence of actions (i.e. hiding, picking, opening and re-picking). Taking this into account, an apparently plausible alternative formalization could be: $$@_{s_0} {\Box}_{{h}} {\Box}_{{p}(d_1)} {\Box}_{{o}} ({\mathcal{P}}_{{s}}(V) > {\mathcal{P}}_{{\bar{s}}}(V))$$ But this is trivially false in any model $M$ that satisfies the axioms above, because the action $\mathit{hide}$ has a successor state $s_1$ (where the car was hidden behind the first door) such that: $$M \vDash @_{s_1} {\Box}_{{p}(d_1)} {\Box}_{{o}} ({\mathcal{P}}_{{s}}(V) < {\mathcal{P}}_{{\bar{s}}}(V))$$ Yet another possible attempt would be to formalize the conjecture as: $$\forall s. \varphi(s) {\rightarrow}@_s {\mathcal{P}}_{{s}}(V) > {\mathcal{P}}_{{\bar{s}}}(V)$$ where $s$ is the current state when the question is asked and $\varphi(s)$ is a formula specifying whether $s$ is a posible current state (i.e. consistent with the player’s observations). However, for a similar reason, this formula is also false in any model $M$ that satisfies the axioms: there is a possible current state $s^*$, where $I_{s^*}({\mathcal{P}}_{{s}}(V)) = 0$ and $I_{s^*}({\mathcal{P}}_{{\bar{s}}}(V)) = 1$. In fact, it is easy to see that, in any possible current state $s$, $I_{s^*}({\mathcal{P}}_{{\bar{s}}}(V))$ and $I_{s^*}({\mathcal{P}}_{{s}}(V))$ are always either $0$ and $1$, because the action of switching has always only one possible outcome.

As evidenced by the failed conjectures above, there is a structural gap between the natural language question and the correct formalization of its intended meaning, and therein lies a potential reason (though probably not the only one) why people tend to have difficulties to reason about the Monty Hall problem. As it is posed, the question induces the player to think in terms of probabilistic outcomes of the action of switching or not switching in the current state. In contrast, the correct thinking requires the player to hypothetically backtrack to the initial state and formulate the conjecture as follows:

-   **Conjecture:** $
    @_{s_0}
    ({\mathcal{P}}_{{h}{::}{p}(d_1) {::}{o}{::}{s}{::}{\texttt{nil}}}(V) 
    > 
    {\mathcal{P}}_{{h}{::}{p}(d_1) {::}{o}{::}{\bar{s}}{::}{\texttt{nil}}}(V))
    $

In any model satisfying the axioms (including the omitted axioms), $I_{s_0}({\mathcal{P}}_{{h}{::}{p}(d_1) {::}{o}{::}{s}{::}{\texttt{nil}}}(V)) = 2/3$ and $I_{s_0}({\mathcal{P}}_{{h}{::}{p}(d_1) {::}{o}{::}{\bar{s}}{::}{\texttt{nil}}}(V)) = 1/3$. Therefore, the conjecture is a theorem[^1].

Related Work {#sec:RelatedWork}
============

Many probabilistic logics are surveyed in [@SEP]. Among those logics, most depart from classical logic by adopting a probabilistic notion of validity and entailment. [**PTL**]{}, on the other hand, remains strictly classical in this respect. The probabilistic modal logics described in Sections 4.1 and 4.2 of [@SEP] are probably the most similar to [**PTL**]{}. However, they are propositional, lack the probabilistic diamond operator, and are atemporal.

Probabilistic logics that incorporate time include **PCTL** [@PCTLOriginal; @PCTL], which extends **CTL** by replacing the existential and universal path quantifiers by a probabilistic operator. **PCTL** is an excellent logic for *model checking* Markov chains. However, its lack of a probabilistic diamond operator makes it susceptible to the issues discussed in Section \[sec:Disambiguation\], thereby limiting its use beyond model checking. They also lack an explicit handling of actions, which is necessary for a convenient formalization of the Monty Hall problem and other examples discussed here. On the other hand, **PCTL**’s temporal modalities (which include, for instance, the *until* operator) are more sophisticated than [**PTL**]{}’s temporal modalities (which can only make statements about the *next* moment in time). [**PTL**]{}’s parsimony is intentional: it includes only the minimal set of temporal modalities needed to capture the desired notion of probability. Nevertheless, in practical applications where other temporal modalities are needed, they could be easily added to [**PTL**]{}as well.

Conclusion and Future Work {#sec:Conclusion}
==========================

The large number of available probabilistic logics indicates that conciliating logic and probability is a non-trivial task. The expressive probabilistic temporal logic [**PTL**]{}described here provides a novel alternative approach, based on the simple intuition that the notion of probability can only be fully grasped in combination with the notions of action and time. The complex interaction of time, action and probability naturally leads to a modal and higher-order logic. [**PTL**]{}is adequate with respect to classical probability theory, of which it can be considered an extension (as shown in Section \[sec:Adequacy\], where a correspondence between events and formulas has been established in detail). [**PTL**]{}’s convenient expressive power allowed a natural formalization of the famous Monty Hall problem. One of the main insights in the development of [**PTL**]{}came with the discovery of the need for both a higher-order probability function and a probabilistic diamond operator, as discussed in Section \[sec:Disambiguation\]. Besides the higher order, the satisfaction of this need is a distinguishing feature of [**PTL**]{}.

In the near future, the implementation of [**PTL**]{}in `Coq` needs to be made more user-friendly, through the implementation of tactics that automate and hide technical details for users. On the philosophical side, it would be interesting to extend [**PTL**]{}with past temporal modalities, since we often need to reason about actions that have happened in the past but whose outcomes we have not yet observed, and to define conditional probabilities, in order to explore the question about the relationship between probabilities of conditionals (e.g. $P(A{\rightarrow}B)$) and conditional probabilities (e.g. $P(B|A)$) [@HajekProbabilities] from [**PTL**]{}’s perspective.

[^1]: An interactive proof of this theorem using the embedding of [**PTL**]{}in `Coq` is freely available in the online repository of the implementation discussed in Section \[sec:Implementation\]. For the sake of simplicity, this formalization of the Monty Hall problem does not concern itself with specifying in which states each action is allowed or disallowed. But this could also be done.
