An Expressive Probabilistic Temporal Logic

arXiv:1603.07453v2 [cs.LO] 8 Oct 2017

Bruno Woltzenlogel Paleo
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.
Keywords: Higher-Order Modal Logics, Probability Theory

1

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 [9]. 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 [10].
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

2

An Expressive Probabilistic Temporal Logic

(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 2) and the semantics (in Section 3)
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 4), and its greater expressiveness allows us
to reason explicitly about event independence (as discussed in Section 5.1) and
to avoid typical ambiguities of natural language discourse about probabilities
(as shown in Section 5.2). 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 8). PTL’s convenience and expressive power are
illustrated through the formalization of the Monty Hall problem (in Section 7).

2

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.
Definition 2.1 Types are freely generated from the set of basic types
{β, ι, η, µ}, the right-associative function type constructor → and the list type
constructor list. µ is the type for states, β is the type for booleans, ι is the type
for objects and η 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 µ → β
and the type of actions α is defined to be an abbreviation for µ → list[µ].
Remark 2.2 The definition of o ensures that the truth of a proposition depends on states. The definition of α 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 2.3, 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 (✷ and ✸) implicitly bind states, they
have a more fundamental role, which reminds that of the λ binder. Therefore,
they are treated separately in Definition 2.4.

Woltzenlogel Paleo

3

Definition 2.3 For every type τ , Sτ is a countably infinite set of uninterpreted symbols of type τ . The set of arithmetic function symbols SAF
is the set {0η , 1η , +η→η→η , ∗η→η→η }. The set of arithmetic relation symbols SAR is {=η→η→o , <η→η→o }. The set of propositional logical symbols
SL is {⊤o , ⊥o , ∨o→o→o , ∧o→o→o , →o→o→o , ↔o→o→o , ¬o→o }. The set of hybrid
of quantifiers SQ is
S logical symbols SH is {@µ→o→o , inµ→o }. The set
τ
τ
τ ∈T {∀(τ →o)→o , ∃(τ →o)→o , =o→o→o }. The symbol nil has type list[τ ], ::
τ
has type τ → list[τ ] → list[τ ], ∈ has type τ → list[τ ] → o and
the length operator |.|τ has type list[τ ] → µ. The probability operator
P has type list[α] → o → η. SThe set of all symbols S is defined as
Sτ ∪ SAF ∪ SAR ∪ SL ∪ SH ∪ SQ ∪ τ ∈T {nilτ , ::τ , |.|τ , ∈τ } ∪ {P}.
Expressions are constructed as in the lambda calculus, using the symbols
from S, application, abstraction and modalities.
Definition 2.4 Expressions are constructed according to the following rules:
•

if sτ ∈ S, then sτ is an expression of type τ .

•

if t1 is an expression of type τ → τ ′ and t2 is an expression of type τ , then
(t1 t2 ) is an expression of type τ ′ .

•

if xτ ∈ Sτ and t is an expression of type τ ′ , then λxτ .t is an expression of
type τ → τ ′ .

•

if ϕ is an expression of type o, p is an expression of type η and a is an
expression of type α, then ✸pa ϕ are ✷a ϕ expressions of type o.

Formulas are expressions of type o. Actions S
are expressions of type α. The set
of expressions of type τ is denoted Eτ . L = τ ∈T Eτ .

Remark 2.5 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:
•

✸a ϕ ≡ ∃xη .✸xa ϕ

•

Pl (ϕ) ≡ ((P l) ϕ)

•

∀x : G. H(x) ≡ ∀x. G(x) → H(x)

•

∃x : G. H(x) ≡ ∃x. G(x) ∧ H(x)

•

∀xτ ∈ ℓlist[τ ] . H(x) ≡ ∀x. (x ∈ ℓ) → H(x)

•

∃xτ ∈ ℓlist[τ ] . H(x) ≡ ∃x. (x ∈ ℓ) ∧ H(x)

•

Pa::l (ϕ :: L) ≡ Pa::l (ϕ) ∧ Pl (L) (with Pnil (nil) ≡ ⊤)

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 P, which takes a list of actions and a proposition as arguments

4

An Expressive Probabilistic Temporal Logic

and returns the probability that the proposition will hold after the execution
of the listed actions.
Example 2.6 The following are some simple examples of probabilistic statements and their corresponding formalizations in PTL:
(i) Tossing a coin has a transition with probability 0.5 to a state where the
coin shows heads: ∀x : Coin.✸0.5
toss(x) heads(x)
(ii) The probability of a coin showing heads after it is tossed is 0.5:
∀x : Coin.Ptoss(x)::nil (heads(x)) = 0.5
(iii) The probability of a coin showing heads twice after it is tossed twice is
less than 0.5: ∀x : Coin .Pt(x)::t(x)::nil (h(x) :: h(x) :: nil) < 0.5 , where
t = toss and h = heads.
(iv) After a coin is tossed it is necessarily either heads or tails:
∀x : Coin.✷toss (x) (heads (x) ∨ tails(x))
(v) After a coin is tossed it is possibly tails: ∀x : Coin .✸toss(x) (tails(x))

3

Semantics

For each type τ , we need a domain Dτ of elements on which expressions of
type τ 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.
Definition 3.1 A domain Dτ for a type τ is a non-empty set such that Dτ ′ →τ
is the set of all functions from Dτ ′ to Dτ (for every τ ′ and τ ), Do = {T, F},
Dη = R and Dlist[τ ] is the set of all lists of elements from Dτ .
As in the most common modal logics [3], 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.
Definition 3.2 A probabilistic labeled frame is a triple (W, R, P ) such that W
is a non-empty set of states, R ⊆ W × W × Dα satisfying the condition that if
(w, w′ , ℓ) ∈ R then (w, w′′ , ℓ) ∈ R for every w′′ ∈ ℓ(w), and P : R → [0, 1] is
a probability function satisfying the condition that for all w ∈ W and for all
ℓ ∈ Dα such that there exists w′ ∈ W with (w, w′ , ℓ) ∈ R,
X
P ((w, w′ , ℓ)) = 1
w ′ | (w,w ′ ,ℓ)∈R

Remark 3.3 The relation R in definition 3.2 may be cyclic. This is convenient,
for instance, when specifying Markov chains.

Woltzenlogel Paleo

5

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 [6]. In the examples considered in this paper, boolean expressions and
probabilistic expressions are always flexibly interpreted, whereas other expressions are always rigidly interpreted.
Definition 3.4 A model is a tuple (W, R, P, {Dτ }τ ∈T , I) where (W, R, P ) is a
probabilistic labelled frame, {Dτ }τ ∈T is a domain, W = Dµ and I is an interpretation function that maps states and expressions of any type τ to elements in
Dτ . 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):
•

Iw (A ∧ B) = T iff Iw (A) = T and Iw (B) = T

•

Iw (A ∨ B) = T iff Iw (A) = T or Iw (B) = T

•

Iw (A → B) = T iff Iw (A) = F or Iw (B) = T

•

Iw (¬A) = T iff Iw (A) = F

•

Iw (∀xτ .ϕ) = T iff Iw [x 7→ e](ϕ) = T for every e ∈ Dτ

•

Iw (∃xτ .ϕ) = T iff Iw [x 7→ e](ϕ) = T for some e ∈ Dτ

•

Iw ((t1 t2 )) = (Iw (t1 ) Iw (t2 ))

•

Iw (λxτ .t) is the function taking an element e ∈ Dτ and returning Iw [x 7→ e](t).

•

Iw (in(s)) = T iff w = Iw (s)

•

Iw (@s ϕ) = T iff IIw (s) (ϕ) = T

where Iw [x 7→ e](x) = e and Iw [x 7→ 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:
•

Iw (✷a ϕ) = T iff Iw′ (ϕ) = T
for every w′ such that (w, w′ , Iw (a)) ∈ R

•

Iw (✸pa ϕ) = T iff P ((w, w′ , Iw (a))) = Iw (p) and Iw′ (ϕ) = T
for some w′ such that (w, w′ , Iw (a)) ∈ R
(
1, if Iw (ϕ) = T
Iw (Pnil (ϕ)) =
0, if Iw (ϕ) = F
P
Iw (Pa::l (ϕ)) =
P ((w, w′ , Iw (a))).Iw′ (Pl (ϕ))

•

•

w′ |(w,w′ ,Iw (a))∈R

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.
Definition 3.5 A formula ϕ is satisfied in a model M ≡ (W, R, P, {Dτ }τ ∈T , I)
in a state w, denoted M, w  ϕ iff Iw (ϕ) = T. A formula ϕ is globally satisfied
in a model M , denoted M  ϕ iff M, w  ϕ for all w ∈ W . A formula ϕ is valid,
denoted  ϕ iff M  ϕ for every model M . A set of formulas T entails
V a formula
ϕ, denoted T  ϕ, iff M  ϕ for every model M such that M  G∈T G.

6

An Expressive Probabilistic Temporal Logic

4

Adequacy

This section shows how the usual mathematical presentation of probability
theory, as recalled in Definition 4.4, can be considered a special case of the
probabilistic logic presented here. This is done by showing (in Theorem 4.5)
how to translate probability spaces into models and the usual set-theoretic
language for probabilistic events into PTL’s language.
Definition 4.1 Set expressions over a set Ω are expressions freely generated
from singleton subsets of Ω and operators for complementation ( ), union (∪)
and intersection (∩).
Remark 4.2 As usual, by abuse of notation, set expressions and the sets they
denote are not explicitly distinguished.
Example 4.3 If Ω = {w1 , w2 } then the following are examples of set expressions: {w1 }, {w2 }, {w2 } (denoting the set {w1 }), {w1 } ∪ {w2 } (denoting the
set {w1 , w2 }), {w1 } ∩ {w2 } (denoting the empty set), . . .
Definition 4.4 A probability space is a triple (Ω, Σ, Q) where Ω is the sample
space (whose elements are outcomes), Σ is a σ-algebra on Ω (i.e. a collection
of subsets of Ω (events) closed under complementation, countable union and
countable intersection) and Q : Σ → [0, 1] is a probability function satisfying
Kolmogorov’s axioms:
(i) Q(E) ≥ 0, for all E ∈ Σ
(ii) Q(Ω) = 1
(iii) For any countable collection C of mutually disjoint events
Q(

[

E∈C

E) =

X

Q(E)

E∈C

Theorem 4.5 For every probability space (Ω, Σ, Q), there is a model M and
a language translation function g from set expressions over Ω to formulas such
that Q(E) = p iff M, w  Pa (g(E)) = p, for some w and some a.
Proof. Let W be {w} ∪ Ω. For each wk ∈ Ω, let Fk be a distinct atomic
proposition. Let I be any interpretation such that Iwi (Fj ) = T iff i = j. Let
R be {(w, wk , Iw (a))|wk ∈ Ω}. Let the probabilistic transition
function be
S
defined such that P ((w, wk , Iw (a))) = Q({wk }). Since Ω = k {wk }, all {wk }
are mutually disjoint and Q(Ω) = 1, the condition (from Definition 3.2) that
X

P ((w, wk , Iw (a))) = 1

wk | (w,wk ,Iw (a))∈R

holds. Finally let M be the model (W, R, P, {Dτ }τ ∈T , I). The translation

Woltzenlogel Paleo

function g is defined recursively:

Fk ,




g(E ′ ) ∨ g(E ′′ ),
g(E) =

g(E ′ ) ∧ g(E ′′ ),



¬g(E ′ ),

if
if
if
if

7

E
E
E
E

= {wk }
= E ′ ∪ E ′′
= E ′ ∩ E ′′
= E′

Now the fact that Q(E) = p iff M, w  Pa (g(E)) = p must be proven. First
notice that, by Definition 3.5, M, w  Pa (g(E)) = p iff Iw (Pa (g(E)) = p), and
by Definition 3.4, Iw (Pa (g(E)) = p) iff
X
P ((w, w′ , Iw (a))).Iw′ (Pnil (g(E))) = p
w ′ | (w,w ′ ,Iw (a))∈R

By Definition 3.4 again and the definition of R, the summation above can be
simplified, resulting in the following equation:
X
P ((w, w′ , Iw (a))) = p
w ′ |w ′ ∈Ω and Iw′ (g(E))=T}

Furthermore, unfolding the definition of P , the equation above reduces to:
X
Q({w′ }) = p
w ′ |w ′ ∈Ω and Iw′ (g(E))=T}

Therefore, it suffices to prove that the equation above holds iff Q(E) = p, or
equivalently, that:
X
Q({w′ }) = Q(E)
w ′ |w ′ ∈Ω and Iw′ (g(E))=T}

P
By Kolmogorov’s third axiom, Q(E) = w′ ∈E Q({w′ }. Hence, letting X be
the following set:
{x|x ∈ Ω and Ix (g(E)) = 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 = {wk }): then g(Ek ) = Fk and, by definition of I, Ix (Fk ) = T
iff x = wk .

•

Induction cases:
· (E = E ′ ): then g(E) = ¬g(E ′ ) and hence:
X = {x|x ∈ Ω and not Ix (g(E ′ )) = T}
Let
Y = {x|x ∈ Ω and Ix (g(E ′ )) = T}
By induction hypothesis, Y = E ′ . Therefore, X = Ω \ Y = Ω \ E ′ = E.

8

An Expressive Probabilistic Temporal Logic

· (E = E ′ ∩ E ′′ ): then g(E) = g(E ′ ) ∧ g(E ′′ ) and hence:
X = {x|x ∈ Ω and Ix (g(E ′ ) ∧ g(E ′′ )) = T}
and so:
X = {x|x ∈ Ω and Ix (g(E ′ )) = T and Ix (g(E ′′ )) = T}
Let:
Y = {x|x ∈ Ω and Ix (g(E ′ )) = T}
Z = {x|x ∈ Ω and Ix (g(E ′′ )) = T}
By induction hypothesis, Y = E ′ and Z = E ′′ . Therefore, X = Y ∩ Z =
E ′ ∩ E ′′ = E.
· (E = E ′ ∪ E ′′ ): this case is analogous to the case above.
✷
Informally, the idea of the proof of Theorem 4.5 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.

5

Expressiveness

A corollary of Theorem 4.5 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 4.5 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.
5.1 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
{h1 h2 , h1 t2 , t1 h2 , t1 t2 }. Saying that, for instance, P ({h1 h2 }) = P (H1 ∩ H2 ) =

Woltzenlogel Paleo

9

P (H1 )P (H2 ) = 0.25 (where H1 = {h1 t2 , h1 h2 } and H2 = {h1 h2 , t1 h2 }) requires the assumption of independence for the tosses. Two events E1 and E2
are often defined to be independent if and only if P (H1 ∩ H2 ) = P (H1 )P (H2 ).
But this definition is epistemologically unsatisfactory. How do we actually
come to know that H1 and H2 are independent? According to this definition,
we must know P (H1 ∩ H2 ) in advance. But that is precisely what, in practice, we do not know and would like to compute (based on our knowledge of
P (H1 ) and P (H2 ))! We can easily get trapped in circular reasoning, trying
to justify, for instance, our claim that P (H1 ∩ H2 ) = 0.25 by saying that H1
and H2 are independent and then trying to justify that they are independent
by saying that P (H1 ∩ H2 ) = 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 ∀x :
0.5
Coin.✸0.5
t(x) .H(x) ∧ ✸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:
0.5
∀x : Coin.✸0.5
t(x) .H(x) ∧ ✸t(x) T (x)  Pt(x)::t(x)::nil (H(x) :: H(x) :: nil) = 0.25

Also dependence can be easily represented. For example, consider a magical
coin cm 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:
•

0.5
@s ✸0.5
t(cm ) .H(cm ) ∧ ✸t(cm ) T (cm )

•

T (cm ) → ✸1t(cm ) .H(cm )

•

H(cm ) → ✸1t(cm ) .T (cm )

•

✷¬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(sb )∧B(sb ); A2: S(sw )∧W (sw ); A3: C(cb )∧B(cb ); A4: C(cw )∧W (cw );
1/|Bag|
G(x).
A5: Bag = sb :: sw :: cb :: cw :: nil; and A6: ∀x ∈ Bag.✸a

10

An Expressive Probabilistic Temporal Logic

It then follows, by the semantics, that:
A1, A2, A3, A4, A5, A6  ∀x ∈ Bag.Pa (S(x) ∧ B(x)) = Pa (S(x)).Pa (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 Pa (S(x) ∧ B(x)) = Pa (S(x)).Pa (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 Tindep of (in)dependence of actions could provide
the following definition for independence of an action a from an action b:
•

Independent (a, b) ≡ (∀s.@s ((∀ϕ.∀p.Pa (ϕ) = p → ✷b (Pa (ϕ) = p)))

It follows from the semantics that Tindep entails the following shortcut theorem:
^

Independent (ai , aj ) → Pa1 ::...::an ::nil (E1 :: . . . :: En :: nil) = Pa1 (E1 ) . . . Pan (En )

1≤i<j≤n

The notion of independence defined in Tindep 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 Tindep or other theories of independence in detail. Tindep 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.
5.2 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 ϕ after a is p”. The
most straightforward and literal logical meaning for this sentence would be
Pa (ϕ) = p. However, it is often the case that the meaning intended by A is
actually ✸pa ϕ. 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 ✸pa ϕ provides fine-grained information about one particular state transition that is made possible by the action, whereas Pa (ϕ) = p
provides coarse-grained aggregated information about transitions to all states
where ϕ 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.

Woltzenlogel Paleo

11

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
✸ and 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 ✸pa ϕ → Pa (ϕ) = p nor Pa (ϕ) = p → ✸pa ϕ is valid. Understanding the difference between ✸pa ϕ and Pa (ϕ) = p is crucial for a correct use
of PTL. Furthermore, the difference in the meanings of ✸ and 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.
Remark 5.1 In natural language dialogues, B tends to cope with the ambiguity by subconsciously attempting to presuppose that ϕ fully specifies a
single outcome of a, in which case A means ✸pa ϕ. 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 Pa (ϕ) = p. Fully understanding the dynamics of presuppositions is an open
linguistic challenge, and probabilities bring yet another dimension of complexity to this difficult problem.
Example 5.2 Consider the following statement:
•

“the probability of picking number n (for 1 ≤ n ≤ 6) is 1/6”

Upon hearing this sentence, we tend to presuppose that there are six outcomes
1/6
(i.e. ✸pick 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 ≤ n ≤ 6) occurs in two distinct faces.”

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

6

Implementation and Automation

A preliminary implementation of PTL in Coq is available in
https://github.com/Paradoxika/ProbLogic.
It follows the embedding
methodology used in [1,2], 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 [1] were rigid, while PTL includes a flexible probability function
P (which is simulated by a flexible predicate in the implementation). Finally,
in contrast to the logics from [1], 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 [2]) and

12

An Expressive Probabilistic Temporal Logic

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 higherorder logic. But even for logics with undecidability issues, automated theorem
provers are occasionaly sufficiently efficient for practical applications [1]. It is
also important to note that, even if arithmetical expressions (of type η) are
restricted to be ground (i.e. by forbidding quantifiers of type (η → o) → 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 ⊤ or ⊥. 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.

7

The Monty Hall Problem

PTL is used here in the formalization of vos Savant’s famous Monty Hall
problem [10], 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 = d1 :: d2 :: d3 :: nil

•

Axiom 2: “behind one door is a car”: ∃d ∈ D.C(d)

•

Axiom 3: “behind the others, goats”: ∀d ∈ D.¬C(d) ↔ 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.”:
∃sc .((@s0 ✸h ✸p(d1 ) ✸o in(sc )) ∧ @sc (O(d3 ) ∧ G(d3 )))

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

Woltzenlogel Paleo

13

which the host hides the car (h), the player picks the first door (p(d1 )), 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 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 pick (p) action, for instance, takes the picked door as
an argument whereas the 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(d3 ). 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 6.
•

Axiom 5: Each door has equal probability of having the car after the hide
1/|D|
(h) action: ∀d ∈ D.✸h
C(d)

•

Axiom 6: The pick (p) action marks the picked door: ∀d ∈ D.✸1p(d) 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:
∀dc .∀dp .(C(dc ) → P (dp ) → ∀d ∈ ((D − dc ) − dp ).✸o1/|((D−d

•

c

)−dp )|

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:
∀do .∀dp .(O(do ) → P (dp ) → ∃d.(d 6= do ∧ d 6= dp ∧ ✸1s P (d)))

•

Axiom 9: When the player does the no switch (s̄) action, the newly picked
door is the same as the previously picked door: ∀d.(P (d) → ✸1s̄ P (d)))

•

Axiom 10: A state is a victorious state if and only if the car is behind the
picked door: V ↔ (∃d.C(d) ∧ 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:
Ps (V ) > Ps̄ (V )

14

An Expressive Probabilistic Temporal Logic

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:
@s0 ✷h ✷p(d1 ) ✷o (Ps (V ) > Ps̄ (V ))
But this is trivially false in any model M that satisfies the axioms above,
because the action hide has a successor state s1 (where the car was hidden
behind the first door) such that:
M  @s1 ✷p(d1 ) ✷o (Ps (V ) < Ps̄ (V ))
Yet another possible attempt would be to formalize the conjecture as:
∀s.ϕ(s) → @s Ps (V ) > Ps̄ (V )
where s is the current state when the question is asked and ϕ(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
Is∗ (Ps (V )) = 0 and Is∗ (Ps̄ (V )) = 1. In fact, it is easy to see that, in any
possible current state s, Is∗ (Ps̄ (V )) and Is∗ (Ps (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: @s0 (Ph::p(d1 )::o::s::nil (V ) > Ph::p(d1 )::o::s̄::nil (V ))

In any model satisfying the axioms (including the omitted axioms),
Is0 (Ph::p(d1 )::o::s::nil (V )) = 2/3 and Is0 (Ph::p(d1 )::o::s̄::nil (V )) = 1/3. Therefore,
the conjecture is a theorem 1 .

8

Related Work

Many probabilistic logics are surveyed in [5]. 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
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 6. 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.

Woltzenlogel Paleo

15

probabilistic modal logics described in Sections 4.1 and 4.2 of [5] 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 [8,4], 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 5.2, 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.

9

Conclusion and Future Work

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 4, 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 5.2. 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 → B)) and conditional probabilities (e.g. P (B|A)) [7] from PTL’s
perspective.

16

An Expressive Probabilistic Temporal Logic

References

[1] Benzmüller, C. and B. W. Paleo, Automating gödel’s ontological proof of god’s existence
with higher-order automated theorem provers, in: ECAI 2014 - 21st European Conference
on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic - Including
Prestigious Applications of Intelligent Systems (PAIS 2014), 2014, pp. 93–98.
URL http://dx.doi.org/10.3233/978-1-61499-419-0-93
[2] Benzmüller, C. and B. W. Paleo, Interacting with modal logics in the coq proof assistant,
in: Computer Science - Theory and Applications - 10th International Computer Science
Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings,
2015, pp. 398–411.
URL http://dx.doi.org/10.1007/978-3-319-20297-6_25
[3] Blackburn, P., M. de Rijke and Y. Venema, “Modal Logic,” Cambridge University Press,
New York, NY, USA, 2001.
[4] Brázdil, T., V. Forejt, J. Kretı́nský and A. Kucera, The satisfiability problem for
probabilistic CTL, in: Proceedings of the Twenty-Third Annual IEEE Symposium on
Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, 2008,
pp. 391–402.
URL http://dx.doi.org/10.1109/LICS.2008.21
[5] Demey, L., B. Kooi and J. Sack, Logic and probability, in: E. N. Zalta, editor, The
Stanford Encyclopedia of Philosophy, 2014, fall 2014 edition .
[6] Fitting, M., “Types, Tableaus, and Gödel’s God,” Kluwer Academic Publishers, 2002.
[7] Hajek, A., “The Conditional Construal of Conditional Probability,” Ph.D. thesis,
Princeton (1993).
URL
http://philosophy.anu.edu.au/sites/default/files/The%20Conditional%20Construal%20of%20Conditional%20Probabi
[8] Hansson, H. and B. Jonsson, A logic for reasoning about time and reliability, Formal
Aspects of Computing 6 (1994), pp. 512–535.
[9] Kolmogorov, A., “Grundbegriffe der Wahrscheinlichkeitsrechnung,” 1933.
[10] vos Savant, M., Ask marilyn, Parade Magazine 16 (1990).

