An Analysis of First-Order Logics of Probability

1 Introduction

Consider the two statements "The probability that a bird chosen at random will fly is greater than .9" and "The probability that Tweety (a particular bird) flies is greater than .9." It is quite straightforward to capture the sec­ ond statement by using a possible-world semantics along the lines of that used in (FH88, FHM88, Nil86]. Namely, we can imagine a number of possible worlds such that the predicate Flies has a different extension in each one. Thus, Flies{Tweety) would hold in some possible worlds, and not in others. We then put a probability distribution on this set of possible worlds, and check if the set of pos­ sible worlds where Flie.,(Tweety) holds has probability greater than .9.

However, as pointed out by Bacchus (Bac88b, Bac88a], this particular possible worlds approach runs into dif­ ficulties when trying to represent the first statement, which we may believe as a result of statistical informa­ tion of the form "More than 90% of all birds fly." What is the formula that should hold at a set of worlds whose probability is greater than .9? The most obvious candidate is perhaps Vx(Bird(x) ::::} Flie&(x)). However, it might very well be the case that in each of the worlds we consider possible, there is at least one bird that doesn't fly. Hence, the statement Vx( Bird( x) ::::} F/ie&( x)) holds in none of the worlds (and so has probability 0). Thus it cannot be used to represent the statistical informat;ion. As Bacchus shows, other straightforward approaches do not work either.

There seems to be a fundamental difference between these two statements. The first captures statistical infor­ mation, and the second captures what has been called a degree of helief (Bac88b, Kyb88]. The first statement seems to assume only one possible world (the "real" world), and in this world, some probability distribution over the set of birds. It is saying that if we consider a bird chosen at random, then with probability greater than .9 it will fly. The second statement implicitly as­ sumes the existence of a number of possibilities (in some of which Tweety flies, while in others Tweety doesn't), with some probability over these possibilities.

Bacchus (Bac88b] provides a syntax and semantics for a first-order logic for reasoning about statistical informa­ tion, where the probability is placed on the domain. This approach has difficulties dealing with degrees of belief. For example, if there is 01lly one fixed world, in this world either Tweety flies or he doesn't, so Flies(Tweety) holds with either probability 1 or probability 0. In particular, a statement such as "The probability that Tweety flies is between .9 and .95" is guaranteed to be false! Recogniz­ ing this difficulty, Bacchus moves beyond the syntax of his logic to define the notion of a helief function, which lets us talk about the degree of belief in the formula a given a knowledge base (J. However, it would clearly be useful to be able to capture reasoning about degrees of belief within a logic, rather than moving outside the logic to do so.

In this paper, we describe two first-order logics, one for capturing reasoning about statistical information, and another for reasoning about degrees of belief. We then show how the two can be easily combined in one frame­ work, allowing us to simultaneously reason about statis­ tical information and degrees of belief.

We go on to consider issues of axiomatizability. Bac­ chus is able to provide a complete axiomatization for his language because he allows probabilities to take on non­ standard values in arbitrary ordered fields. Results of a companion paper [AH89J show that if we require prob­ abilities to be real-valued (as we do here), we cannot in general hope to have a complete axiomatization for our language. We give sound axiom systems here which we show are complete for certain restricted settings. This suggests that our axiom systems are sufficiently rich to capture a great deal of interesting reasoning about prob­ ability.

2 Probabilities on the domain

We assume that we have a first -order language for rea­ soning about some domain. We take this language to consist of a collection ell of predicate symbols and func­ tion symbols of various arities (as usual, we can iden­ tify constant symbols with functions symbols of arity 0). Given a formula tp in the logic, we also allow formulas of the form w..,( tp) ~ 1/2, which can be interpreted as "the probability that a random x in the domain satisfies tp is greater than or equal to 1/2". We actually extend this to allow arbitrary sequences of distinct variables in the sub­ script. To understand the intuition beltind this, suppose the formula Son(x, y) says that xis the son of y. Now consider the three terms w..,(Son(:r, y)), wy(Son(x, y)), and W(z,y)(Son(x, y)). The first describes the probabil­ ity that a random x is the son of y; the second describes the probability that x is the son of a random y; the third describes the probability that a random pair (x, y) will have the property that x is the son of y.

We formalize these ideas by using a two-sorted lan­ guage. The first sort consists of the function symbols and predicate symbols in ell, together with a countable family of object variable8 x 0 , y 0 , .... The second sort consists of the binary function symbols + and x, which represent addition and multiplication, constant symbols 0 and 1, representing the real numbers 0 and 1, binary relation symbols > and =, and a countable family of field variable8 xf, yf, .... (We drop the superscripts on the variables when it is clear from context what sort they are.) Terms of the first sort describe elements of the do­ main we want to reason about. Terms of the second sort typically represent probabilities, which we want to be able to add and multiply.

We now define object terms, field terms, and formu­ las simultaneously by induction. We form object terms, which range over the domain of the first-order language, by starting with object variables and closing off un­ der function application, so that if f is an n-ary func­ tion symbol in ell and t1, ... , tn are object terms, then J(t1, ... , t,.) is an object term. We form field terms, which range over the reals, by starting with 0, 1, and probability terms of the form w1( tp ), where tp is an ar­ bitrary formula, and then closing off under + and x, so that t1 + t2 and t1 x t2 are field terms if t1 and t2 are. We form formulas in the standard way. We start with atomic formula8: if P is an n-ary predicate symbol in ell, and t),····t,. are object terms, then r(t), ... ,t,.) is an atomic formula, while if t 1 and t2 are field terms, then t1 = t2 and t1 > t2 are atomic formulas. We sometimes also consider the situation where there is an equality symbol for object terms; in this case, if t1 and t2 are object terms, then t1 = t2 is also an atomic formula. We then close off under conjunction, negation, and universal quantification, so that if lf!l and 1f!2 are form11las and xis a (field or object) variable, then tp1 II tp2 , ·tp1, and Vxtp1 are all formulas. We call the resulting language £ 1 ( <l> ); if it includes equality between object terms, we call it £!(ell).

We define V, =>, and 3, in terms of 11, ·, and Vas usual. In addition, if t1 and t2 arc two field terms, we use other standard abbreviations such as t1 < t2 for t2 > t1, t1 ~ t2fort1 > t2Vt1 =t2, t1 ~ 1/2for(1+1)xt1 ~ 1, and so on.

The only differences between our syntax and that of Bacchus is that we write wr(IP) rather than [<11]%, and, for simplicity, we do not consider what Bacchus calls mea8uring function8 (functions which map object terms into field terms), and the only field functions we allow are+ and X. The language is still quite rich, allowing us to ex­ press conditional probabilities, notions of independence, and statistical notions; we refer the reader to [Bac88bJ for examples.

We defim~ a type 1 probability 8tructure to be a tuple (D, 1r, J-L), where D is a domain, 1r assigns to the predi­ cate and function symbols in ell predicates and functions of the right arity over D (so that (D, 1r) is just a stan­ dard first-order structure), and fl. is a rJiscrete probability function on D. That is, we take fL to be a mapping from D to the real interval [0, lj such that LdED J-L( d) = l. For any A ~ D, we define fL( A) = LdE A fL( d). 1 Given a probability function fL, we can then define a dis­ crete probability function fL" on the product domain D" consisting of all n-tuples of elements of D by taking tL"(dl, ... , dn) = J-L(d!) X ... X J-L(d,.). Define a valuation to be a function mapping each object variable into an element of D and each field variable into an element of IR (the reals). Given a type 1 probability structure M and valuation v, we proceed by induction to associate with every object (resp. field) term t an element [t](M,w) of D (resp. IR), and with every formula <p a truth value, writing (111, v) f= <p if tl1e value true is associated with <p by (M, v). The definitions follow the lines of first-order logic, so we just give a few clauses of the definition here, leaving the remainder to the reader:

1 The restriction to discrete probability functions is made here for ease of exposition only. We can allow arbitrary prob­ a.bility functions on the domain by considering inner mea­ ~ure$, as is done in [FHl\188, FH89]. It might seem that for practical a.pplica.tions we should further restrict to uniform probability functions, i.e ., ones that assign equal probability to a.ll domain elements. Although we allow uniform probabil­ ity functions, and the language is expressive enough to a.llow us to say that the probability on the domain is uniform, we do not require them. There are a number of reasons for this . For one thing, there are no uniform probability functions in countable domains . (Such a probability function would have to assign probability 0 to each individual element in the do­ main, which means by countable additivity it would have to assign probability 0 to the whole doma.in .) And even if were­ strict attention to finite domains, we can construct two-sta.ge processes (where, for example, one of three urns is chosen at random, and then some ball in the chosen urn is chosen at random) where the most natural way to a.ssign probabilities would not assign equal probability to every ball [Ca.r50].

• (M, v) I= t1 = t2 iff [tdcM,·) = [t2](M,v)·
• (M, v) I= 'Vx 0 <p iff (!vf, v[x 0 ld]) I= <p for all d E D, where v[x 0 I dJ is the valuation which is identical to 11 except that it maps X 0 to d.
• [w(., 1 , ..· ,.,.)(<fJ)]{M,v) = tt"({(dl,····d,.): ( 1\f, v[xd d1, ... , x,. I d,.J) I= <p} ).

The major difference between our semantics and that of Bacchus is that Bacchus allows non~tandard probabil­ ity functions, that take values in arbitrary ordered fields, and are only finitely additive, not necessarily countably additive. Our probability functions are standard: they are real-valued and countably additive. (Bacchus allows such nonstandard probability functions in order to ob­ tain a complete axiomatization for his language. We return to this point later.)

We write M I= <p if ( M, v) I= <p for all valuations v, and write 1=1 cp, and say that <p i., valid with re~pect to type 1 ,,tructure~, if M I= <p for all type 1 probability structures M.

As an example, suppose the language has only one predicate, the binary predicate Son, and we have a structure M = ({a, b, c}, 1r, J.L) such that 1r(Son) consists of only the pair (a, b), JL(a.) = 113, JL(b) = 112, and tt(c) = 116. Let v be a valuation such that v(.r.) = a and v(y) = c. Then it is easy to check that we have [w.,(Son(x, y))](M,·) = 0, [wy(Son(x, y))](M,·) = 112, and [w(.r,y)(Son(x, y))](M,v) = 116. Thus, if we pick a random x from the domain and fix y to be c, the proba­ bility that x is a son of y is 0: no member of the domain is a son of c. If we fix x to be a and pick a y at random from the domain, the probability that x is a son of y is 112, which is exactly the probability that y = b. Finally, if we pick pairs at random from the domain, the proba­ bility of picking a pair ( x, y) such that x is a son of y is 116.

This example shows that the syntax and semantics of this logic are well suited for reasoning about statistical information. But, as discussed in the introduction, the logic is not well suited for making statements about de­ grees of belief about properties of particular individuals. It is easy to see that for any closed formula cp, such as Fly(Tweety ), we have Fl w..!( <p) = 0 V w.o!( <p) = 1 for any vector x of distinct variables. Thus, a formula such as .9 ~ wz(Flie.~(Tweety)) ~ .95 is guaranteed to be false. In order to make sense out of such formulas, we must put probabilities on possible worlds.

3 Probabilities on possible worlds

We have seen that in a precise sense type 1 probability structures are inappropriate for reasoning about degrees of belief. In practice, it might well be the case that the way we derive our degrees of belief is from the statistical information at ou.r disposal. For example, if we know that wx(Bird(x):::} Flies(x)) ~ .9 in a given structure, and we know that Tweety is a bird, then we might con­ clude that the probability that Tweety flies at least .9. However, as pointed out by Bacchus and others, this type of reasoning is fraught with difficulties. For example, if we have more specific information about Tweety, such as the fact that Tweety is a penguin, we no longer want to draw the conclusion that the probability that Tweety flies is at least .9. Bacchus provides some heuristics for deriving such degrees of belief. While this is a very in­ teresting topic to pursue, it also seems appropriate to construct a formal model that allows us to directly cap­ lure such degrees of belief. Such a formal model can be constructed in a straightforward way using possible worlds, as we now show.

The syntax for a logic for reasoning about possible worlds is essentially the same as the syntax used in the previous section. Starting with a set ci> of function and predicate symbols, we form more complicated formulas and terms as before except that instead of allowing prob­ ability terms of the form w.o!( <p ), where x is some vector of distinct object variables, we only allow probability terms of the form w( <p ), interpreted as "the probability of cp". Since we are no longer going to put a probabil­ ity distribution on the domain, it does not make sense to talk about the probability that a random choice for x will satisfy cp. It does make sense to talk about the probability of <p though: this will be the probability of the set of possible worlds where <p is true. We call the resulting language .C2( ci> ); if it includes equality between object terms, we call it .C2(cfl).

More formally, a type 2 probability ~tructure is a tuple (D, S, 1r, J.L), where D is a domain, S is a set of ~tate~ or poHihle world~, for each state s E S, 1r(.,) assigns to the predicate and function symbols in ci> predicates and functions of the right arity over D for each state s E S, and J.L is a discrete probability function on S. Note the key difference between type 1 and type 2 prob­ ability structures: in type 1 probability structures, the probability is taken over the domain D, while in type 2 probability structures, the probability is taken over the set S of states. Given a type 2 probability structure M, a state s, and valuation v, we can associate with ev­ ery object (resp. field) term t an element [t](M,·,·) of D (resp. m), and wit~ every formula <fJ_ a trut~ value, _writ­ ing (M, ,,, v) I= <p If the value true JS assoctated w1th <p by (M, s, v). Note that we now need the state to pro­ vide meanings for the predicate and function symbols; they might have different meanings in each state. Again, we just give a few clauses of the definition here, which should suffice to indicate the similarities and differences between type 1 and type 2 probability structures:

• (Af, .~, v) I= t1 = t2 iff [tdcM,·,·l = [t2](M,·,v)·
• (M, s, v) I= 'Vx 0 <p iff (M, ,,, v[x" ld]) I= <p for all dE D,
• [w(cp)](M,s,v) = p.({s' E S: (M,.,',v) I= cp}).

We say M I= <p if (.M, s, v) I= <p for all stales s in M and all valuations v, and say <p is valid with re~pect to type 2 ~tructure~, and write F2 cp, if M I= <p for all type 2 probability structures M.

As expected, in type 2 probability structures, it is completely consistent for the probability that Tweety flies to be between .9 and .95. A sentence such as .9 ~ w( Flie.,(Tweety)) ~ .95 is true in a structure M (independent of the state s) precisely if the set of states where Flie.~(Tweety) is true has probability between .9

and .95. However, there is no straightforward way to capture statistical information using £ 2 . 2

Possible extensions: We have made a number of sim­ plifying assumptions in our presentation of type 2 proba­ bility structures. We now briefly discuss how they might be dropped.

1. Just as in the case of type 1 probability structures, we can allow arbitrary probability functions, not just discrete ones, by using inner measures.
2. We have assumed that all functions and predicates are flexible, i.e., they may take on different mean­ ings at each state. We can easily designate some functions and predicates to be rigid, so that they take on the same meaning at all states.
3. We have assumed that there is only one domain. We could instead view each state 3 as a first-order structure, with its own domain D,. In this case, ?r( 3) would assign to each predicate and function symbol in ci> a predicate (resp. function) of the right arity on D,. Let D = u.EsD. U { ..l }, where ..l is a distinguished element not in u.EsD ·. We now take a valuation to be a function that associates with each field variable an element of IR, as before, and with each object variable an element of D. Given a predicate on D., we can view it as a predicate on D with the same extension. We can also ex­ tend an n-ary function f on D, to one on D by defining f(dl, ... , d,.) = ..l if some d; ~ D,. We can now define the semantics of terms and formu­ las in a straightforward way, along the same Jjnes as before. Note that universal quantification must be taken over the appropriate domain, so we have:

1. We have assumed that there is only one probability measure 11 on the set of states. We may want to allow uncertainty about the probability functions. We can achieve this by associating with each state a (possibly different) probability function on the set of states ( cf. (FII88, Hal89]). Thus a structure would now consist of a tuple (D, S, 1r, {11' : 3 E S} ); in order to evaluate the value of the (field) term w(cp) in a state 3, we use the probability function 11'.

4 Probabilities on the domain and on possible worlds

In the previous sections we have presented structures to capture two different modes of probabilistic reasoning.

2 We rema.rk that there is a sense in which we can trans­ late back and forth between domain-based probability and possible-world-based probability. For example, there is an ef­ fective translation that maps a formula cp in .c'! to a formula <p 1 in language £~, and a mn.pping from type 1 structures M to type 2 structure M' such that M F= cp iff M' F= cp'. Similar mappings exist in the other direction. (Details can be found in [AH89).) However , we would still argue that £1 is not the right language for reasoning about probability over possible worlds, while £2 is not the right language for reasoning about probability over the domain.

We do not want to say that one mode is more "right" than another; they both have their place. Clearly there might be situations where we want to do both modes of reasoning simultaneously. We consider three examples here.

Example 4.1: Consider the statement "the probability that Tweety files is greater than the probability that a random bird flies." This can be captured by the formula

Example 4.2: For a more complicated example, con­ sider two statements )jke "The probability that a ran­ dom bird flies is greater than .99" and "The probability that a random bird flies is greater than .9." An agent might consider the first statement rather unlikely to be true, and so take it to hold with probability less than .2, while he might consider the second statement exceeding likely to be true, and so take it to hold with probability greater than .95. We can capture this by combining the syntax of the previous two sections to get:

where a conditional statement such as w:r(Flie3(x) I BiTd(x)) > T is an abbreviation for w:r(Flie.,(x) A BiTd(x)) > Tw.,(BiTd(x)). 3

Example 4.3: A final example is given by Miller's principle (Sky80], which can be viewed as a way of con­ necting degrees of belief with probabilities on the do­ main. Perhaps the most obvious connection we can ex­ pect to hold between an agent's degree of belief in cp( a), for a particular constant a, and the probability that cp( x) holds for a random individual x is equality, as character­ ized by the following equation:

Miller's principle says something a little different; it says that for any real number r0 , the conditional probability of cp(a), given that the probability that a random x sat­ isfies cp is To, is itself T0 · Assuming that the real variable T does not appear free in cp, we can express (this instance of) Miller's principle in our notation as

'vVe examine the connection between Miller's principle and ( *) after we define our formal semantics.

Given a set ci> of function and predicate symbols let £ 3 ( ci>) be the language that results by allowing probabil­ ity terms both of the form wx( cp ), where xis a vector of distinct object variables, and of the form -w( cp ); we take £3' ( ci>) to be the extension of £ 3 ( ci>) that includes equal­ ity between object terms. To give semantics to formulas in £ 3 (1])) (resp. LJ'(ci>)), we will clearly need probabi]jty funclions over both the Ret of states and over the domain.

3 More typi cally, the conditional probability of A given B is taken to be the proba.bility of A n B divided by the probability of B . We have cleared the denominator here to avoid having to deal with the difficulty of dividing by 0 should the proba.bility of B be 0.

Let a type 3 probability ~tructure be a tuple of the form (D, S, 1r, Jl-D, Jl·s), where D, S, and 1r are as for type 2 probability structures, Jl-D is a discrete probability func­ tion on D and /l·S is a discrete probability function on S. Intuitively, type 3 structures are obtained by combining type 1 and type 2 structures.

Given a type 3 probability structure Af, a state s, and valuation v, we can give semantics to terms and formulas along much the same lines as in type 1 and type 2 structures. For example, we have:

• (w(%,, ... ,%.>(c,o)](M,·,v> = 11-v({(dt.····d,.): (M,.,,v[x!/d1,····xn/d,.]) F c,o}).
• (w(c,o)](M,·,v) = J.Ls({s' E S: (M,s',v) F= c,o}).

As it stands, in a given type 3 probability structure, we have one fixed probability function on the domain. This means that the truth of a formula such as w%(c,o(x)) = r is independent of the state; it is either true in all states or false in all states. Thus (using FJ to denote validity in type 3 structures) we immediately get:

Lemma 4.4:

This means that type 3 structures as we have defined them are not expressive enough to capture the intuition behind Example 4.2, since the conditional probability will be the same in all states. The only way for the agent to believe that the statement "The probability that a random bird flies is greater than .99" holds with prob­ ability less than .2 is for the statement to be false at all worlds (and thus hold with probability 0). Similarly, the only way for the agent to believe that the statement "The probability that a random bird flies is greater than .90" holds with probability greater than .95 is for it to be true at all possible worlds.

We can easily extend type 3 structures to deal with this problem. We simply allow the probability function on the domain to be a function on the state; thus at each state s we would have a (possibly different) probability function 11-b on the domain. When computing the value of a field term such as wx(c,o(x)) at states, we use the function Jl.v· With this change, a statement such as "The probabilty that a random bird flies is greater than . 99" can be true at some worlds and false at others, thus allowing us to better capture our intuitions here. Other extensions of type 3 structures, along the lines discussed for type 1 and type 2 structures, are possible as well.

In type 3 structures as we have defined them, there is a close connection between Miller's principle and ( * ). In fact, as the following theorem shows, they are equivalent. Proposition 4.5 : F3 (w(c,o(a)) wx(c,o(a:))] _ Vr[w(c,o(a) I (wx(c,o(x)) = r)) = r].

We remark that this result depends crucially on the fact that the probability on the domain is the same at every state. If we drop this assumption, then neither direction of the implication necessarily holds.

The idea of there being two types of probability has arisen in the literature before. Skyrms [SkyRO] talks about first- and second-order probabilities, where first­ order probabilities represent propensities or frequency­ essentially statistical information--while second-order probabilities represent degrees of belief. These are called first- and second-order probabilities since typically one has a degree of belief about statistical information (this is the case in our second example above). Although £3 ( ~) allows arbitrary alternation of the two types of probability, the semantics does support the intuition that these really are two fundamentally different types of probability.

5 On obtaining complete axiomatizations

In order to guide (and perhaps help us automate) our reasoning about probabilities, it would be nice to have a complete deductive system. Unfortunately, results of [AH89] show that in general we will not be able to ob­ tain such a system. We briefly review the relevant results here, and then show that we can obtain complete axiom­ atizations for important special cases.

5.1 Decidability and undecidability results

All the results in this subsection are taken from [AH89]. The first result is positive:

Theorem 5.1: If~ con.!i,,t,, only of unary predicatr..,, then the validity problem for £1(~) with re~pect to type 1 probability ,,tructure~ i., decidable.

The restrictions made in the previous result (to a lan­ guage with only unary predicates, without equality be­ tween object terms) are both necessary. Once we al­ low equality in the language, the validity problem is no longer recursively enumerable (r.e.), even if~ is empty. And a binary predicate in ~ is enough to guarantee that the validity problem is not r.e., even without equality between object terms.

Theorem 5.2:

1. For all~' the validity problem for £1(~) with re­ ~pect to type 1 ~tructure~ i~ not r.e.
2. If~ contain~ at lea~t one predicate of arity greater than or equal to two, then the validity problem for £1 (~) with re.,pect to type 1 probability .!tructure~ i~ not r.e .

Once we move to £ 2 , the situation is even worse. Even with only one unary predicates in~. the validity problem for £2 (~) is not r.e. If we have equality, then the validity problem is not r.e. as long as~ has at least one constant symbol. (Note that c,o ::::} ( w( c,o) = 1) is valid if c,o contains no nonlogical symbols- that is, c,o does not contain any function or predicate symbols, other than equality- so we cannot make any nontrivial probability statements if ~is empty.)

Theorem 5.3:

1. If~ contain., at lea~t one predicate of arity greater than or equal to one, then the validity problem for £2 (~) with re.,pect to type 2 probability ~tmcture~ i~ not r. e.
2. If ~ i~ nonempty, then the validity problem for £2(~) with re.,pect to type 2 probability structure,, i~ not r.e.

These results paint a rather discouraging picture as far as complete axiomatizations go. If a logic is to have a complete recursive axiomati:r.ation, then the set of valid formulas must be r.e. (we can enumerate them by just carrying out all possible proofs). Thus, for all the cases cited in the previous theorems for wh.ich the validity problem is not r.e., there can be no complete axiomatization. 4

There .is some good news in this bleak picture. In many applications it suffices to consider structures of size bounded by some N (or of size exactly N). In this case, we get decidability.

Theorem 5.4: If we re8trict to finite .,tructurc., of 11ize at mo8t N then, for all~. the validity problem for .C}(~) {relfp., £2(~), .CJ'(~)) with relfpect to type 1 {re8p., type 2, type 3) probability 8tructure8 i., decidable.

A fortiori, the same result holds if equality is not in the language. We also get decidability if we restrict to structures of size exactly N.

The restriction to bounded structures is necessary though.

Theorem 5.5: For all ~ (re&p., for all nonempty cp, for all~} the validity problem for .C}(~) {re.,p., .C2(cp), .CJ'(~)) with re&pect to type 1 (re8p., type 2, type 3) prob­ ability .,tructure., of finite lfize ilf not r.e.

5.2 An axiom system for probability on the domain

Although the previous results tell us that we cannot in general get a complete axiomatization for reasoning about probability, it is still useful to obtain a collection of sound axioms that lets us carry out much of our rea­ soning.

In order to carry out our reasoning, we will clearly need axioms for doing first-order reasoning. In order to reason about probabilities, which we take to be real num­ bers, we need the theory of real closed fields. An ordered field is a field with a linear ordering <. A real clo8ed field is an ordered field where every positive element has a square root and every polynomial of odd degree has a root. Tarski showed [Tar51, Sho67J that the theory of real closed fields coincides with the theory of the reals (for the first-order language with equality and nonlogi­ cal symbols +, x, >, 0, 1 ). That is, a first-order formula involving these symbols is true of the reals if and only if it is true in every real closed field. He also showed that the theory of real closed fields is decidable and has an elegant complete axiomatization. We incorporate this into our axiomatization too, since the language of real closed fields is a sublanguage of £ 1 ( ~ ).

Our axiom system for reasoning about probabilities on the domain, AX 1, includes the axioms of first-order logic, the axioms ofreal closed fields, and axioms for reasoning about probabilities, similar to those of [Bac88b, FHM88J. The axioms for reasoning about probability are:

4 We rema.rk that in (AH89J, the exact degree of undecid­ ability of the validity problem for a.! I these logics is completely chara.cterized . It turns out to be wildly undecidable, much harder than the validity problem for the first- order theory of a.rithmetic. We refer the reader to [AH89] for details.

Reasoning about probabilities over the domain:

• PD1 Vx1 ... Vx,.cp => W(x 1 , .·. ,x.)('P) 1, where (x1, ... , x,.) is a sequence of distinct object variables
• PD2 w..;(cp) ~ 0
• PD3 wx('P 1\ 7/J) + wz(cp 1\ -,?jJ) = w..;(cp) .
• PD4 w..;(cp) = Wi[x;fzl(cp[x;JzJ), where z is an object variable which docs not appear in x or cp
• PD5 w..;,g( cp 1\ 7/J) = w1( cp) x wg( 7/J ), if none of the free variables of cp are contained in fi, none of the free variables of 7/J are contained in x, and x and ii are disjoint

RPD 1 From fP ::::: 7/J infer w1( cp) = w1( 7/J)

Note that PD4 allows us to rename bound variables, while PD5 lets us do reasoning based on the indepen­ dence of the random variables. AX 1 is a straightforward extension of the axiom system used in [FHM88J for rea­ soning about the propositional case. Not surprisingly, it is also quite similar to the collection of axioms given in [Bac88bJ. Bacchus does not use the axioms for real closed fields, but instead he uses the axioms for ordered fields, since he allows his probability functions to take values in arbitrary ordered. fields. His axioms for reason­ ing about probabilities are essentially the same as ours (indeed, axioms PD1, PD2, and PD4 are also used by Bacchus, while PD5 is a weaker version of one of his axioms).

It is easy to check that these axioms are /found with respect to type 1 probability structures: if !tf is a type 1 probability structure, then 1\f f= cp for every axiom cp. By the results of Subsection 5.1, AX1 (or any other ax­ iom system!) cannot hope to be complete for £ 1 ( ~) once ~ has a predicate of arity at least two, nor can it be com­ plete for £"{'. However, if we restrict cp to consist only of unary predicates and do not have equality between object terms in the language, then it is complete.

Theorem 5.6: lf ~ conlfilft., only of unary predicate.,, then AX 1 ilf a /found and complete axiomatization for th e language £ 1 (~) with re,,pect to type 1 probability ~true­ lure~.

The previous result shows that AX 1 is rich enough to let us carry out a great deal of probabilistic reasoning. The next result reinforces this impression.

Let A X{" be AX 1 together with the following axiom, which says that the domain has size at most N:

Theorem 5. 7: AX{" i ., a /found and complete axiomati­ zation for .C}(~) with re~pect to type 1 probability 8truc­ ture8 of ~ize at mo&t N, for any ~et ~.

We can of course modify axiom FINN to say that the domain has exactly N elements, and get a complete ax­ iomati:r.ation with respect to structures of size exactly N. We can also get sound axiom systems AX2 and AX3 for reasoning about type 2 and type 3 structures respec­ tively. Again, they are not complete, but they are com­ plete with ,respect to structures of size at most Nonce we add FINN. We leave details to the full paper.

6 Conclusions

We have provided natural semantics to capture two dif­ ferent kinds of probabilistic reasoning: in one, the prob­ ability is on the domain, and in the other, the proba­ bility is on a set of possible worlds. We also showed how these two modes of reasoning could be combined in one framework. We then considered the problem of pro­ viding sound and complete axioms to characterize first­ order reasoning about probability. While complexity re­ sults of [AH89] show that in general there cannot be a complete axiomatization, we did provide sound axiom systems that we showed were rich enough to enable us to carry out a great deal of interesting probabilistic reason­ ing. In particular, together with an axiom guaranteeing finiteness, our axiom systems were shown to be complete for domains of bounded size.

Our results form an interest.ing contrast to those of Bacchus [Bac88b]. Bacchus gives a complete axiomati­ zation for his language (which, as we remarked above, is essentially the same as our language .C1 ( Cl>) for rea­ soning about probabilities on the domain), thus showing that the validity problem for his language is r.e. The reason for this difference is that Bacchus allows nonstan­ dard probability functions, which are only required to be finitely additive and can take values in arbitrary ordered fields. In [AH89] it is shown that all the undecidability results mentioned above can be proved even if we only require the probability function to be finitely additive, and restrict probabilities to taking only rational values. This shows that the key reason that Bacchus is able to obtain a complete axiomatization is that he allows prob­ abilities to take values in arbitrary ordered fields. 5

The situation here is somewhat analogous to that of axiomatizing arithmetic. Godel's famous incompleteness result shows that the first-order theory of arithmetic (for the language with equality and nonlogical symbols +, x, 0, 1, where the domain is the natural numbers) does not have a complete axiomatization. The axioms of Peano Arithmetic are sound for arithmetic, but not complete. They are complete with respect to a larger class of domains (including so-called non.!landard mod­ e[.,). Our results show that reasoning about probabilities is even harder than reasoning about arithmetic (since the validity problem for arithmetic is easier than Til), and so cannot have a complete axiomatization. However, Bac­ chus' axioms are complete with respect to a larger class of structures, where probabilities can assume nonstan­ dard values. And just as the axioms of Peano Arith­ metic are sufficiently rich to let us carry out a great deal of interesting arithmetic reasoning, so the axioms that we have provided (or the axioms of [Bac88b]) are suf­ ficiently rich to enable us to carry out a great deal of interesting probabilistic reasoning.

~Bacchus claims [Ba.c88b] that it is impossible to have a complete proof theory for countably additive probability functions. Although, as our results show, his claim is essen­ tially correct (at least, as long as the language contains one binary predicate symbol or equality), the reason that he gives for this claim, namely, that the corresponding logic is not compact, is not correct. For example , even if <Ji = {P}, where P is a unary predicate, the logic is not compact. (Consider the set {w.,(P(x)) "/: 0, w.,(P(x)) < 1/2, w.,(P(x)) < 1/3, w.,(P(x)) ~ 1/4, . .. }. Any finite subset of these formulas is satisfiable, but the full set is not .) However, by Theorem 5.6, the logic in this case has a complete axiomatization .

Acknowledgements

Discussions with Fahiem Bacchus provided the initial impetus for this work. I would like to thank Martin Abadi, Fahiem Bacchus, Ron Fagin, Hector Levesque, Joe Nunes, and Moshe Vardi for their helpful comments on earlier drafts.