Abstract:
We present a propositional logic to reason about the uncertainty of events, where the uncertainty is modeled by a set of probability measures assigning an interval of probability to each event. We give a sound and complete axiomatization for the logic, and show that the satisfiability problem is NP-complete, no harder than satisfiability for propositional logic.

---

Extracted Text

Journal of Artificial Intelligence Research 17 {2002} 57-81Submitted 12/01;
published 8/02
A Logic for Reasoning about UpperProbabilities
 Joseph Y. Halpernhalpern@cs.cornell.edu
 RiccardoPucella riccardo@cs.cornell.edu
Department of Computer Science Cornell University
 Ithaca, NY 14853 http://www.cs.cornell.edu/home/halpern Abstract
 We present a propositional logic to reason about the uncertaintyof events,
where the
 uncertaintyis modeled by a set of probability measuresassigning an interval
of probability to each event. We give asound and complete axiomatization
for the logic, andshow that
 the satisfiability problem is NP-complete, no harder than satisfiability
for propositional
 logic.
 1. Introduction Various measures exist that attemptto quantify uncertainty.
For many trained in the use
 of probability theory, probabilitymeasures are an obvious choice. However,probability
 cannot easiliy capture certain situations of interest. Consider a simpleexample:
suppose
 we have a bagof 100 marbles; we know 30 are red and weknow the remaining
70 are
 eitherblue or yellow, although we do not knowthe exact proportionof blue
and yellow.If
 we are modeling the situation wherewe pick a ball from the bag at random,
weneed to
 assign a probability to threedifferent events: picking up a redball {re
d-event }, picking up a blue ball {blue-event },and picking up a yellow ball
{yel low-event }. We can clearlyassign
 a probability of .3 tore d-event, but there is no clearprobability to assign
to blue-eventor
 yel low-event.
 One way to approach this problem is torepresent the uncertainty using a
set ofproba-
 bility measures, with a probabilitymeasure for each possible proportion
of blueand yellow
 balls. Forinstance, we could use the set of probabilitiesP = f026
 ff : ff 2 [0;:7]g, where
 026 ff
 gives re d-eventprobability :3, blue-eventprobability ff, and yellow-event
probability
 :7 000 ff. To any setof probabilities P we can assign a pairof functions,
the upper and lower probability measure, that for an eventX give the supremum
{respectively, the infimum} of
 theprobability of X according to theprobability measures in P . Thesemeasures
can be
 used to deal withuncertainty in the manner described above, where the lower
and upper probability of an event defines a rangeof probabilityfor that event.
1
 {This example can be viewed as giving a frequentist interpretation of upper
probabilities. Upperprobabilities
 can also be given a subjective interpretation, for example, byconsidering
the odds at which
 someone would be willing to accept or reject a bet {Smith, 1961; Walley
, 1991}.}1. Note that using setsof probability measures is not the only wayto
model this situation. An alternative approach, using inner measures, is studied
by Fagin and Halpern {1991}.
 c
 fl2002 AI Access Foundation and Morgan Kaufmann Publishers.All rights reserved.Halpern
& Pucella Given a measure of uncertainty, one can define a logic for reasoning
about it. Fagin,
 Halpern and Megiddo{1990} {FHM from now on} introduce a logic for reasoning
about
 probabilities,with a possible-worlds semantics that assigns a probabilityto
each possible
 world. Theyprovide an axiomatization for the logic, whichthey prove sound
and complete
 with respect to the semantics. Theyalso show that the satisfiability problem
forthe logic,
 somewhatsurprisingly,is NP-complete, and hence no harder than thesatisfiability
problem
 for propositionallogic. They moreover show how theirlogic can be extended
to other notions of uncertainty, such as innermeasures {Fagin & Halpern,
1991} andDempster-Shafer belief
 functions {Shafer,1976}.
 Inthis paper, we describe alogic for reasoning about upper probabilitymeasures,
along
 the lines of the FHM logic.The logic allows reasoning about linearinequalities
involving
 upperprobabilities measures. Like the logicsconsidered in FHM, our logic
is agnostic as to the interpretation of upperprobabilities, whether frequentist
or subjectivist. The
 main challenge is toderive a provably complete axiomatization of the logic;
to do this, we
 needa characterization of upper probability measuresin terms of properties
that can be expressed in the logic. Manysemantic characterizations of upper
probabilitymeasures have
 been proposed in theliterature. The characterization of Anger andLembcke
{1985} turns
 out to bebest suited for our purposes. Eventhough we are reasoning about
potentially infinite sets of probability measures, thesatisfiability problem
for our logic remains NP- complete. Intuitively, we need guessonly a small
number of probability measuresto satisfy
 any given formula, polynomially many in the size of the formula.Moreover,
theseprobability
 measures can be taken to be defined ona finite state space, again polynomial
in thesize of
 the formula. Thus,we need to basically determine polynomially many values|a
value for
 each probability measure at each state|todecide the satisfiability of a
formula. The rest of this paper is structured asfollows. In Section 2, we
review therequired
 material from probability theory andthe theory of upper probabilities. InSection
3, we
 present the logic andan axiomatization. In Section 4, we provethat the axiomatization
is
 soundand complete with respect to the natural semantic models expressed
in terms of upper probability spaces. Finally,in Section 5, we prove that
the decisionproblem for the logic is
 NP-complete.The proofs of the new, more technical results are given in Appendix
A. To make the paper self-contained, we also review Anger and Lembcke's results
in Appendix B.
 2. Characterizing UpperProbability Measures
 Westart with a brief review of the relevant definitions. Recall that a probability
measure
 is a function 026: 006 ! [0; 1] for 006 analgebra of subsets of 012
{that is 006 is closed under
 complements and unions}, satisfying026{;} = 0, 026{012} = 1, and 026{A
[ B } = 026{A} + 026{B }for
 all disjoint sets A;B in 006.
 2
 A probability space is a tuple {012; 006; 026}, where 012 is aset, 006
is
 an algebra of subsets of 012{the measurable sets}, and 026 is a probabilitymeasure
defined on
 006. Givena set P of probability measures, letP
 003
 be the upperprobability measure defined2. If 012 is infinite, wecould also
require that 006 be a 033-algebra {i.e., closed under countable unions}
and that
 026 be countably additive.Requiring countable additivity would notaffect
our results, since we show that we can take 012 to be finite.For ease of
exposition, we have not required it.
 58A Logic for Reasoning aboutUpper Probabilities
 by P 003
 {X } = supf026{X } : 0262 P g for X 2 006. 3
 Similarly, P 003
 {X } = inff026{X } : 0262 P g is
 the lower probability of X 2 006. A straightforward derivation shows that
the relationship P
 003
 {X} = 1000P
 003 {X } holds between upper and lower probabilities, whereX is the complement
of X in 012. Becauseof this duality, we restrict thediscussion to upper
probability measures in this paper, with the understanding thatresults for
lower probabilities can be similarly derived. Finally, an upper prob ability
spac eis a tuple {012; 006; P } where P isa set of probability
 measureson 006.
 We would like a setof properties that completely characterizes upperprobability
mea-
 sures. In other words, we would like a set of propertiesthat allow us to
determine if a
 function f : 006 ! R{for an algebra 006 of subsets of 012} isan upper
probability measure,
 thatis, whether there exists a set Pof probability measures such that for
allX 2 006,
 P
 003
 {X } =f {X }.
 4
 One approach to the characterization of upper probability measures is to
adapt the characterization of Dempster-Shafer belieffunctions; these functions
are known to be the lower envelope of the probabilitymeasures that dominate
them, and thus form a subclass
 of the class of lower probabilitymeasures. By the duality noted earlier,
a characterization
 of lower probabilitymeasures would yield a characterization of upper probability
measures.
 The characterizationof belief functions is derived from ageneralization
of the following
inclusion-exclusion principle for probabilities{obtained by replacing the
equality with an inequality}:
 026{ n
 [
 i=1 A
 i
 } = n
 X
 i=1 {0001}
 i0001
 {
 X
 J022f1;::: ;ng
 jJ j=i
 026{
   j2J A
 j
 }): It seems reasonable that a characterizationof lower {or upper} probability
measures could be derived along similar lines.However, asis well known, most
properties derivable
 from theinclusion-exclusion principle {which include most of the properties
reported in the
 literature} are insufficient to characterize upperprobability measures.
Huber {1981,p. 257}
 and Walley {1991, p.85} give examples showing the insufficienciesof such
properties.
 Togive a sense of the insufficiency of simple properties, consider the following
\inclusion- exclusion"{style properties, some of whichare taken from {Walley
, 1991}.To simplify the
 statement of theseproperties, let P
 0001 = P
 003
and P
 +1
 =P 003
 .
 {1}P
 003
 {A
 1
 [ 001001 001 [A
 n
 } 024 P
 n
 i=1 P
 jI j=i
 {0001}
i+1
 P
 {0001}
 i
 {
T
 j2I
 A j
 },
 {2}P
 003
 {A
 1
 [ 001 001 001[ A
 n
 } 025 P
 n
 i=1 P
 jI j=i
 {0001}
i+1
 P
 {0001}
 i+1
 { T
 j2I
 A
 j
 },
 {3}P
 003
 {A[ B } + P
 003 {A \ B } 024 P 003
 {A} +P
 003
 {B} 024 P
 003
 {A[ B } + P 003
 {A \ B},3. Inthe literature, the term upper probability issometimes used
in a more restricted sense than here.For
 example, Dempster {1967} usesthe term to denote a class of measures which
were later characterized as
 Dempster-Shafer belief functions {Shafer, 1976}; belief functions are in
fact upper probability measures inour sense, but the converse is nottrue
{Kyburg, 1987}. In the measure theoryliterature, what we call
 upper probability measures are a special case of upperenvelopes of measures,
which are definedas the
 sup of sets of general measures, notjust probability measures.
 4. Itis possible to define a notion of upperprobability over an arbitrary
set of subsetsof 012, not necessearily
 an algebra, bysimply requiring that f coincideswith P
 003
 on its domain,for some set P of probability measures. See Walley {1991}
fordetails.
 59Halpern & Pucella {4} P
 003
{A} + P
 003 {B } 024 P
 003
 {A [ B} + P
 003
 {A \ B } 024 P
 003
 {A}+ P 003
 {B }, {5} P
 003
 {A} + P
 003
 {B } 024 P
003
 {A \ B} + P
 003
 {A [ B } 024 P
 003
 {A}+ P 003
 {B }. Note that without the alternation betweenupper probabilities and lower
probabilities, {1} and {2} would just be thestandard notions of subadditivity
and superadditivity, re-
 spectively.While subadditivity and superadditivity holdfor upper and lower
probabilities, respectively, {1} and {2} arestronger properties. It is easily
verifiedthat all five properties
 hold for upper probability measures. The question is whether they completely
characterize
 theclass of upper probability measures.We show the inherent incompleteness
ofthese
 properties by proving that theyare all derivable from the following simpleproperty,
which
 is by itselfinsufficient to characterize upperprobabilitymeasures:
 {6} If A \B = ;, then P 003
 {A} +P
 003
 {B} 024 P
 003
 {A [ B } 024 P 003
 {A}+P
 003
 {B}.
 Proposition 2.1:Prop erty {6} implies prop erties{1}-{5}.
 Observe that our property {6} is already given by Walley{1991, p. 84}, as
properties {d} and {e}. The following example shows the insufficiency of
Property {6}.Let P be the set
 of probability measures f026 1
 ; 026
 2 ; 026
 3
 ; 026 4
 g over 012= fa; b; c; dg {with006 containing all subsets
 of 012} defined onsingletons by
 026
 1 {a} =
 14
 026
 1
 {b} =
 14
 026 1
 {c} = 14
 026 1
 {d} = 14
 026 2
 {a} = 0026
 2
 {b} =
 18
 026
 2
{c} =
 38
 026
 2 {d} =
 12
 026
3
 {a} =
18
 026 3
 {b} = 38
 026 3
 {c} = 0026
 3
 {d} =
 12
 026
 4
{a} =
 38
 026
 4 {b} = 0 026 4
 {c} = 18
 026 4
 {d} = 12
 ; and extended by additivity to all of006. This defines an upper probabilitymeasure
P
 003
 over 006. Consider the function 035 
* 
 :006 ! [0; 1] defined by
 035 
* 
 {X }=
 032
 P
003
 {X } + 
* if X = fa; b; cg
 P
 003
 {X } otherwise.
 Weclaim that the function 035

* 
 , for small enough 
*  >0, satisfies property {6}, but cannot be an upper probability measure.
Proposition 2.2: For0 < 
*  <
 18
 , the function 035 
* 
 satisfies prop erty{6}, but is not an
 upperprob ability measur e. Thatis, we cannot find a set P 0
 of prob abilitymeasur es such
 that 035 
* 
 = {P
 0
 }
 003
.
 This example clearly illustrates the need to go beyond the inclusion-exclusionprinciple
to find properties that characterize upperprobability measures. As it turns
out, various
 complete characterizations havebeen described in the literature {Lorentz,1952;
Huber,
 1976, 1981; Williams,1976;Wolf, 1977; Giles,1982; Anger & Lembcke, 1985;
Walley , 1991}.
 Most of these characterizations are obtained by considering upper and lower
expe ctations,
 rather than workingdirectly with upper and lower probabilities.Anger and
Lembcke {1985} 60A Logic for Reasoning aboutUpper Probabilities
 give a characterization in terms of upper and lowerprobabilities. Since
their characterization is particularly well-suited to the logicpresented
in the next section, we review ithere.
 The characterization is based on thenotion of set cover. Aset A is said
to be cover e d n times by a multisetffA
 1
 ;: : : ; A
 m
gg of sets if every element ofA appears in at least
 nsets from A
 1
 ;: : : ; A
 m
: for all x 2 A, there existsdistinct i
 1
 ; : : :; i
 n
 in f1; : : : ; mgsuch
 that for all j 024n, x 2 A
 i j
 . It is important tonote here that ffA
1
 ; : : : ; A m
 gg is a multi- set, not a set; the A
 i 's are not necessarily distinct.{We use the ff gg notation to denote
 multisets.}An {n; k}-coverof {A; 012} is a multisetffA
 1
 ;: : : ; A
 m
 gg that covers 012 ktimes
 and covers A n+ k times. For example,ff1; 2g; f2; 3g; f1;3gg covers f1;
2; 3g 2 times, and fff1; 2g;f2; 3g; f1; 3g; f2g;f2ggg is a {2,2} cover of
{f2g; f1;2; 3g}.
 Thenotion of {n; k}-coveristhe key concept in Anger and Lembcke's characterization
 ofupper probabilitymeasures.
 Theorem 2.3: {Anger& Lembcke, 1985} Supposethat 012 is a set, 006 is an
algebra of subsets
 of 012, and035 :006 ! R. Thenthere exists a set P ofprob ability measur
es with035 =P
 003
 if and
 only if 035 satisfies the fol lowing thre e prop erties: UP1. 035{;}=
0,
 UP2. 035{012} = 1,
 UP3.for al l natural numbersm; n; k and al l subsetsA
 1
 ; : : :; A
 m
 in 006, if ffA
 1 ; : : : ; A
m
 gg
 is an{n; k}-cover of{A; 012}, then k+ n035{A} 024 P
 m
 i=1 035{A
 i
 }.
 Proof: Wereproduce a proof of this result in AppendixB.Note that UP1is redundant
in the presence ofUP2 and UP3. Indeed,ff012; ;ggis a
 {0; 1}-coverof {012; 012}, and applyingUP3 yields 035{;}+ 035{012}
= 1. SinceUP2 states that
 035{012}= 1, this means that 035{;}= 0. A further consequence ofUP3 is
that if A022 B, then
 035{A} 024 035{B },since ffB gg is a {1; 0}-cover of{A;012}. Therefore,
for all A2 006, 035{A}2 [0; 1].
 Weneed to strengthen Theorem 2.3 in order to prove the main result of this
paper, namely, the completeness of theaxiomatization of the logic we introduce
inthe next section.
 We show that ifthe cardinality of the state space 012 isfinite, then we
need only finitely many instances of property UP3. Notice that we cannot
derive this fromTheorem 2.3
 alone: even ifj012j is finite, UP3does not provide any bound onm, the number
of sets to consider in an {n; k}cover of a set A. Indeed,there does not seem
to be anya priori reason
 why the value of m, n, and kcan be bounded. Bounding this value of m {and
hence of n and k, since they are no largerthan m} is one of the key technicalresults
of this paper, and
 a necessaryfoundation for our work.
 Theorem 2.4:There exist constants B 0
 ; B
 1 ; : : : such that if012 is a finite set, 006is an algebra of subsets
of 012, and 035 : 006 ! R,then there exists a set Pof prob ability measur
es such that 035 = P 003
 if and only if035 satisfies the fol lowing prop erties:
 UPF1. 035{;} = 0,
 UPF2. 035{012} = 1, UPF3. for al l integers m; n; k 024B j012j
 and all sets A
 1
 ;: : : ; A
 m
 , if ffA
 1 ; : : : ; A
m
 gg
 is an{n; k}-cover of{A; 012}, then k+ n035{A} 024 P
 m
 i=1 035{A
 i
 }.
 61Halpern & Pucella Property UPF3 is significantly weaker than UP3. In principle,
checking that UP3
 holds for a givenfunction requires checking that it holds forarbitrarily
large collections of
 sets,even if the underlying set 012 is finite. Onthe other hand, UPF3 guarantees
that if 012is
 finite, then it is in fact sufficientto look at collections of size at mostB
 j012j
 .This observation
 is key to thecompleteness result.
 Theorem 2.4 does notprescribe any values for the constantsB
 0
 ; B
 1
 ; : : : . Indeed,the
 proof found in Appendix A relieson a Ramsey-theoretic argument that does
not even
 provide a bound on theB
 i
 's. Wecould certainly attempt to obtain such bounds,but
 obtaining them is completely unnecessaryfor our purposes. To get completeness
ofthe
 axiomatization of the logic introduced in the next section, it is sufficient
forthere to exist
 finiteconstantsB
 0
 ; B
 1
 ; : : : .
3. The Logic
 The syntax for thelogic is straightforward, andis taken fromFHM. We fix
a set 010
 0
 =
 fp
 1
 ; p
 2
 ; : : : g of primitive prop ositions. The set 010 ofprop ositional formulas
is the closure of 010
 0
 under^ and :. We assume a special propositional formula true ,andabbreviate
 :true asfalse . We use p to represent primitive propositions, and ' and
to represent
 propositionalformulas. A term is an expressionof the form 022
 1
 l{'
 1
 }+ 001 001 001 + 022 k
 l{'
 k
 }, where
 022 1
 ; : : : ;022
 k
 are reals andk 0251. A basiclikelihoo d formula is a statement ofthe form
t 025 ff, where t is a term and ffis a real. A likelihoo dformula is a Boolean
combination of basic likelihood formulas. Weuse f and g torepresent likelihood
formulas. We use obvious abbreviations where needed, such asl{'} 000 l{
} 025 a for l{'} + {0001}l{ } 025 a, l{'} 025 l{ }
 for l{'}000 l{ } 0250, l{'} 024 afor 000l{'} 025 000a, l{'} < afor
:{l{'}025 a} and l{'} = a for
 {l{'} 025 a} ^{l{'} 024 a}. Define the length jfj of the likelihoodformulaf
to be the number ofsymbols required to write f, where each coefficient is
countedas one symbol. Let L
 QU
 be
 the language consistingof likelihoodformulas. {TheQU stands for quantitative
uncertainty.
 The name for the logic is takenfrom {Halpern, 2002}.}
 In FHM, the operator l was interpreted as either\probability" or \belief
" {in the sense of Dempster-Shafer}. Under the first interpretation, a formula
such as l{'} + l{ }025 2=3
 wouldbe intereted as \the probability of' plus the probability of   isat
least 2=3". Here
 weinterpret l as upper probaiblity. Thus, the logic allows us to makestatements
about
 inequalitiesinvolving upper probabilities.
 To capture this interpretation, we assigna semantics to formulas in L QU
 using an upper probability space, asdefined in Section2. Formally , an upperprob
ability structure isa
 tuple M = {012; 006; P ; 031} where {012; 006;P } is an upper probability
space and031 associates with
 eachstate {or world} in 012 a truth assignmenton the primitive propositions
in 010 0
 . Thus,
031{s}{p}2 ftrue; falseg fors 2 012 and p 2 010 0
 . Let [[p] ]
 M
 =fs 2 012 : 031{s}{p} = trueg.
 We call M measur able if for each p2 010
 0
 , [[p] ]
 M
 ismeasurable. If M is measurable then [['] ]
 M is measurable for all propositional formulas '. In this paper, we restrictour
attention
 to measurable upperprobability structures. Extend 031{s} to a truth assignment
on all propositional formulas in a standard way, and associate with each
propositional formula
 the set [['] ]
 M
 =fs 2 012 : 031{s}{'} = trueg. An easy structural induction shows that
[['] ]
 M
 62A Logic for Reasoning aboutUpper Probabilities
 is a measurable set.If M = {012; 006; P ; 031}, let M j= 022
 1 l{'
 1
 }+ 001 001 001 + 022 k
 l{'
k
 } 025 ff iff022
 1
 P
 003 {[['
 1
 ] ]
 M
 } +001 001 001 + 022
 k
 P
 003
{[['
 k
 ] ] M
 } 025 ff M j= :f iffM 6j= f
 Mj= f ^ giffM j= f andM j= g:
 Note thatL
 QU
 can express lowerprobabilities: it follows from the duality between upper
 and lower probabilitiesthat M j= 000l{:'} 025 fi 0001 iff P
 003
 {[[:'] ]
M
 } 025 fi . 5
 Consider the followingaxiomatization AX
 up
of upper probability, which we prove sound
 and complete in the next section.The key axioms are simply a translation
into L
 QU
 of the characterization of upper probability given in Theorem 2.3. As in
FHM, AX up
 is divided
 into threeparts, dealing respectively with propositionalreasoning, reasoning
about linear
 inequalities, and reasoning about upperprobabilities.
 Prop ositionalre asoning
 Taut.All instances of propositional tautologies inL
 QU
 {see below}. MP. From f andf =} g inferg.
 Re asoning about linear inequalities
 Ineq. All instances of valid formulas about linear inequalities {see below}.
 Re asoning about upper prob abilities L1. l{false} = 0.
 L2. l{true } = 1.
 L3. l{'} 0250.
 L4. l{' 1
 } + 001 001 001+ l{'
 m
 } 000 nl{'}025 k if' }
W
 J 022f1;::: ;mg; jJ j=k+n
 V
 j2J '
 j
 and
 W
 J 022f1;::: ;mg; jJ j=k V
 j2J
 '
 j
 are propositionaltautologies.
 6
 L5.l{'} = l{ } if ' ,   isa propositional tautology.
 Theonly difference between AX up
 and the axiomatization forreasoning about probability
 givenin FHM is that the axiom l{' ^  } + l{'^ : } = l{'} inFHM, which expresses
 theadditivity of probability, isreplaced by L4. Although it may not beimmediately
 obvious, L4 is the logical analogue of UP3. To see this,first note that
ffA
 1
 ; : : : ; A m
 gg
 coversA m times if and only if A022
 S
 J 022f1;::: ;mg; jJ j=n
 T
 j2J
 A
 j
 .Thus, the formula ' }
 W
 J 022f1;::: ;mg; jJ j=k+n
 V
 j2J '
 j
 saysthat ' {more precisely, the set of worlds where ' is true}
 iscovered k + n times byff'
 1
 ;: : : ; '
 n
 gg, while
 W J 022f1;::: ;mg; jJ j=k
V
 j2J
 ' j
 says that the whole space is covered k times byff'
 1
 ;: : : ; '
 n
 gg; roughlyspeaking, the multisetff'
 1
 ;: : : ; '
 n
 gg
 is an {n;k}-cover of {'; true}. The conclusion of L4thus corresponds to
the conclusion of5. Another approach, morein keeping with FHM, would be to
interpretl as a lower probability measure. On the other hand, interpretingl
as an upper probability measure is morein keeping with the literature
 on upperprobabilities.
 6. Note that, according tothe syntax of L
 QU
 , '
 1
 ; : : :; '
 m
 mustbe propositional formulas.
63Halpern & Pucella UP3. Note that in the same waythat UP1 follows from UP2
andUP3, axiom L1 {as
 wellas L3} follows from L2 andL4.
 Instances of Taut include all formulas of the formf_ :f , where fis an arbitrary
 formula inL
 QU
 . Wecould replace Taut by a simplecollection of axioms that characterize
propositional reasoning {see, for example,{Mendelson, 1964}), butwe have
chosen tofocus
 on aspects of reasoning about upper probability.
 As in FHM, the axiomIneq includes \all valid formulas about linear inequalities."
An
 inequality formula is a formula of theform a
 1
 x
 1
 + 001 001 001+ a
 n
 x
 n
 025 c, over variables x
 1
 ;: : : ; x
 n
 .
 An inequality formula is said tovalid if it is true under every possibleassignment
of real
 numbers tovariables. To get an instance ofIneq, we replace each variable
x
 i
 that occurs in a valid inequality formula by a primitive likelihood term
of the forml{'
 i
 } {naturallyeach
 occurence of the variable x
 i
 must bereplaced by the same primitive likelihoodterm l{'
 i
 }).
 As with Taut, we can replace Ineq by a sound and complete axiomatization
for Boolean
 combinationsof linear inequalities. Onesuch axiomatization is given in FHM.
4. Soundness and Completeness A formula f is provable in an axiom system
AX iff can be proven using the axiomsand
 rules of inferences of AX. AX is sound with respect toa class M of structures
if every formula provable in AXis valid in M {i.e., valid in every structure
in M};AX is complete
 withrespect to M if every formula valid in M is provablein AX.
 Our goal is to provethat AX
 up
 is a sound andcomplete axiomatization for reasoning
 about upper probability {i.e., with respect to upperprobability structures}.The
soundness
 of AX
 up
 is immediate from our earlierdisscussion. Completeness is, as usual, harder.Un-
 fortunately, the standard technique for proving completeness in modal logic,
whichinvolves
 considering maximal consistent sets and canonical structures {see, for example,
{Popkorn,
 1994}) does not work.We brieflyreview the approach, just topoint out the
difficulties.
 Thestandard approach uses the following definitions.A formula 033 is consistent
with
 an axiom systemAX if :033 isnot provable from AX. A finite set of formulas
f033
 1
 ;: : : ; 033
 n
 g
 is consistent with AXif the formula 033
 1 ^ 001 001 001 ^ 033 n
 is consistent withAX; an infinite set
 offormulas is consistent with AX if all itsfinite subsets are consistent
with AX. F is
 a maximalAX-consistent set if Fis consistent with AX and no strict superset
of F is
 consistentwith AX. If AX includes Taut and MP, then it is not hard toshow,
using
 only propositional reasoning,that every AX-consistent set of formulascan
be extended to
 a maximalAX-consistent set.
 Toshow that AX is complete with respect tosome class M of structures, we
must show that every formula that is valid in M is provablein AX. To do this,
it is sufficient to show
 that every AX-consistent formula is satisfiable in somestructure in M. Typically,this
is
 done by constructing what iscalled a canonic al structure M
 c
 inM whose states are the
 maximalAX-consistent sets, and then showing that a formula 033 is satisfied
in a worldw
 in M
 c
 iff 033 is one of the formulas in the canonical set associated with worldw.
 Unfortunately, this approachcannot be used to prove completeness here.To
see this,
 consider the set offormulas
 F
 0
 = fl{'} 024 1n ; n = 1; 2; : : :g [ fl{'} >0g:
 64A Logic for Reasoning aboutUpper Probabilities
 This set is clearlyAX
 up
 {consistent according toour definition, since every finite subset is satisfiable
in an upper probabilitystructure and AX
 up
is sound with respect to upper probability structures. It thus can be extended
to a maximal AX
 up {consistent set F .
 However, the set F
 0 of formulas is not satisfiable:it is not possible to assign l{'} a value
 thatwill satisfy all the formulas at the same time.Hence, F is not satisfiable.Thus,
the
 canonicalmodel approach, at least applied naively, simply will not work.
 We take a different approach here, similarto the one taken in FHM. We do
not try to
 constructa single canonical model. Of course, westillmust show that if a
formulaf is
 AX
 up -consistent then it is satisfiable in an upper probability structure.
Wedo this by an
 explicit construction, depending on f . We proceed asfollows.
 By a simple argument,we can easily reduce the problem to the casewhere f
is a
 conjunctionof basic likelihood formulas and negationsof basic likelihood
formulas. Let p
 1
 ; : : :; p
 N
 be the primitive propositions that appear in f. Observe that there are 2
2
 N
 inequivalent propositional formulas overp
 1
 ; : : :; p
 N
 . Theargument goes as follows. Letan
 atom over p
 1 ; : : : ; p
 N be a formula of the formq
 1
 ^ : : :^ q
 N
 , whereq
 i
 is either p i
 or :p
 i
 .
 There are clearly 2 N
 atoms over p 1
 ; : : : ;p
 N
 . Moreover,itis easy to see that any formula over p
 1
 ;: : : ; p
 N
can be written in a unique way as adisjunctionof atoms. There are 2 2
 N
 suchdisjunctions,so the claim follows.
 Continuing withthe construction of a structure satisfyingf , let 032
 1 ; : : : ; 032
 2
 2
 N
be some
 canonical listing of theinequivalent formulas overp
 1
 ; : : :; p
 N
 . Withoutloss of generali-
 ty, weassumethat 032
 1
 is equivalent to true , and032 2
 2
 N
 is equivalent to false. Since ev-
 ery propositional formula over p
 1
; : : : ; p
 N is provably equivalentto some 032, itfollows
 that f is provablyequivalent to a formula f 0
 where each conjunct off
 0
 is of the form 022
 1
 l{032
 1
 } + 001001 001 + 022
 2 2
 N
 l{032
 2
 2
N
 } 025 fi .Note that the negation of such a formulahas the form
 022
 1 l{032
 1
 } + 001 001 001 +022
 2
 2
 N l{032
 2
 2
 N
 } < fior, equivalently , {000022
 1
 }l{032
 1
 } + 001001 001 + {000022 2
 2
 N
 }l{032
 2 2
 N
 } >000fi .
 Thus, the formulaf gives rise in a natural way toa system of inequalities
of the form: 022
 1;1
 l{032
 1
} + 001 001 001 + 022 1;2
 2
 N
 l{032
2
 2
 N
 }025 ff
 1
 . .
 .
 .
 . .
 .
 .
 . 022
 r;1
 l{032
 1
} + 001 001 001 + 022 r;2
 2
 N l{032
 2
 2
 N
 } 025ff
 r
 022
 0
 1;1
 l{032
 1
 }+ 001 001 001 + 022 0
 1;2
 2
 N
 l{032 2
 2
 N
 } > fi
 1
 .
 .
 .
 . .
 .
 .
 . .
 022
 0
 s;1
 l{032 1
 } + 001 001 001+ 022
 0
 s;2
 2
 N
 l{032
 2
 2 N
 } > fi
 s
 :
 {1}
 We can express {1} as a conjunction ofinequality formulas, by replacing
each occurrence
 of l{032 i
 } in {1} by x i
 . Call this inequality formulaf .
 If f is satisfiable in some upperprobability structure M , then we cantake
x
 i
 to be the upper probability of 032 i
 in M ; thisgivesa solution off .However,f mayhave a solution
 without fbeing satisfiable. For example, iff is the formula l{p} = 1=2 ^
l{:p} = 0, thenf has an obvious solution;f , however, isnot satisfiable inan
upper probability structure,
 because the upper probability of the setcorresponding to p and the upper
probability of the
 set corresponding to:p must sum to at least 1 in all upper probability structures.
Thus, we must add further constraints to thesolution to force it to act like
an upperprobability.
 UP1{UP3or, equivalently , the axiomsL1{L4, describe exactly whatadditional
con-
 straints are needed.The constraint corresponding to L1{or UP1} is just x
 1
 = 0, since
 65Halpern & Pucella we have assumed 032
 1
 is the formula false. Similarly, the constraint corresponding to L2 is
 x
2
 2
 N
 =1.The constraint corresponding to L3is x
 i
 025 0,for i = 1; : : : ;2
 2
 N
 .What about
 L4? Thisseems to require an infinite collection of constraints, just as
UP3 does.
 7 This is where UPF3 comes into play. It turns out that, if fis satisfiable
at all, it
 issatisfiable in a structure with at most 2 N
 worlds, one for each atom over p
 1
 ; : : :; p
 N
 .
 Thus,we need to add only instances ofL4 where k; m; n < B 2
 N
 and ' 1
 ; : : : ; ' m
 ; ' are all among 032
 1
 ;: : : ; 032
 2
2
 N
 . Although this is alarge number of formulas {in fact, wedo not know
 exactly how large, sinceit depends on B
 2
 N
 , which we have notcomputed}, it suffices for our
 purposesthat it is a finite number.For each of these instances ofL4, there
is an inequality of the form a
 1 x
 1
 + 001001 001 + a
 2 2
 N
 x
 2
 2
 N
025 k. Let
 ^ f , the inequalityformula corr esp onding tof,
 be the conjunction consisting off , together with all theinequalities corresponding
to the
 relevant instances of L4, and the equations and inequalitiesx
 1
 = 0, x 2
 2
 N
 = 1, and x
 i
 025 0
 for i= 1;: : : ; 2
 2
 N
 , corresponding to axiomsL1{L3.
 Proposition4.1: The formula f issatisfiable in an upper prob abilitystructure
iff the
 inequality formula
 ^
 fhas a solution. More over,if
 ^
 f hasa solution, then f is satisfiable in an upper prob abilitystructure
with at most 2
 jf j
 worlds.
 Theorem 4.2: The axiom systemAX
 up
 is sound and complete for upper prob abilitystruc-
 tures.
 Proof:For soundness, it is easy to see that every axiom is valid for upper
probability structures, including L4, whichrepresents UP3.
 Forcompleteness, we proceed as in the discussion above. Assume that formula
fis not
 satisfiable in an upperprobability structure; we must show thatf is AX
 up
 {inconsistent.
 We first reducef to a canonical form. Letg
 1
 _ 001001 001 _ g
 r
 be a disjunctive normal form expression for f {where eachg
 i
 is a conjunction of basic likelihood formulas and their negations}. Using
propositional reasoning, we can show that f is provably equivalent to this
 disjunction. Since f is unsatisfiable,each g
 i
 must also be unsatisfiable. Thus, it is sufficient to show that any unsatisfiable
conjunctionof basic likelihoodformulas and theirnegations is
 inconsistent. Assumethat f is such a conjunction.Using propositional reasoning
and axiom L5, f is equivalent to a likelihood formulaf
 0
 that refers to 2 2
 N
 propositional formulas, say
 032
 1 ; : : : ; 032
 2
 2
 N
 .Since f is unsatisfiable, so isf
 0
 . By Proposition4.1, the inequality formula
 ^
 f
 0
 correspondingto f
 0
 has no solution.Thus, by Ineq, the formula:f
 00
 that results by replacing each instance of x i
 in
 ^
 f
 0
 by l{032
 i
 } isAX
 up
 {provable.All the conjuncts of f
 00 that
 are instances of axiomsL1{L4 are AX
 up {provable. It follows that:f
 0
 is AX up
 {provable,
 and hence so is :f .5. Decision Procedure Having settled the issue of the
soundnessand completeness of the axiom system AX up
 ,
 weturn to theproblem of the complexity of deciding satisfiability. Recall
the problem of7. Although we are dealing with only finitely many formulas
here,032
 1
 ; : : :; 032
 2
 2 N
 , recall that the formulas '
 1
 ; : : :; '
 m
 in L4need not be distinct, so there are potentially infinitely many instances
ofL4 to deal
 with.
 66A Logic for Reasoning aboutUpper Probabilities
 satisfiability:given a likelihood formulaf , we want to determine if thereexists
an upper
 probability structureM such that M j= f . As we now show, thesatisfiability
problem is
 NP-complete, and thus no harder than satisfiability for propositional logic.
 For the decision problemto make sense, we need to restrict our language
slightly. If
 we allow real numbers as coefficients in likelihoodformulas, we have to
carefully discuss theissue of representation of such numbers. To avoid these
complications, we restrict our
 language {in this section} toallow only integer coefficients.Note that we
can stillexpress rational coefficients by the standard trick of \clearing
the denominator". For example, we
 can express 23
l{'} 025 1 by 2l{'} 025 3 andl{'} 025
 23
 by 3l{'} 025 2. Recallthat we defined
 jfj to be the length of f, that is, the number of symbolsrequired to write
f , where each coefficient is counted as one symbol.Define jjf jj to be thelength
of the longest coefficient appearing in f , when written inbinary. The size
of a rational number
 ab , denoted jj
 ab
 jj,
 where a and b are relatively prime,is defined to be jjajj+ jjbjj.
 Apreliminary result required for the analysis of thedecision procedure shows
that if a formula is satisfied in some upperprobability structure, then it
is satisfied ina structure
 {012; 006; P ; 031}, whichis \small"in terms of the number of states
in 012,the cardinality of the
 set Pof probability measures, and the size of thecoefficients in f .
Theorem 5.1: Suppose fis a likelihoo d formula that issatisfied in some upper
prob ability
 structur e. Thenf is satisfied in a structure {012; 006; P; 031}, wherej012j
024 jf j 2
 , 006 = 2 012
 {every
 subsetof 012 is measur able},jP j 024 jf j,026{w} is a rationalnumber
such that jj026{w}jj is
 O{jf j
 2
 jjf jj + jf j
 2
 log{jf j}) for every world w 2012 and 026 2 P ,and 031{w}{p}= false
for every
 worldw 2 012 and every primitive prop osition p not appe aringin f .
 Theorem 5.2:The problem of decidingwhether a likelihoo d formula is satisfiablein
an
 upper prob abilitystructure is NP-complete.
 Proof: For the lower bound,it is clear that a given propositional formula
' is satisfiable iff
 the likelihood formula l{'} >0 is satisfiable, therefore the satisfiabilityproblem
is NP-hard.
 For the upper bound, given a likelihoodformulaf , we guess a \small" satisfyingstructure
 M = {012;006; P ; 031}for f of the form guaranteed to existby Theorem
5.1. We can describe such a model M in size polynomial in jf j andjjf jj.
{The fact that031{w}{p} =false for
 every world w2 012 and every primitive propositionp not appearing in f
meansthat we
 must describe031 only for propositions that appear inf .} We verify thatM
j= f as follows. Let l{ } be an arbitrarylikelihood term in f .We compute
[[ ] ] M
 by checking the truth assignment of each s 2012 and seeing whether this
truth assignment makes   true. We then
 replace each occurence of l{ } in f by max 0262P
 f
 P s2[[ ] ] M
 026{s}g and verify that the resulting expression is true.6. Conclusion
 Wehave considered a logic with the same syntaxas the logic for reasoning
about probabili- ty, innermeasures, and belief presented in FHM, with uncertainty
interpreted asthe upper
 probability of a set ofprobability measures. Under this interpretation,we
have provided
 a sound andcomplete axiomatization for the logic. We further showed that
the satisfiabil- ity problem is NP-complete {as it is forreasoning about
probability, inner measures,and
 67Halpern & Pucella beliefs}, despite having to deal withprobability structures
with possibility infinitely many
 states and infinite sets of probability measures. The key step in theaxiomatization
involves
 finding a characterization of upper probability measures thatcan be captured
in the logic.
 Thekeystep in the complexity result involves showing that if a formula is
satisfiable at all, it is satisfiable in a \small" structure, where the
size of the state space, as well as thesize
 of the set of probabilitymeasures andthe size of all probabilities involved,
are polynomial
 in the length of the formula. Given the similarityin spirit of theresults
for the various interpretations ofthe uncer-
 tainty operator {as aprobability, inner measure, belieffunction, and upper
probability}, including the fact that the complexity ofthe decision problem
is NP-complete in all cases, we conjecture that there is some underlyingresult
from which all these results should follow.
 It would be interesting to make that precise.
 In FHM, conditionalprobabilities as well as probabilitiesare investigated.
We have not, in this paper, discussed conditional upperprobabilities. The
main reason for this is that, unlike probability, we cannot characterize
conditional upper probabilities in termsof {un-
 conditional} upper probabilities.Thus, our results really tell us nothing
about conditional
 upper probabilities.It might be of interest to consider alogic that allows
conditional up-
 per probabilities as primitive likelihoodterms {that is, allows likelihood
terms ofthe form
 l{' j }). While there is no intrinsicdifficult giving semantics to such
a language,it is far
 from clear what an appropriateaxiomatization would be, or the effect of
thisextension on
 complexity.
 Finally , it is worth noting that the semantic framework developed here
and in FHM is in fact rich enough to talk about gambles {that is, real-valued
functions overthe set
 of states} and the expectationof such gambles. Expectation functions canbe
defined for
 the different measures of uncertainty, includingupperprobabilities, and
it is not difficult to extend the FHM logic in order to reason about expectation.
One advantageof working with
 expectation functions isthat they are typically easier to characterizethan
the corresponding
 measures;for instance, the characterization of expected upper probabilities
is much simpler than that of upper probabilities {Huber,1981; Walley , 1981,
1991}. However,gettinga
 complete axiomatization is quitenontrivial. We refer the reader to {Halpern
& Pucella,
 2002} for more details onthis sub ject. We remark that Wilson andMoral {1994}
take as
 their starting point Walley's notion of lower and upperprevisions. They
consider when
 acceptance of one set of gambles impliesacceptanceof another gamble. Since
acceptance involvesexpectation, it cannot beexpressed in the logic considered
in this paper;however,
 it can be expressed easiliyin the logic of {Halpern & Pucella, 2002}. Acknowledgments
 A preliminaryversion of this paper appears in Uncertainty in Artificial
Intel ligence, Pro-
 c e e dingsof the Seventeenth Conferenc e, 2001. Thanks to Dexter Kozen,
Jon Kleinberg, and
 HubieChen for discussionsconcerning set covers. Vicky Weissman read a draft
of this paper and provided numerous helpful comments.We also thank the anonymous
UAI and JAIR reviewers for their useful comments andsuggestions. This work
was supported inpart by
 NSF under grants IRI-96-25901 andIIS-0090145, andONR under grants N00014-00-1-03-
68A Logic for Reasoning aboutUpper Probabilities
 41, N00014-01-10-511,and N00014-01-1-0795. The first author wasalso supported
in part
 by a Guggenheimand a Fulbright Fellowshipwhile on sabbatical leave; sabbatical
support from CWI and the Hebrew University ofJerusalem is also gratefully
acknowledged. Appendix A. Proofs
Proposition 2.1: Prop erty{6} implies prop erties {1}-{5}. Proof: We introduce
thefollowing auxiliary properties to help derivethe implications:
 {7} P
 003
 {A} + P 003
 {B }024 P
 003
 {A[ B } + P
 003 {A \ B }.
 {8} P
 003
 {A} + P
 003
 {B } 024 P
003
 {A \ B} + P
 003
{A [ B }.
 {9}P
 003
 {A[ B } + P
 003 {A \ B } 024 P 003
 {A} +P
 003
 {B}.
 {10} If A \B = ;, then
P
 003
 {A}+ P
 003
 {B} 024 P
 003
 {A [ B } 024 P 003
 {A}+P
 003
 {B} 024 P
 003
 {A [ B } 024 P 003
 {A} +P
 003
 {B}:
 Using these properties, weshow the following chain of implications: {6}
=} {10}
 {10} =} {9} =}{3}
 {10} =} {7} =} {4}
 {10} =}{8} =} {5}
 {4}; {5} =} {1}; {2}:
 The implication {4},{5} =} {1}, {2} followseasily by mutual induction on
n. The
 base case is the followinginstances of properties {4} and {5}:P
 003
 {A[ B } 025 P
003
 {A} + P 003
 {B }000
 P
 003
{A \ B } and P 003
 {A [ B} 024 P
 003
 {A} + P
 003 {B } 000 P
 003
 {A \ B}. The details are left to the reader. We now prove the remainingimplications.
 {9} =}{3}: Since {9} is already one of theinequalities in {3}, it remains
to show that it implies the other inequality in {3}, that is, P
 003
 {A} + P
 003
 {B } 024 P
 003 {A [ B } + P 003
 {A \ B}.
 P
 003
{A [ B } + P 003
 {A \ B} = 1 000 P
 003 {A [ B} + 1 000 P
 003 {A \ B } = 1 000 P
 003 {A \B} + 1 000 P
 003
 {A[B }
 = 2 000 {P
 003 {A \B } + P
003
 {A [B })
 =2 000 {P
 003 {B \A} + P
 003 {B [A})
 0252 000 {P
 003 {B} + P 003
 {A})
 = 1 000 P
 003
 {B} + 1 000 P
 003 {A}
 = P
 003
 {B } + P
 003 {A}:
 69Halpern & Pucella {7} =} {4}: Since{7} is already one of the inequalities
in {4},it remains to show that
 it implies theother inequality in {4}, that is, P 003
 {A [ B} + P
 003
 {A \ B } 024 P
 003
 {A} + P 003
 {B }.
 P
 003
 {A}+ P
 003
 {B} = 1 000 P
 003 {A} + 1000 P
 003
 {B }
 = 2 000{P
 003
 {A} + P
 003 {B})
 025 2 000 {P 003
 {A[B } + P 003
 {A\B })
 = 1 000 P
 003
 {A [B } + 1 000 P
 003
 {A \B }
 =1 000 P
 003
{A \ B }+ 1 000 P
 003
{A [ B } = P
 003
 {A \ B } + P
 003
 {A [ B}:
 {8} =}{5}: Since {8} is already one of theinequalities in {5}, it remains
to show that it implies the other inequality in {5}, that is, P
 003
 {A \ B } + P
003
 {A [ B }024 P
 003
 {A} + P
 003
 {B }.
 P
003
 {A} + P 003
 {B }= 1 000 P
 003
 {A} + 1 000 P 003
 {B}
 = 2 000 {P 003
 {A} + P
 003
 {B})
 0252 000 {P
 003 {A \B } + P
003
 {A [B })
 =1 000 P
 003
{A \B } + 1 000 P 003
 {A[B }
 = 1 000 P
 003 {A [ B} + 1 000 P
 003 {A \ B } = P
 003
 {A [ B } + P
 003
 {A \ B}:
 For the next implications,given A; B , let Z =A\ B .
 {10} =} {9}:
 P
 003 {A [ B } =P
 003
 {(A000 Z } [ B } 024 P
 003
{A 000 Z } + P 003
 {B }[since {A 000 Z }\ B = ;]
024 P
 003
 {(A 000 Z } [ Z} 000 P
 003
 {Z } + P
 003 {B }
 = P 003
 {A} +P
 003
 {B} 000 P
 003
 {A \ B }:
 {10} =} {7}:
 P
 003
 {A[ B } = P
 003 {(A 000 Z }[ B }
 025 P 003
 {A 000Z } + P
 003 {B }
 025P
 003
 {(A000 Z } [ Z }000 P
 003
 {Z } + P
 003 {B }
 = P 003
 {A} +P
 003
 {B} 000 P
 003
 {A \ B }:
 {10} =} {8}:
 P
 003
 {A[ B } = P
 003 {(A 000 Z }[ B }
 025 P 003
 {A 000Z } + P
 003 {B }
 025P
 003
 {(A000 Z } [ Z }000 P
 003
 {Z } + P
 003 {B }
 = P 003
 {A} +P
 003
 {B} 000 P
 003
 {A \ B }:
 70A Logic for Reasoning aboutUpper Probabilities
 {6} =} {10}: Again, since {6} alreadycomprises two of the inequalities in
{10}, it remains to show that it implies theother two, that is, if A \B
=;, then
 P 003
 {A} +P
 003
 {B }024 P
 003
 {A[ B } 024 P
 003 {A}+ P
 003 {B }:
 First,we show that P
 003 {A} + P
 003 {B } 024 P
 003
 {A [ B}. Using {6}, we know that P
 003
 {A \B} + P
 003
 {A} 024 P
 003 {(A\B } [ A}= P
 003
 {B }:
 In other words,P
 003
 {A \B} 024 P
 003
 {B}+ P
 003
 {A}. From this, we derive that
 P
 003
 {A[ B } = 1 000 P 003
 {A [ B }
 = 1000 P
 003
 {A \B }
 025 1 000{P
 003
 {B } 000 P
 003
 {A})
 = 1 000 P
 003 {B} + P 003
 {A} = P
 003
 {B } + P
 003 {A}:
 Second,we show that P
 003 {A [ B } 024 P 003
 {A}+P
 003
 {B}. Using {6}, we know that P
 003
 {A \B} + P
 003
 {A} 025 P
 003 {(A\B } [ A}= P
 003
 {B }:
 {The last equality follows from the fact that {A \B} [ A =B when A \ B
=;.} In
 other words,P
 003
 {A \B} 025 P
 003
 {B } 000 P 003
 {A}. From this, we derive that
 P
 003
 {A[ B } = 1 000 P 003
 {A [ B }
 = 1000 P
 003
 {A \B }
 024 1 000{P
 003
 {B } 000 P
 003
 {A})
 = 1 000 P
 003 {B } + P 003
 {A} = P
 003
 {B } + P
 003 {A}:Proposition 2.2: For 0 < 
*  <
 18
 , the function035
 
* 
 satisfies prop erty {6}, but is not an
 upper prob ability measur e.That is, we cannot find a setP
 0
 of prob abilitymeasur es such
 that 035 
* 
 = {P
 0
 }
 003
.
 Proof: We are given 0< 
*  <
 18
 . It is easy to check mechanically that 035
 
*  satisfies {6}.
 Wenow show that there is no set P 0
 such that 035 
* 
 = {P
 0
 }
 003
 . By way of contradiction, assume there is such a P 0
 . By the properties ofsup, this means that there is a 0262 P
 0
 such that 026{fa; b; cg} >
 34
 , since 035
 
* 
 {fa; b; cg} =
 34
 + 
*  >
 34
 .Consider this 026 in detail. Since026 2 P ,
 we must have for all X 2 006, X6= fa; b; cg,that 026{X } 024{P
 0
 } 003
 {X }= P
 003
 {X}. In particular,
 026{fa; bg}; 026{fb; cg}; 026{fa; cg} 024 12
 .Therefore,
 026{fa;bg} + 026{fb; cg} + 026{fa; cg} 024 32
 : {2}
 However,from standard properties of probability, it follows that
 026{fa; bg} + 026{fb; cg} + 026{fa; cg} = 2026{fa; b; cg}>2 002
 34
 =
 32
 ;
 71Halpern & Pucella which contradicts {2}. Therefore,026, and therefore
P
0
 cannot exist, and 035 
* 
 is not an upper probabilitymeasure.Theorem 2.4: There exists constants B
 0
 ;B
 1
 ; : : :such that if 006 is an algebra of subsets
 of 012 and035 is a function 035 :006! R, then there exists a setP of
prob ability measur es such
 that 035 =P
 003
 if and only if035 satisfies the fol lowing prop erties:
 UPF1. 035{;} = 0,
 UPF2. 035{012} = 1, UPF3. for al l integers m; n; k 024B j012j
 and all sets A
 1
 ;: : : ; A
 m
 , if ffA
 1 ; : : : ; A
m
 gg
 is an{n; k}-cover of{A; 012}, then k+ n035{A} 024 P
 m
 i=1 035{A
 i
 }.
 Proof: Inview of Theorem 2.3, we need only show thatthere exist constant
B
 0 ; B
 1
 ; : : : such that a function 035satisfies UP3 iff it satisfiesUPF3. Clearly,
UP3 alwaysimplies
 UPF3, soit is sufficientto show that there exists B
 0
 ; B
 1 ; : : : such that UPF3implies
 UP3.
 Weneed some terminology before proceeding.An exact {n; k}-cover of {A; 012}
is a cover
 C of A with the property that every element of A appears inexactly n + k
sets inC , and
 everyelement of 012000 A appears in exactlyk sets in C . Thus,while an
{n; k}-coverof {A; 012}
 can have many extra sets, as long as the sets coverA at least n + k timesand012
k times,
 an exact cover hasonly the necessary sets, with the right total number of
elements. An
 exact{n; k}-cover C of{A; 012} is dec omp osableif there exists an exact
{n 1
 ; k
 1 }-cover C
 1 and
 an exact {n
 2
 ; k
 2
 }-cover C
 2
 of {A; 012} such thatC
 1
 and C 2
 form a nontrivial partition ofC ,
 with n = n 1
 + n
 2 and k =k
1
 + k
 2 . Intuitively, an exact cover C is decomposable if it can be split into
two exact covers. It follows easily by induction thatfor any exact {n; k}-
cover, thereexists a {not necessarilyunique} finite set of nondecomposable
exact covers
 C
 1
 ;: : : ; C
 m
, with C
 i
 an exact {n
 i
 ; k
 i
 }-cover, suchthat the C
 i
 's a nontrivial partition of C
 withn =
 P
 m
 i=1
 n
 i
 and k =
 P
 m i=1
 . {If Cis itself nondecomposable, we can takem = 1 and
 C
 1
 = C .} Onecan easily verify that if C isan exact {n; k}-coverof {A; 012}
and C 0
 022 C is an exact {n
 0 ; k
 0
 }-coverof {A; 012} with n 0
 + k
 0 < n + k, thenC is decomposable.
 The followinglemma highlights the most important property of exact covers
from our
 perspective. It says that for any setA 2 006, there cannot be a \large"nondecomposable
 exact cover of {A; 012}.
 Lemma A.1:There exists a sequenc eB
 0
 1
; B
 0
 2
 ; B
 0
 3
 ; : : : such that for all A 022 012, every exact {n; k}-coverof {A; 012}
with n> B
 0
 j012j or k>B
 0 j012j
 is dec omp osable.
 Proof: Itis clearly sufficient to show that for anyfinite 012 we can find
a B j012j
 with the required properties. Fix a 012.Given A 022 012, we first showthat
there exists N
 A
 such that
 if n > N A
 or k >N
 A
 , every exact {n; k}-cover of {A;012} is decomposable. Supposefor the
 sake of contradiction thatthis is not the case. This means that wecan find
an infinite
 sequenceC
 1
 ; C
 2
 ; : : : suchthat C
 i
 is a nondecomposable exact {n
 i
 ; k
 i
 }-coverof {A; 012}, with
 either n
 1
 < n 2
 < : : : ork
 1
 < k 2
 < : : : . To derive a contradiction, we usethe following lemma, knownas
Dickson's Lemma {Dickson, 1913}.
 72A Logic for Reasoning aboutUpper Probabilities
 Lemma A.2:Every infinite sequenc e ofd-dimensional vectors over the natural
 numb ers contains a monotonical ly nondecr e asing subsequenc e in the pointwise
 or dering{where x 024 y inthe pointwise ordering iff x i
 024 y
 i for al l i}.
 Proof: It is straightforward to prove by induction on k that ifk 024 d,
then
 everyinfinite sequence of vectors x 1
 ; x
 2 ; : : : contains a subsequencex
 i
 1
 ;x
 i
 2
 ; : : : such that x
 i 1
 j
 ; x i
 2
 j
; : : : is a nondecreasing sequence ofnatural numbers for all
 j024 k. The base case is immediatefrom the observation that every infinite
sequence of natural numbers contains anondecreasing subsequence. For the
inductive step, observe that ifx
 i
 1
 ;x
 i
 2
 ; : : :is a subsequence such that x i
 1
 j
 ; x
 i
 2 j
 ; : : :
 isa nondecreasing sequence of natural numbers for all j 024 k, then the
sequence x
 i
 1
 k+1
 ; x
 i 2
 k+1
 ; : : :of natural numbers must have anondecreasing subsequence. This
 determinesa subsequence of the original sequence with theappropriate property
 for allj 024 k + 1.Let S
 1
; : : : ; S
 2 j012j
 be an arbitraryordering of the 2
 j012j
 subsets of 012. Wecan associate
 with any coverC a 2
 j012j -dimensional vector x
C
 = {x
 C 1
 ; : : : ;x
 C
 2
 j012j
 }, where x C
 i
 is the number oftimes the subset S
 i of 012 appears in the multisetC . The key property of this association
 is that if C
0
 and C are multisets, thenC
 0
 022 Ciff x
 C
 0 024x
 C
 in the pointwise ordering.
 Consider the sequence ofvectors x
 C
 1 ; x
 C
 2 ; : : : associated with thesequence C
 1
 ;C
 2
 ; : : : of nondecomposable exact covers of {A; 012}. By Lemma A.2, there
is anondecreasing sub-
 sequence of vectors,x
 C
 i
 1 024 x
 C
 i 2
 024 001 001 001. But this means that C
 i
 1
 022 C i
 2
 022 001001 001 . Since
 n
 1
 < n
 2
 < : : : or k
1
 < k
 2
< : : : , every cover in the chain must be distinct. But any pair of exact
covers inthe chain is such that C
 i
 022C
 i+1
 , meaningC
 i+1
 is decomposable,contra-
 dicting our assumption.Therefore, there must exist an N A
 such that any exact {n; k}-cover
 of Awith n> N
 A
 ork > N
 A
 isdecomposable.
 Now defineB
 0
 j012j = maxfN
 A : A 022 f1;: : : ; j012jgg.It is easy to see that this choice works.Toget
the constants B
 1 ; B
 2
 ; : : :, let B
 N
 = 2N B
 0
 N
 , for N = 1; 2; : : : , where B
0
 N
 is as
 in Lemma A.1. We now show thatUPF3 impliesUP3 with this choice ofB
 1
 ; B
 2
 ; : : : .
 Assumethat UPF3 holds. Fix 012. Supposethat C = ffA 1
 ; : : : ;A
 m
 gg is an {n; k}-cover
 of {A; 012} with jC j= m. We want to showthat k + n035{A}024
 P
 m
 i=1
 035{A
 i
 }. We proceed as follows.
 The first step is to show that, without loss of generality,C is an exact
{n; k}-cover of
 {A;012}. Let B
 i
 consist of those states s 2 A i
 such that eithers 2 A and s appears in more than n + k sets inA
 1
 ; : : :; A
 i0001
 or s 2 012 000 Aand s appears in more than ksets in
 A
 1
 ; : : : ; A
 i0001
 . Let A 0
 i
 =A i
 000 B
i
 . Let C
0
 =ffA
 0
 1
 ; : : :; A
 0
 m
 gg. It is easy to check that C
 0
 is
 an exact {n; k}-cover of {A;012}. For if s 2 A, then s appears in exactlyn
+ k sets in C
 0
 {it
 appears inA
 0
 j
 iffA
 j
 is among the firstn + k sets in C inwhich s appeared} and, similarly,
 if s 2 012 000A, then s appears in exactlyk sets in C
 0
 . Clearly if UP3 holds forC
 0
 , then it holds for C , since 035{A
 0
 i
 } 024 035{A
 i
 } for i = 1;: : : ; m. Thus, we canassume without loss of
 generalitythat C is an exact {n;k}-cover of A.
 We can also assume without loss of generality that no set in C is empty{otherwise,
 we can simply remove theempty sets in C ; the resulting setis still an {n;
k}-coverof
 {A; 012}). Thereare now two cases to consider.If max{m; n; k} 024B
 j012j
 , thedesired result
 73Halpern & Pucella follows from UPF3. Ifnot, considera decomposition of
Cinto multisets C
 1 ; : : : ; C
 p ,
 where C
 h is an exact {n
 h ; k
 h
 }-coverof {A; 012} and is not furtherdecomposable. We claim
 thatmax{jC
 h
 j; n
 h
 ; k
 h
 } 024 B
j012j
 for h = 1; : : : ; p. Ifn
 h
 > B
 j012j
 or k
 h > B
 j012j , thenit is
 immediatefrom Lemma A.1that C
 h
 can be furtherdecomposed, contradicting the fact
 that C
 h
 is not decomposable.And if jC
 h
 j > B
 j012j , then observe that
 P X 2C
 h
jX j 025 jC
 h j.
 Since jC
 h
 j > B
 j012j
 = 2j012jB 0
 j012j
 , there must be some s 2 012 which appearsin at least 2B
 0
 j012j
 sets in C h
 . Since C
 h
 is an exact {n h
 ; k
 h }-cover, it follows that eithern
 h
 > B
 0 j012j
 or k h
 > B
 0
 j012j
 .
 Butthen, by Lemma A.1, C
 h is decomposable, again a contradiction. Now we can apply UPF3 to each
ofC
 1
 ; : : :; C
 k
 to get X
 X 2C
 h
 035{X }000 n
 h
 035{A} 025 k
h
 :
 Since the C h
 's form a decomposition ofC , we have
 p X
 h=1
 0 @
 X
 X 2C h
 035{X }000 n
 h
 035{X }
 1
 A 025
 p
 X h=1
 k
 h }
 p
 X
 h=1
 0
 @
 X
 X 2C
 h 035{X }
 1 A
 000
 p
 X
 h=1
 n h
 035{A}025
 p
 X
 h=1
 k
 h }
 m
 X
 i=1
 035{A i
 } 000 { p
 X
 h=1 n
 h
 }035{A} 025
 p X
 h=1
 k h
 By decomposition, n=
 P
 p
 h=1
 n
 h
 andk =
 P
 p
 h=1
 k
 h
 , and therefore
 P
m
 i=1
 035{A
 i
 } 000n035{A} 025 k,
 showing that UP3 holds, as desired.Proposition 4.1:The formula f is satisfiable
in anupper prob ability structure iff the
 inequality formula ^
 f has a solution.More over, if
 ^
 f has a solution, then fis satisfiable in
 an upper prob ability structurewith at most 2
 jfj
 worlds.
 Proof:Assume first that f issatisfiable. Thus there is some upperprobability
structure
 M ={012; 006; P ;031} such that M j= f . As in Section 4, letp
 1
 ; : : :; p
 N
 be the primitive propo-
 sitions that appear inf , and let 032
 1 ; : : : ; 032
 2
 2
 N
be some canonical listing of the inequivalent
 formulas over p 1
 ; : : : ;p
 N
 . Withoutloss of generality, we assume that032
 1
 is equivalent to
 true , and032
 2
 2
 N is equivalent to false. Define the vector x 003
 by letting x 003
 i
 = P 003
 {[[032 i
 ] ]
 M },
 for 1 024 i024 2
 2
 N
 . Since M j=f , it is immediate that x 003
 is a solution to the inequality
 formulaf. Moreover, since 032 1
 = false and032
 2
 2
N
 = true , it follows thatx
 003
 1
= 0 {since
 P
 003 {[[false ]] M
 } = P
003
 {;} = 0}andx
 003
 2
2
 N
 = 1{sinceP
 003
 {[[true ]]
 M
} = P
 003
 {012} =1}. Final-
 ly, consider a conjunctof
 ^
 f correspondingto an instance of L4; supposeit has the form
 x
 i
 1
 + 001 001 001x
 i
 m
 000nx
 i
 m+1 025 k. Since this conjunct appears in
 ^
 f ,it must be the case that
 {032
 i
 m+1
 }
 W
 J 022f1;::: ;mg; jJj=k+n
 V J 022f1;::: ;mg; j2J
 032
 i
 j
 } ^ { W
 jJ j=k
 V
 j2J 032
 i
 j } is a propositionaltau- tology. Thus, it follows that [[032
 i
 1 ] ]
 M
 ;: : : ; [[032
 i
 m
 ] ]
 M
 is an {n; k}-cover for {[[032 i
 m+1
 ] ] M
 ; [[true]]
 M
 }. It follows from UP3 that
 P
 003
 {[[032
 i
 1
] ]
 M
 } +001 001 001 + P
003
 {[[032
 i
 m
 ] ]
 M
 } 000 nP 003
 {[[032] ]
 M
 } 025k:
 74A Logic for Reasoning aboutUpper Probabilities
 Thus,x
 003
 is a solution to theinequality formulas corresponding toL4. Hence, x
 003 is a solution
 to
 ^ f .
 For the converse,assume that x
 003
 is asolution to
 ^
 f .We construct an upper probability structure M = {S;E ; P ; 031} suchthatM
j= f as follows.Let p
 1
 ; : : :; p
 N
 be the primitive propositions appearing in f. Let S = fffi 1
 ; : : : ; ffi 2
 N
 g be the atoms over p
 1
 ;: : : ; p
 N
. Let E be
 the set of allsubsets of S . As observed earlier, every propositional formula
overp
 1
 ; : : :; p
 n
 is equivalent to a unique disjunction of atoms.Thus, we can get a canonical
collection 032
 1
 ; : : :; 032
 2
 2
 N
 of inequivalentformulas over p
 1 ; : : : ; p
n
 by identifying each formula032
 i
 with a different element of E ,where 032
 1
 corresponds tothe empty set and 032
 2 2
 N
 corresponds to all of S . Define a set function035 by taking 035{fffi
 i
 1
; : : : ; ffi
 i j
 g} = x 003
 i
 if 032 i
 is the disjunction of the atoms ffi
 i
 1 ; : : : ; ffi
 i
 j
 . Let031{ffi}{032} =true iff ffi } 032. It is now sufficient to show
that035 is an upper probability {of a setP of probability
 measures},since then it is clear that {S;E ; P ; 031} j= f {since x
 003
 is a solution to ^
 f , the system of inequalities derived from formulaf }. To do this, by Theorem2.4,
it suffices to verify
 UPF1, UPF2, and UPF3, usingB
 2
 N
 inUPF3, since jS j = 2 N
 .
 UPF1:035{;} = x
 003
 1
 = 0.
 UPF2: 035{S }= x
 003
 2
 2
 N
 = 1.
 UPF3: Suppose that A andA
 1
 ; : : :; A
 m
 are inE and satisfy the premises of prop- erty UPF3, with k;m; n 024 B
 2
 N
 . Let 032
 i
 1
 ; : : :; 032
 i
 m ; 032
 i
 m+1
 be the canoni-
 cal formulas corresponding to A 1
 ; : : : ;A
 m
 ; A, respectively. Clearly, A 022 S
 J 022f1;::: ;mg; jJ j=k+n
 T
 j2J A
 i
 j
 iff 032
 i
m+1
 }
 W J 022f1;::: ;mg; jJ j=k+n V
 j2J
 032
 i
 j
 is a
 propositional tautology andsimilarly 012 022
 S J 022f1;::: ;mg; jJ j=k
T
 j2J
 A i
 j
 iff W
 J 022f1;::: ;mg; jJ j=k V
 j2J
 032
 i
 j
 is a propositional tautology.Thus,
 P
 m
 j=1
 x
 i
 j
 000
 x
i
 m+1
 025k is one of the inequality formulas in ^
 f . Thus, it followsthat
 P
 m
 j=1
 x
 003
 i j
 000 x
003
 i
 m+1 025 k, as desired. Byour definition of 035, we therefore have
 k+n035{A} 024
 P
 m i=1
 035{A i
 }, and so UPF3holds.Theorem 5.1:Suppose f is a likelihoo d formula that
is satisfiedin some upper prob ability structur e. Then f issatisfied in
a structure{012; 006; P ;031}, where j012j 024 jf j
 2 , 006 = 2
 012 {every
 subset of 012is measur able}, jP j 024 jf j, 026{w}is a rational number
such thatjj026{w}jj is O{jf j
 2
 jjf jj + jf j
 2
 log{jf j}) for every worldw 2012 and 026 2 P, and 031{w}{p} = false
for every world w 2 012 and everyprimitive prop osition p not appe aring
in f .
 Proof:The first step in the proof involves showing that if P is a set ofprobability
measures
 defined on an algebra 006 of a finite space 012, we can assumewithout
loss of generality that
 for each set X 2 006, there isa probability measure 026
 X 2 P such that 026 X
 {X } =P
 003
 {X}
 {rather than P
003
 {X } just being thesup of 026{X } for026 2 P }.
 LemmaA.3: Let P bea set of prob ability measur esdefined on an algebra 006over
a finite set
 012.Then there exists a set P 0
 of prob abilitymeasur es such that, for eachX 2 006, P
 003
 {X } = {P
 0
 } 003
 {X };more over, there is a prob ability measur e 026 X
 2 P
 0 such that 026
 X {X } = P
 003
 {X }.In
 addition, for any interpretation 031, if M ={012; 006; P ;031} and M
= {012; 006; P
 0 ; 031}, then for all
 likelihoo d formulas f, M j= f iffM
 0
 j=f .
 75Halpern & Pucella Proof: Since 006 is finite, to show that P
 0
 exists, it clearly suffices to show that, for each X 2 006, there is a
probabilitymeasure 026
 X
 such that026
 X
 {X }= P
 003
 {X} and, if P
 0
 = P [ f026
 X g,
 then P
003
 {Y } = {P
 0
 }
 003 {Y} for all Y2 006.
 Given X ,if there exists 026 2 P suchthat 026{X } = P 003
 {X }, then weare done. Otherwise,
 we construct asequence 026
 1
 ;026
 2
 ; : : :of probability measures in Psuch that lim
 i
 026
 i
 {X} =
 P
 003
 {X } and, for all Y2 006, the sequence 026 i
 {Y } convergesto some limit. Let X
 1 ; : : : ; X
 n be an enumeration of the sets in 006, with X
 1
 =X. We inductively construct a sequenceof
 measures 026
 m1 ; 026
 m2
 ; : : : in P form 024 n such that 026 mi
 {X
 j } converges to a limit fori 024 k
 andlim
 i!1
 026
 mi {X } = P
 003
 {X }. For m = 1, we know there mustbe a sequence 026
 11 ; 026
 12
 ; : : : of measures in P suchthat 026
 1i
{X } converges to P 003
 {X }.For the inductive step, if m < n,
 supposewe have constructed anappropriate sequence 026
 m1
 ; 026
 m2 ; : : : . Consider the sequence of real numbers 026
 mi
 {X
 m+1 }. Using the Bolzano-Weierstrasstheorem {Rudin, 1976} {which
 says thatevery sequence of real numbers has a convergent subsequence}, this
sequence has a convergent subsequence. Let026
 {m+1}1
 ; 026
 {m+1}2 ; : : : be the subsequence of026
 m1
 ; 026 m2
 ; : : :
 which generates this convergentsubsequence. This sequence of probability
measures clearly
 has all the required properties.This completes the inductive step. Define
026
 X
{Y } = lim
 i!1
 026
 ni
 {Y}. It is easy to checkthat that 026
 X
 is indeed a probability
 measure, that 026 X
 {X } =P
 003
 {X}, andif P
 0
 = P [ f026
 X g, thatP
 003 {Y } = {P 0
 }
 003 {Y } for all
 Y 2 006. This shows that anappropriate set P
 0
 exists.
 Now, given 031, let M = {012; 006; P ; 031} and M 0
 = {012; 006; P
 0
 ; 031}. A straightforward induction on the structure of f showsthat M j=
f iffM
 0
 j=f . For the base case: {012; 006; P ;031} j= a
 1
 l{'
 1 } + 001 001 001 +a
 n
 l{' n
 } 025 a , a
 1
 P 003
 {[[' 1
 ] ]
 M } + 001 001 001 +a
 n
 P
 003 {[['
 n
 ] ]
 M
 } 025a
 , a
 1 {P
 0
 } 003
 {[[' 1
 ] ]
 M 0
 } + 001 001 001+ a
 n
 {P 0
 }
 003 {[['
 n
 ] ]
 M
 0
 } 025 a
 , {012; 006; P
 0 ; 031} j=a
 1
 l{' 1
 }+ 001 001 001+ a
 n
 l{'
 n
 } 025a:
 The others cases are trivial.Just as in FHM, to prove Theorem 5.1, we make
use of the followinglemma which
 can be derived fromCramer's rule {Shores, 1999} and simple estimates onthe
size of the
 determinant {see also{Chvatal, 1983} for a simpler variant}:
 Lemma A.4:If a system of r linearequalities and/or inequalitieswith integer
co efficients e ach of length at most lhas a nonnegative solution, then it
has anonnegative solution with at
 most r entries positive, and where the size of each memberof the solution
is O{rl+ r log{r}). Continuing with the proof of Theorem5.1, suppose that
f is satisfiable in an upper
 probability structure.By Proposition 4.1, the system ^
 f of equality formulashas a solution,
 so f issatisfied in a upper probability structure witha finite state space.
Thus, by Lem- ma A.3, f is satisfied in astructure M = {012; 006; P ; 031}
such that for all X 2 006, there exists 026
 X
 2 Psuch that 026
 X {X } = P
 003
 {X }.
 As in the completeness proof, we can writef in disjunctive normal form.Each
disjunct
 g isa conjunction of at most jfj 000 1 basic likelihood formulasand their
negations. Since
 Mj= f , there must besome disjunct g suchthat Mj= g. Supposethat g is the
conjunction
 of r basic likelihood formulas ands negations of basic likelihood formulas.Let
p
 1
 ;: : : ; p
 N
 76A Logic for Reasoning aboutUpper Probabilities
 be the primitiveformulas appearing in f .Let ffi
 1
 ;: : : ; ffi
 2
 N
 be the atoms overp
 1
 ; : : :; p
 N
 .
 Asin the proof of completeness, we derive asystem of equalities and inequalities
fromg.
 It is a slightly more complicatedsystem, however. Recall that each propositionalformula
 overp 1
 ; : : : ; p N
 is a disjunction of atoms.Let '
 1
 ; : : :; '
 k
 be the propositional formulas that
 appear ing. Notice that k < jf j {since there are some symbolsin f , such
as the coefficients, that are not in the propositional formulas}. The system
of equations and inequalitieswe
 construct involve variables x
 ij
 , wherei = 1; : : : ; kandj = 1; : : :; 2
 N
 . Intuitively, x
 ij
 represents026
 [['
 i ] ]
 M
 {[ [ffi
 j
 ] ]
 M
 }, where 026
 [['
 i
 ] ] M
 2 P is such that026
 [['
 i ] ]
 M
 {[ ['
 i
 ] ]
 M
 } = P
 003 {[['
 i
 ] ]
 M
 }. Thus, the system includes k < jf j equations of the following form, x
 i1
 +001 001 001 + x
 i2
 N
 = 1;
 for i = 1;: : : ; k. Since 026 [['
 i
 ] ]
 M
 {[ ['
 i
 ] ]
 M
 } 025 026{[['
 i
 ] ] M
 } for all 0262 P , if E
 i is the subset of
 f1; : : : ; 2
 N g such that '
i
 =
 W
 j2E
 i
 ffi j
 , the system includesk
 2
 000 kinequalities of the form
 X j2E
 i
 x
 ij
 025
 X
 j2E
 i x
 i
 0
 j
 ;
 for each pairi, i
 0
 such thati 6= i
 0
 . For each conjunct ing of the form 022
 1 l{'
 1
 } + 001 001 001 + 022
 n
 l{'
 k
 } 025 ff, there is a corresponding inequality where,roughly speaking, we
replace l{'
 i
 }
 by026
 [['
 i ] ]
 M
 {[ ['] ]
 M
 }. 8
 Since 026
 [['
 i
 ] ] M
 corresponds to P
 j2E
 i
 x
 ij
, the appropriate inequality is
 k
 X
 i=1 022
 i
 X j2E
 i
 x
 ij
 025ff: Negations of such formulas correspondto a negated inequalityformula;
as before,this is
 equivalent to a formulaof the form
 000{
 k
 X
 i=1 022
 i
 X j2E
 i
 x
 ij
 }> 000ff:
 Notice that there are at mostjf j inequalities corresponding tothe conjuncts
of g. Thus, altogether, there are at mostk{k 0001} + 2jf j < jf j 2
 equations and inequalities inthe
 system {since k < jf j}. We know that thesystem has a nonnegative solution
{taking x
 i
 j
 tobe 026
 [[' i
 ] ]
 M
 {[ [ffi
 j
 ] ] M
 }). It follows fromLemma A.4 that the system has a solution x
 003
 = {x
 003
 11
 ;: : : ; x
 003
 12
 N
 ; : : :; x
 003
 k1 ; : : : ; x
 003 k2
 N
 }with t024 jf j
 2
 entries positive, and witheach entry
 of size O{jf j
 2
 jjf jj + jf j
 2
 log{jf j}).
 We use this solution toconstruct a small structure satisfying the formulaf
. Let I =
 fi : x
 003
 ij is positive, for some jg; suppose that I =fi
 1
 ; : : :; i
 t
 0
 g, forsome t
 0 024 t. Let
 M= {S; E ; P ;031} where S has t 0
 states, say s 1
 ; : : : ;s
 t
 0
 ,and E consists of all subsets ofS . Let
 031{s h
 } be the truth assignmentcorresponding to the formula ffi i
 h
 , that is,031{s
 h
 }{p} = true
 if and only ifffi
 i
 h
 }p {and where 031{s h
 }{p} =false if p does not appear inf }. Define
 P =f026
 j
 : 1024 i 024 kg, where026
 j
 {s h
 }= x
003
 i
 h
j
 . It is clear from theconstruction that M j=f .
 Since jP j= k < jf j, jS j = t
 0 024 t 024 jf j 2
 and 026
 j
 {s
 h } = x
 003
 i
 h
 j
, where, by construction, the size of x
 003
 i h
 j
 is O{jf j
 2
 jjf jj + jf j 2
 log{jf j}), the theorem follows.8. Forsimplicity here, we are implicitly
assuming thateach of the formulas '
i
 appears in each conjunct of g. This is without loss of generality, since
if '
 i does not appear, we can put it in,taking 022
 i
 =0. 77Halpern & Pucella Appendix B. Proof of theCharacterization of Upper
Probabilities To make this paper self-contained,in this appendix we give
a proof ofTheorem 2.3. The
 proof we give isessentially that of Anger and Lembcke{1985}. Walley {1991}
gives an alternate proof along somewhat similar lines.Note that the functional
~gwedefine in our
 proofcorresponds to the construction in Walley's Natural Extension Theorem,
which is needed in his version of this result. Theorem 2.3: Supposethat 012
is a set, 006 is an algebra of subsets of 012, and 035: 006 ! R.
 Thenthere exists a set P ofprob ability measur es with035 = P
 003
 if and only if 035 satisfies the fol lowing thre e prop erties:
 UP1. 035{;} = 0,
 UP2. 035{012} = 1, UP3. for al l integers m; n; k andal lsubsets A
 1
 ;: : : ; A
 m
 in 006, if ffA 1
 ; : : : ;A
 m
 gg
 is an {n; k}-cover of {A; 012},then k + n035{A}024
 P
 m
 i=1
 035{A
 i
 }.
 Proof:The \if " direction of the characterization is straightforward. GivenP
= f026
 i g
 i2I
 a
 set of probability measures, we show P
 003
 satisfiesUP1-UP3.
 UP1:P
 003
 {;}= supf026
 i
 {;}g = supf0g = 0
 UP2: P 003
 {012} = supf026
 i
 {012}g = supf1g = 1 UP3: Given A
 1
 ; : : : ; A m
 and A such thatA 022
 S
 J022f1;::: ;mg;jJj=k+n
 T j2J
 A
 i
 j
 and
 012022
 S
 J 022f1;::: ;mg;jJj=k
 T
 j2J
 A
 i
 j
 , then for any iwe have k026
 i {012} + n026
 i {A} 024
 P m
 j=1
 026 i
 {A
 j }, that is k + n026 i
 {A} 024 P
 m
 j=1 026
 i
 {A j
 } 024 sup i
 f
 P
 m
 j=1
 026 i
 {A
 j }g 024
 P
m
 j=1
 sup
 i
 f026
 i {A
 j
 }g =
 P
 m j=1
 P
 003 {A
 j
 }.But sup
 i
 fk+n026
 i
 {A}g = k+nsup
 i
 f026 i
 {A}g=
 k +nP
 003
 {A}, sok +nP
 003 {A} 024
P
 m
 j=1
 P
 003
 {A j
 }, as required. As for the \only if " direction, wefirst prove a general
lemma relating theproblem to the
 Hahn-Banach Theorem.Some general definitions are needed.Suppose that we
are given a space W and an algebra Fof subsets of W . LetK be the vector
space generated by the indicator functions 1
 X defined by
 1
X
 {x} =
032
 0 if x62X
 1 if x2 X,
 for X 2 F .A sublinear functional on Kis a mapping c : K ! Rsuch that c{ffh}
=ffc{h}
 for ff025 0 and c{h
 1
 + h
 2 } 024 c{h 1
 } + c{h
 2
 } for allh
 1
 ; h
 2
 . A sublinear functional isincre asing
 if h 0250 impliesc{h + h 0
 } 025 c{h
 0
 } for allh
 0
 2 K.The following result is a formulation of the well-known Hahn-Banach
Theorem {see, forexample, {Conway, 1990}). Theorem {Hahn-Banach}: Let K
be a vectorspac e over R, andlet g be a sublinear functional on K. IfM is
a linear subspac ein K and 025 : M !R is a linear functional such that 025{x}
024g{x} for al lx in M, then there is a linear functional 025
 0 : K ! R such that 025
 0
 j
 M
 = 025 and 025 0
 {x} 024g{x} for al lx in K.
 Lemma B.1:Let g : F ! [0; 1] be such that g{W } = 1 and suppose that there
is an
 incre asing sublinear functional ~g on K such that
78A Logic for Reasoning aboutUpper Probabilities
 1. ~g{1
 K
 } =g{K } for K 2F ;
 2. ~g{h} 024 0 if h024 0;
 3. ~g{0001} 024 0001 {where ~g{ff} is identified with~g{ff1
 W }}.
 Then g is an upper prob ability measur e. Proof: We show thatg is an upper
probability by exhibitinga set f026
 X
: X 2 006g of probability measures, withthe propertythat 026
 X
 {X } = g{X }and 026
 X
 {Y } 024 g{X }for Y 6= X . Each probability measure 026 X
 is constructed through anapplication of the Hahn-Banach
 Theorem. Given X 2 F ,definethe linear functional 025 on thesubspace generated
by 1
 X by
 025{ff1
 X
 } = ff~g{1
 X
 }.We claim that 025{h} 024 ~g{h}for all h in the subspace. Sincethe elements
 of the subspace havethe form ff1
 X
 , there are two cases to consider:ff 025 0 and ff < 0. If ff 025 0, then
025{ff1
 X
 } =ff~g {1
 X } = ~g{ff1
 X
 }, since ~g is sublinear. Moreover,0= ~g{0} =
 ~g{0001
 X
 + 1
 X
 } 024~g{0001
 X } + ~g{1
 X
 }, so ~g{0001
 X
 }025 000~g{1
 X
 }. Thus, if ff>0, then
 025{000ff1
 X
 }= 000ff~g{1 X
 } 024 ff~g{0001
X
 } = ~g{000ff1
 X
}:
 Now, by the Hahn-BanachTheorem, we can extend 025 to a linearfunctional
025
 0
 on all of K such that 025
 0
 {h} 024 ~g{h} for all h. We claim that {a} 025 0
 {1
 Y } 025 0 for all Y2 K and {b}
 025
 0
 {1} = 1. For{a}, note that 025
 0 {0001
 Y
 } 024 ~g{0001
 Y
 } 0240 by assumption, so 025
0
 {1
 Y
} 025 0. For
 {b},note that 025
 0
 {1}024 ~g{1} = g{W } = 1 and that 025 0
 {1} = 000025 0
 {0001} 025 000~g{0001} 0251 {since
 ~g{0001} 024 0001, by assumption}. Define 026
 X
{Y } = 025
0
 {1
 Y
}. Since 025
 0 {1
 W
 } = 1,026
 X
 {W} = 1. If Y andY
 0
 are disjoint, it is immediate from the linearity of 025that 026
 X
 {Y [ Y
 0
} = 026
 X
 {Y } + 026
 X
 {Y
 0
 }.By construction,
 026
X
 {Y } 024~g{1
 Y
 }= g{Y } for anyY 6= X , and 026 X
 {X } =025{1
 X
 } = ~g{1
 X
 }= g{X }. Bottom line: there is a probability measure026
 X
 dominated byg suchthat 026
 X {X } = g{X }.
 Take P= f026
 X
 : X 2 006g.Since for any X we have that026
 X
 {X} = g{X } and 026
 X
 {Y} 024 g{X }{if Y 6= X },we have P
 003 {X } = 026
 X
 {X } = g{X }. Therefore, g =P
 003
 .The main result follows by showing how to construct, from a function035
satisfyingthe
 properties ofTheorem 2.3, a sublinear functional con K with the required
properties. Suppose that g : 006! R is a function satisfyingUP1-UP3. As
we show in thediscussion
 after Theorem 2.3 in the text,UP1-UP3 show that the range ofg is in fact
[0; 1].Since g
 satisfies UP3, if ffK
 1 ; : : : ; K
m
 gg is an {n; k}-cover of {K;012}, we have k +ng{K } 024
P
 m
 i=1
 K
 i
 .
 This is equivalent to saying that k+ n1
 K
 024 P
 m
 i=1 1
 K
 i
 . Hence, for all K
1
 ; : : : ; K m
 such that
 k+ n1
 K
 024
 P
 m
 i=1
 1
 K
 i , we have k +ng{K } 024
 P
 m
 i=1
 g{K
 i
 },or equivalently
 000 kn
 +
 1n m
 X
 i=1 g{K
 i
 } 025 g{K }: {3}
 This observationmotivates the following definition of thefunctional ~g :
K ! R[
 f0001; 1g: ~g{h} = inf {
 000
 kn
 +
 1n
 m
 X i=1
 g{K i
 } : m; n; k2 N ; m; n > 0; K
 1
 ; : : :; K
 m
 2 F; 000
 kn
 +
 1n
 m
 X i=1
 1
 K i
 025 h
}
 :
 Our goal now is toshow that ~g satisfiesthe conditionsof Lemma B.1.
 79Halpern & Pucella 
*  It is almost immediate from thedefinitions that ~g is increasing:if h
025 0 and 000 kn
+
 1n
 P
 m
 i=1
 1 K
 i
 025 h+ h
 0
 , then000
 kn +
 1n P
 m
 i=1 1
 K
 i
025 h
 0
 . 
*  To see that ~g issublinear, note that it is easy tosee using the properties
of inf that ~g{h
 1 + h
 2
 }024 ~g{h
1
 } + ~g{h
 2
 }. Toshow that ~g{ffh} = ff~g{h} for ff 025 0, first observethat
 the definition of ~g isequivalent to
 inf
 {
 000fi+
 m
 X
 i=1
 fi
 i
g{K
 i
 } :m 2 N ; fi ; fi i
 2 R
 + ; K
 1
 ; : : :; K
 m
 2 F000 fi +
 m
 X
 i=1
 fi i
 1
 K
 i
 025 h
 } :
 Consider first the caseff > 0. Then
 ~g{ffh} = inf
 { 000fi +
 m X
 i=1
 fi i
 g{K
 i
 } : 000 fi+
 m
 X
i=1
 fi
 i 1
 K
 i
 025 ffh
 }
 =inf
 {
 000fi+
 m
 X
i=1
 fi
 i g{K
 i
 } : 000
 fiff
 +
 1ff
 m X
 i=1
 fi i
 1
 K
 i
 025 h
 } = ff inf
 { 000
 fiff
 +
 1ff
 m
 X i=1
 fi
 i g{K
 i
 } : 000
 fiff
 +
 1ff
 m X
 i=1
 fi i
 1
 K
 i
 025 h
 } = ff~g {h}:
 For ff= 0, it is clear from the definition of~g that ~g{1 ;
 } 024 g{;}. From {3} it follows that ~g{1
 ; } 025 g{;},and hence ~g{0} = ~g{1
 ;
 }= g{;} = 0.

*  It is immediate from the definitionof ~g that ~g{1 K
 } 024 g{K } for K 2 F ;the fact that
 ~g{1 K
 } = g{K } now follows from {3}. 
*  It is immediate from thedefinition that ~g{0001} 024 0001.
 
* If h024 0, then 000h 025 0; since ~gis increasing, ~g{h} 024 ~g{000h
+ h} = ~g{0}, and since ~g is sublinear, ~g{0} = 0. Since the conditions
of Lemma B.1 aresatisfied, g is an upper probabilitymeasure.References Anger,
B., & Lembcke, J. {1985}.Infinitely subadditive capacities as upperenvelopes
of
 measures.Zeitschriftfªur WahrscheinlichkeitstheorieundVerwandte Gebiete,68,
403{
 414.
 Chvatal, V. {1983}. Linear Pro gr amming. W. Freemanand Co., San Francisco,
Calif. Conway, J. B. {1990}.ACourse in Functional Analysis{Second edition}.
No. 96 in Graduate Texts in Mathematics. Springer-Verlag.
 Dempster, A. P. {1967}.Upper and lower probabilitiesinduced bya multivalued
mapping.
 Annalsof Mathematical Statistics,38{2}, 325{339.
 80A Logic for Reasoning aboutUpper Probabilities
 Dickson, L. E.{1913}. Finiteness of the odd perfect andprimitive abundant
numbers with n distinct prime factors. American Journal of Mathematics, 35{4},
413{422.
 Fagin, R., & Halpern, J. Y. {1991}. Uncertainty, belief and probability.Computational
 Intel ligence, 7 {3}, 160{173.
 Fagin, R., Halpern, J. Y., & Megiddo, N.{1990}. A logic for reasoning aboutprobabilities.
 Information and Computation, 87 {1,2}, 78{128.
 Giles, R.{1982}. Foundations for a theory of possibility. In Gupta, M. M.,
& Sanchez, E.
 {Eds.}, Fuzzy Information and Decision Pro c esses, pp. 183{195.North-Holland.
 Halpern, J. Y. {2002}.Reasoning about uncertainty.Book manuscript.
 Halpern, J. Y., &Pucella, R. {2002}. Reasoning about expectation. In Pro
c. Eighteenth
 Confer enc e on Uncertaintyin Artificial Intel ligence {UAI 2002}.
 Huber, P. J. {1976}.Kapazitªaten statt Wahrscheinlichkeiten? Gedanken zur
Grundlegung
 der Statistik. Jber. Deutsch. Math.-Ver ein, 78, 81{92.
 Huber, P. J. {1981}. Robust Statistics. Wiley Interscience. Kyburg, Jr.,
H. E. {1987}. Bayesianand non-Bayesian evidential updating.Artificial Intel-
 ligence, 31, 271{293.
 Lorentz, G. G.{1952}. Multiply subadditive functions.CanadianJournal of
Mathematics, 4 {4}, 455{462.
 Mendelson, E.{1964}. Intro duction to Mathematical Lo gic. Van Nostrand,
NewYork.
 Popkorn, S. {1994}.First Steps in Modal Lo gic. Cambridge University Press,
Cambridge; New York.
 Rudin, W. {1976}.Principles of Mathematical Analysis{Third edition}. McGraw-Hill.
 Shafer, G. {1976}. A Mathematical Theory of Evidence.Princeton University
Press, Prince- ton, NJ.
 Shores,T. {1999}.Applied Linear Algebra and Matrix Analysis {Secondedition}.
McGraw-
 Hill.
 Smith, C. A. B. {1961}. Consistencyin statistical inference and decision.Journal
of the
 Royal Statistical Society, Series B, 23, 1{25.
 Walley , P.{1981}. Coherent lower {and upper}probabilities. Manuscript,
Dept. of Statistics, University of Warwick. W alley , P. {1991}.Statistical
Re asoning with Impre cise Prob abilities. Chapmanand Hall.
 Williams, P. M. {1976}.Indeterminate probabilities. In Przelecki, M.,Szaniawski,
K., &
 Wojciki,E. {Eds.}, Formal Methodsin the Methodolo gy of Empirical Sciences,
pp.
 229{246. Wilson, N., & Moral, S. {1994}.A logical view of probability.In
Pro c. 11th Europ e an Confer enc e on Artificial Intelligence {ECAI-94},
pp. 71{95. Wolf, G. {1977}. Ober e und Untere Wahrscheinlichkeiten. Doctoral
dissertation, Eid-
 genªossischen TechnischenHochschule, Zurich. {Diss.ETH 5884}.
 81