PrSAT Tutorial (Mathematica Notebook)

June 16, 2011

First, load in the PrSAT package

See my PrSAT website for instructions on downloading and installing PrSAT (assuming you have Mathematica installed).

<<PrSAT`

Example #1

The first example of a probability model that we saw was the following:

MODEL1 = PrSAT[{Pr[X∧Y]==(1/6),Pr[X∧¬Y]==(1/4),Pr[¬X∧Y]==(1/8),Pr[¬X∧¬Y]==(11/24)}]

PrSAT will show us an STT representation of MODEL1:

TruthTable[MODEL1]

We can use PrSAT to calculate probability, using MODEL1:

EvaluateProbability[{Pr[X∨Y],Pr[X],Pr[Y]},MODEL1]

We can also check arbitrary claims to see if they are true on MODEL1:

EvaluateProbability[Pr[X|Y]>Pr[X],MODEL1]

Example #2

The second example we saw was an algebraic proof of the following theorem:

Pr(X∨Y)==Pr(X)+Pr(Y)-Pr(X∧Y)

PrSAT easily verifies this theorem (note: it does not present a readable proof).

PrSAT[{Pr[X∨Y]≠Pr[X]+Pr[Y]-Pr[X∧Y]}]

This output means there are no probability models on which Pr[X ∨ Y] ≠ Pr[X] + Pr[Y] - Pr[X ∧ Y].  That "proves" that the above statement is a theorem of probability calculus.

Example #3

The second example we saw was an algebraic proof of the following theorem:

Pr(X)==Pr(X∧Y)+Pr(X∧¬Y)

PrSAT easily verifies this theorem (note: it does not present a readable proof).

PrSAT[{Pr[X]≠Pr[X∧Y]+Pr[X∧¬Y]}]

This output means there are no probability models on which Pr[X] ≠ Pr[X ∧ Y] + Pr[X ∧ ¬ Y].  That "proves" that the above statement is a theorem of probability calculus.

Example #4

The next example involves the following theorem:

Pr(X→Y)≥Pr(Y | X)

PrSAT easily verifies this theorem (note: it does not present a readable proof).  First, we need to define the conditional operator.

X_→Y_:=¬X∨Y;

PrSAT[{Pr[X→Y]<Pr[Y|X]}]

This output means there are no probability models on which Pr[X → Y] ≥ Pr[Y | X].  That "proves" that the above statement is a theorem of probability calculus.

Example #5

The next example involves the following theorem:

d(X,Y)=d(X∨Y,Y)+d(X∨¬Y,Y), where d(X,Y)= Pr(X|Y)-Pr(X).

PrSAT easily verifies this theorem (note: it does not present a readable proof).  First, we need to define d(X, Y).

d[X_,Y_]:=Pr[X|Y]-Pr[X];

PrSAT[{d[X,Y]≠d[X∨Y,Y]+d[X∨¬Y,Y]}]

This output means there are no probability models on which d[X, Y] ≠ d[X ∨ Y, Y] + d[X ∨ ¬ Y, Y].  That "proves" that the above statement is a theorem of probability calculus.

Example #6

The next example involves the fact that Pr(X | Y ∨ Z) = Pr(X | Y ∧ Z) is NOT a theorem:

PrSAT easily finds a counter-model to this claim.

PrSAT[{Pr[X|Y∨Z]≠Pr[X|Y∧Z]}]

The model PrSAT finds by defualt is non-regular.  We can force it to find a regular counter-model, as follows:

MODEL2=PrSAT[{Pr[X|Y∨Z]≠Pr[X|Y∧Z]},Probabilities->Regular]

Here is an STT representation of MODEL2:

TruthTable[MODEL2]

We can calculate the values of Pr[X | Y ∧ Z], Pr[X | Y ∨ Z] on this model as follows:

EvaluateProbability[{Pr[X|Y∧Z],Pr[X|Y∨Z]},MODEL2]

We can look at decimal representations of these exact real numbers, as follows:

%//N

We gave a different model in the lecture notes.  We can enter that model in by hand, and then verify it has the desired properties, as follows:

MODEL3=PrSAT[{Pr[X∧Y∧Z]==(1/6),Pr[X∧Y∧¬Z]==(1/6),Pr[X∧¬Y∧Z]==(1/4),Pr[X∧¬Y∧¬Z]==(1/16),Pr[¬X∧Y∧Z]==(1/6),Pr[¬X∧Y∧¬Z]==(1/12),Pr[¬X∧¬Y∧Z]==(1/24),Pr[¬X∧¬Y∧¬Z]==(1/16)}]

TruthTable[MODEL3]

EvaluateProbability[{Pr[X|Y∧Z],Pr[X|Y∨Z]},MODEL3]

We can also see the algebraic form of an expression, as follows:

AlgebraicForm[Pr[X|Y∧Z]==Pr[X|Y∨Z],{X,Y,Z}]

Note that PrSAT uses different conventions (i.e., a different ordering in the truth-table) for the (Subscript[𝕒, i]) than I use in the lecture notes.

Here is a verfifcation of some of our independence theorems:

PrSAT[{
Pr[P∧Q]==Pr[P] Pr[Q],
Pr[P|Q]≠Pr[P] ,
}]

PrSAT[{
Pr[P∧¬Q]==Pr[P] Pr[¬Q],
Pr[P∧Q]≠Pr[P] Pr[Q]
}]

PrSAT[{
Pr[P∧Q]==Pr[P] Pr[Q],
Pr[P∧¬Q]≠Pr[P] Pr[¬Q]
}]

Here is a (regular) model showing that pairwise independence does not entail mutual independence (for a set of 3 events)

PrSAT[{
Pr[X∧Y]==Pr[X] Pr[Y],
Pr[X∧Z]==Pr[X] Pr[Z],
Pr[Y∧Z]==Pr[Y] Pr[Z],
Pr[(X∧Y)∧Z]≠Pr[X∧Y] Pr[Z],
Pr[X]==Pr[Y]==Pr[Z]==1/2
},Probabilities->Regular]

TruthTable[%]

Here is a (regular) model showing that independence is not transitive:

PrSAT[{
Pr[X∧Y]==Pr[X] Pr[Y],
Pr[Y∧Z]==Pr[Y] Pr[Z],
Pr[X∧Z]≠Pr[X] Pr[Z],
Pr[X]==Pr[Y]==Pr[Z]==1/2
},Probabilities->Regular]

TruthTable[%]

Extra Example (not from my lecture #1 notes):  Here's an example of a set of constraints that are satisfiable but only on probability models containing irrational numbers

PrSAT[{Pr[Y|X]==Pr[Y∨X],Pr[X∧Y]==(1/4),Pr[¬X∧Y]==(1/4)}]

TruthTable[%]

Can you prove that this is the only model for this set of constraints?

The first numerical probability model appearing in the lecture notes

MODEL1=PrSAT[{
Pr[X∧Y]==(1/6),
Pr[X∧¬Y]==(1/4),
Pr[¬X∧Y]==(1/8)
}]

TruthTable[MODEL1]

Using PrSAT to translate probabilistic expressions into algebraic ones

AlgebraicForm[Pr[¬X∨Y]<Pr[Y|X],{X,Y}]

DenialOfTheorem=AlgebraicForm[Pr[¬X∨Y]<Pr[Y|X],{X,Y}]

We can then use Mathematica's decision procedure for real algebra (FindInstance) to refute this claim, assuming that the underlying variables are constrained so as to constitute a probability model:

FindInstance[DenialOfTheorem&&(Subscript[𝕒, 1])+(Subscript[𝕒, 2])+(Subscript[𝕒, 3])+(Subscript[𝕒, 4])==1&&0≤(Subscript[𝕒, 1])≤1&&0≤(Subscript[𝕒, 2])≤1&&0≤(Subscript[𝕒, 3])≤1&&0≤(Subscript[𝕒, 4])≤1,{(Subscript[𝕒, 1]),(Subscript[𝕒, 2]),(Subscript[𝕒, 3]),(Subscript[𝕒, 4])}]

Using PrSAT to find a model on which Pr(X | Y ∧ Z) ≠ Pr(X | Y ∨ Z)

MODEL2=PrSAT[{
Pr[X|Y∧Z]≠Pr[X|Y∨Z]
},
Probabilities->Regular,BypassSearch->True]

TruthTable[MODEL2]

EvaluateProbability[{Pr[X|Y∧Z],Pr[X|Y∨Z]},MODEL2]

Using PrSAT to show the ordinal non-equivalence of {𝒹, 𝓇, ℓ, 𝓈}

𝒹[ℍ_,𝔼_]:=Pr[ℍ | 𝔼]-Pr[ℍ];
𝓇[ℍ_,𝔼_]:=((Pr[ℍ | 𝔼]-Pr[ℍ])/(Pr[ℍ | 𝔼]+Pr[ℍ]));
ℓ[ℍ_,𝔼_]:=((Pr[𝔼 | ℍ]-Pr[𝔼 | ¬ℍ])/(Pr[𝔼 | ℍ]+Pr[𝔼 | ¬ℍ]));
𝓈[ℍ_,𝔼_]:=Pr[ℍ | 𝔼]-Pr[ℍ|¬𝔼];

J[ℍ_,𝔼_]:=(1/(Pr[ ¬ℍ |𝔼]))-(1/(Pr[ ¬ℍ]));

A model showing that 𝒹 and 𝓇 are not ordinally equivalent:

MODEL3=PrSAT[{
𝒹[(Subscript[ℍ, 1]),(Subscript[𝔼, 1])]≥𝒹[(Subscript[ℍ, 2]),(Subscript[𝔼, 2])],
𝓇[(Subscript[ℍ, 1]),(Subscript[𝔼, 1])]<𝓇[(Subscript[ℍ, 2]),(Subscript[𝔼, 2])]
},
Probabilities->Regular]

TruthTable[MODEL3]

EvaluateProbability[{{𝒹[(Subscript[ℍ, 1]),(Subscript[𝔼, 1])],𝒹[(Subscript[ℍ, 2]),(Subscript[𝔼, 2])]},
{𝓇[(Subscript[ℍ, 1]),(Subscript[𝔼, 1])],𝓇[(Subscript[ℍ, 2]),(Subscript[𝔼, 2])]}},MODEL3]//N

A model showing that 𝒹 and ℓ are not ordinally equivalent:

MODEL4=PrSAT[{
𝒹[(Subscript[ℍ, 1]),(Subscript[𝔼, 1])]≥𝒹[(Subscript[ℍ, 2]),(Subscript[𝔼, 2])],
ℓ[(Subscript[ℍ, 1]),(Subscript[𝔼, 1])]<ℓ[(Subscript[ℍ, 2]),(Subscript[𝔼, 2])]
},
Probabilities->Regular]

I leave the remaining pairs as exercises.

Selection of Properties (1)-(8)

Verification that 𝓇 satisfies commutativity (4):

PrSAT[{

𝓇[ℍ,𝔼]≠𝓇[𝔼,ℍ]

},BypassSearch->True]

Model showing that 𝓈 violates (4):

MODEL5=PrSAT[{

Pr[ℍ|𝔼]>Pr[ℍ],
𝓈[ℍ,𝔼]≠𝓈[𝔼,ℍ]

},Probabilities->Regular]

TruthTable[MODEL5]

EvaluateProbability[{𝓈[ℍ,𝔼],𝓈[𝔼,ℍ]},MODEL5]//N

Model showing that ℓ violates the so-called "Law of Likelihood" (2):

MODEL6=PrSAT[{

Pr[𝔼|ℍ1]>Pr[𝔼|ℍ2],
ℓ[ℍ1,𝔼]<ℓ[ℍ2,𝔼]

},Probabilities->Regular]

Model showing that 𝓈 violates (3) — people were very surprised when I reported this one:

MODEL7=PrSAT[{

Pr[ℍ|𝔼1]>Pr[ℍ|𝔼2],
𝓈[ℍ,𝔼1]<𝓈[ℍ,𝔼2]

},Probabilities->Regular]

EvaluateProbability[{Pr[ℍ|𝔼1],Pr[ℍ|𝔼2],𝓈[ℍ,𝔼1],𝓈[ℍ,𝔼2]},MODEL7]//N

Here is a bizarre measure ℽ, which satisfies (ℛ), but violates (8).  This was discovered by Crupi et al.  See their paper: "Towards a Grammar of Bayesian Confirmation", which can be downloaded from my Mathcamp webpage http://fitelson.org/mathcamp/

ℽ[ℍ_,𝔼_]:=((Pr[ℍ|𝔼])^2)-((Pr[ℍ])^2);

This model shows that ℽ violates (8):

MODEL8=PrSAT[{

Pr[𝔼|ℍ1]>Pr[𝔼|ℍ2],
Pr[𝔼|¬ℍ1]==Pr[𝔼|¬ℍ2],
ℽ[ℍ1,𝔼]<ℽ[ℍ2,𝔼]

},SearchAttempts->10,Probabilities->Regular]

PrSAT[{

Pr[𝔼|ℍ1]>Pr[𝔼|ℍ2],
Pr[𝔼|¬ℍ1]<Pr[𝔼|¬ℍ2],
J[ℍ1,𝔼]<J[ℍ2,𝔼],
Pr[ℍ1]==2Pr[ℍ2]

},SearchAttempts->10,Probabilities->Regular]

We can verify that  ℽ satisfies (ℛ), as follows:

PrSAT[{

Pr[ℍ|𝔼]>Pr[ℍ]&&ℽ[ℍ,𝔼]≤0||Pr[ℍ|𝔼]==Pr[ℍ]&&ℽ[ℍ,𝔼]≠0||Pr[ℍ|𝔼]<Pr[ℍ]&&ℽ[ℍ,𝔼]≥0

},BypassSearch->True]

My Hint about exercise (ii)

FullSimplify[((x-y)/(x+y))==Tanh[(1/2) Log[(x/y)]]]

Both tanh and log are increasing functions.  And, increasing functions preserve order.

Best Probability Bounds

PrSAT has a built-in function PrRange for computing best possible bounds on a probability expression, subject to (arbitrary) numerical constriants.  Here are some examples:

Modus ponens:

PrRange[Pr[B],Pr[B|A]==(1/2)&&Pr[A]==(1/3)]

Constraints don’t have to be equalities:

PrRange[Pr[B],Pr[B|A]<(1/4)&&Pr[A]>(1/3)]

Modus tollens:

PrRange[Pr[¬A],Pr[B|A]==(1/4)&&Pr[¬B]==(1/3)]

Denying the antecedent:

PrRange[Pr[¬B],Pr[B|A]==(1/4)&&Pr[¬A]==(1/3)]

We can also solve analytically for general symbolic best possible bounds.  Here are the bounds for modus ponens:

MPCons=AlgebraicForm[Pr[B|A]==x&&Pr[A]==y,{A,B}]

PrB=AlgebraicForm[Pr[B],{A,B}]

BackCons=0<(Subscript[𝕒, 2])<1&&0<(Subscript[𝕒, 3])<1&&0<(Subscript[𝕒, 4])<1&&(Subscript[𝕒, 2])+(Subscript[𝕒, 3])+(Subscript[𝕒, 4])≤1;

MPMax=Maximize[{PrB,MPCons&&BackCons},{(Subscript[𝕒, 2]),(Subscript[𝕒, 3]),(Subscript[𝕒, 4])},Reals][[1]]

FullSimplify[MPMax,0<y<1&&0<x<1]

MPMin=Minimize[{PrB,MPCons&&BackCons},{(Subscript[𝕒, 2]),(Subscript[𝕒, 3]),(Subscript[𝕒, 4])},Reals][[1]]

FullSimplify[MPMin,0<y<1&&0<x<1]

And, here are the bounds for modus tollens:

MTCons=AlgebraicForm[Pr[B|A]==x&&Pr[¬B]==y,{A,B}]

PrNotA=AlgebraicForm[Pr[¬A],{A,B}]

MTMax=Maximize[{PrNotA,MTCons&&BackCons},{(Subscript[𝕒, 2]),(Subscript[𝕒, 3]),(Subscript[𝕒, 4])},Reals][[1]]

FullSimplify[MTMax,0<y<1&&0<x<1]

MTMin=Minimize[{PrNotA,MTCons&&BackCons},{(Subscript[𝕒, 2]),(Subscript[𝕒, 3]),(Subscript[𝕒, 4])},Reals][[1]]

FullSimplify[MTMin,0<y<1&&0<x<1]

FullSimplify[MTMin,0<y<1&&0<x<1&&x+y≤1]

FullSimplify[MTMin,0<y<1&&0<x<1&&x+y>1]