Examples from "A Decision Procedure for Probability Caluclus with Applications"

Branden Fitelson
Philosophy Department
UC–Berkeley
January 4, 2008

First, load the PrSAT package (freely downloadable from the PrSAT website: http://fitelson.org/PrSAT/).

<<PrSAT`

Example #1: A probability model in which three statements A, B, and C are pariwise independent but not mutually independent

Note: the additional equational side-constraints [Pr[A]==(1/10),Pr[B]==(1/10),Pr[C]==(1/10)] are added here to reduce the number of variables of the problem, so that the model is found much more quickly.  This is a very useful heuristic for speeding-up model searches.  The option Probabilities->Regular guarantees that the model generated is regular (i.e., that it assigns nnonzero probability to all state descriptions of the minimal sentential language required for the expression of the problem given).  Finally, the option BypassSearch->True tells Mathematica to skip Blum's random search add-on, and send the problem straight to the decision procedure.

MODEL1=PrSAT[
{
Pr[A∧B∧C]≠Pr[A] Pr[B] Pr[C],
Pr[A∧B]==Pr[A] Pr[B],
Pr[A∧C]==Pr[A] Pr[C],
Pr[B∧C]==Pr[B]Pr[C],

(* Heuristic -- add additional equational side-constraints *)
Pr[A]==(1/10),Pr[B]==(1/10),Pr[C]==(1/10)
},
Probabilities->Regular,
BypassSearch->True
]

PrSAT also includes a TruthTable function, which allows for the visualization of a model, as a stochastic truth-table:

TruthTable[MODEL1]

If we set BypassSearch->False, then Blum's random-search add-on is consulted first, and a model is (usually) found (relatively) quickly even without any side-constraints!

MODEL11=PrSAT[
{
Pr[A∧B∧C]≠Pr[A] Pr[B] Pr[C],
Pr[A∧B]==Pr[A] Pr[B],
Pr[A∧C]==Pr[A] Pr[C],
Pr[B∧C]==Pr[B]Pr[C]
},
Probabilities->Regular,
BypassSearch->False
]

TruthTable[MODEL11]

We can also Evaluate probabilities on given models, as follows:

EvaluateProbability[{Pr[A|B],Pr[B|A∧¬C]},MODEL11]

%//N

A Simultaneous Countermodel to the s-instances of both (*) and (†)

Again, the additional equational side-constraints [Pr[H]==(1/2),Pr[E1]==(1/4),Pr[E2]==(3/4)] are added to speed the model search, and Probabilities->Regular indicates that we are asking PrSAT to find a regular probability model.

MODEL2=PrSAT[
{
Pr[H | E1] > Pr[H],
Pr[H | E2] > Pr[H],
Pr[H|E1]>Pr[H|E2],
Pr[H | E1] - Pr[H | ¬E1]<Pr[H | E2] - Pr[H | ¬E2],
Pr[H | E1 ∧ E2] - Pr[H | ¬E1∧E2] ==Pr[H | E1] - Pr[H | ¬E1],
Pr[H | E2 ∧ E1] - Pr[H | ¬E2∧E1] ==Pr[H | E2] - Pr[H | ¬E2],
Pr[H | E1 ∧ E2] - Pr[H | ¬(E1∧E2)]<Pr[H | E2] - Pr[H | ¬E2],

(* Heuristic -- add additional equational side-constraints *)
Pr[H]==(1/2),Pr[E1]==(1/4),Pr[E2]==(3/4)
},
Probabilities->Regular,
BypassSearch->True
]

TruthTable[MODEL2]

A Simultaneous Countermodel to two claims concerning Hawthorne & Fitelson's new Bayesian approach to the raven paradox

The following single model shows that neither of the following two claims:

(6)  Pr(H | ~R & ~B) > Pr(H)
(7)  Pr(H | ~R & B) < Pr(H)

follows from the following three claims:

(1) Pr(R | H & B) = 1
(2) Pr(~B) > Pr(R)
(C) Pr(H | R) ≥ Pr(H | ~B)

Here, a regular model is impossible (since one of the contraints requires a zero probability for one of the state descriptions).  But, by adding the constraint Pr[(¬H)∧B∧(¬R)]>0, we can ensure that this is the only zero in the model.  And, as usual, we add equational side-constraints [Pr[H]==(60/100),Pr[R]==(20/100),Pr[B]==(10/100)] to speed the model-finding process by reducing the number of free variables in the problem.

MODEL3=PrSAT[
{
Pr[H∧R∧(¬B)]==0,
Pr[(¬H)∧B∧(¬R)]>0,
Pr[¬B]>Pr[R],
Pr[H|R]==Pr[H|¬B],
Pr[H |(¬R)∧(¬B)]<Pr[H],
Pr[H |B∧(¬R)]>Pr[H]
},
Constraints->{Pr[B]==(1/10),Pr[H]==(1/2),Pr[R]==(1/10)},
BypassSearch->True
]

TruthTable[MODEL3]

We can also solve this one (quickly) with Blum's random search add-on, and with no side-constraints:

PrSAT[
{
Pr[H∧R∧(¬B)]==0,
Pr[(¬H)∧B∧(¬R)]>0,
Pr[¬B]>Pr[R],
Pr[H|R]==Pr[H|¬B],
Pr[H |(¬R)∧(¬B)]<Pr[H],
Pr[H |B∧(¬R)]>Pr[H]
},
BypassSearch->False
]

Theorems and Countermodels from Sobel's "Lotteries and Miracles"

Since Sobel's problems only involve two atomic sentences, no heuristics are needed to yield a fast solution by the decision procedure (and Blum's random search add-on is also not necessary, since the decision procedure is quite fast in such cases).

A PrSAT model showing that Sobel's (1)–(3) do not entail (4)

MODEL4=PrSAT[
{Pr[T]<(1/2),
Pr[T|W]>(1/2),
Pr[W|T]>(1/2),
Pr[T|¬W]>Pr[W]
},
Probabilities->Regular,
BypassSearch->True
]

TruthTable[MODEL4]

A PrSAT model showing that Sobel's (1)–(3) do not entail (5)

MODEL5=PrSAT[
{Pr[T]<(1/2),
Pr[T|W]>(1/2),
Pr[W|T]>(1/2),
Pr[T|W]-Pr[T|¬W]<Pr[¬W]-Pr[W]
},
Probabilities->Regular,
BypassSearch->True
]

TruthTable[MODEL5]

A PrSAT ``Proof'' that Sobel's (1)–(3) do entail the disjunction (4) ∨ (5)

PrSAT[
{Pr[T]<(1/2),
Pr[T|W]>(1/2),
Pr[W|T]>(1/2),
Not[Or[Pr[T|¬W]<Pr[W],Pr[T|W]-Pr[T|¬W]>Pr[¬W]-Pr[W]]]
},
BypassSearch->True
]