We introduce and study counting propositional logic, an extension of propositional logic with counting quanti ers. This new kind of quanti cation makes it possible to express that the argument formula is true in a certain portion of all possible interpretations. We show that this logic, beyond admitting a satisfactory proof-theoretical treatment, can be related to computational complexity: the complexity of the underlying decision problem perfectly matches the appropriate level of Wagner's counting hierarchy.
Introduction
Counting Hierarchy
Among the many intriguing relationships existing between logic and computer
science, we can certainly mention the ones connecting classical propositional
logic (PL, for short), on the one hand, and computational complexity, the theory
of programming languages, and several other branches of theoretical computer
science, on the other. As it is well known, PL provided the rst example of a
nontrivial NP-complete problem [
Nevertheless, some aspects of the theory of computation have not found a
precise logical counterpart, at least so far. One such development concerns the
counting classes of complexity and the related counting hierarchy (CH, for short),
as introduced by Valiant [
In this paper we aim at bridging the gap by introducing a new quantied propositional logic, called counting propositional logic (CPL, for short). To present this logic in a more intuitive way, we start by de ning a univariate fragment of CPL, that we call CPL0, and we later describe the general, multivariate, logic CPL. The main feature of both these logics is the presence of counting quanti ers, which are designed to count the number of values of the bound propositional variables satisfying the argument formula. We study the proof theory of counting logics together with its relations to computational complexity. Along the way, we introduce a sound and complete proof system in the form of a single-sided sequent calculus on labelled formulas. We also establish complexity results for both univariate CPL0, the validity of which corresponds to P]SAT, and for multivariate CPL, whose decision problem characterizes the whole CH. Indeed, we prove that deciding (a special kind of) prenex normal forms is complete for the appropriate level of the hierarchy, in the spirit of the correspondence between quanti ed propositional logic (QPL, for short) and PH.
The presentation is structured as follows. First, we introduce the syntax,
semantics, and proof theory of counting logics. Speci cally, in Section 2 we present
a sound and complete proof system for CPL0, in the form of a labelled sequent
calculus. In the univariate case, the correspondence with computational
complexity is limited to the class P]SAT. In Section 3, we extend the calculus for
CPL0 to the multivariate counting logic CPL. Section 4 is devoted to
establishing the connection between counting logic and complexity theory, by relating
the decision problem for CPL with the hierarchy CH. The proof proceeds by a
careful analysis of prenex normal forms, which by construction have precisely
the shape one needs to match Wagner's complete problems [
On Univariate Counting Propositional Logic In this section we introduce a univariate version of counting propositional logic, called CPL0, together with a sound and complete proof system for it. Although this fragment has a limited expressive power, it provides an intuitive overview over the main semantical and proof-theoretical ingredients behind the more general logic CPL, introduced in the next section. Furthermore, the problem of establishing the validity of a CPL0-formula is proved to be in the class P]SAT. 2.1
CPL0-Formulae and their (Quantitative) Semantics
In the semantics of standard propositional logic the interpretation of a formula
is a truth-value. The core idea from which our counting logics arise is to replace
this way of interpreting formulas by a more quantitative semantics: the
interpretation of a formula will be the measurable set of all valuations that satisfy
it. Speci cally, since propositional formulas may have an arbitrary number of
propositional values, a valuation can be taken as an element of 2!; hence, given
a formula of CPL0, call it A, we may take as its interpretation the set JAK 2!
made of all maps f 2 2! \making A true". Such sets can be easily seen to belong
to the standard Borel algebra B(2!) over 2!, thus yielding a genuinely
quantitative semantics. In particular, atomic propositions are interpreted by cylinder
sets [
Cyl(i) = ff 2 2! j f (i) = 1g: and non-atomic propositions are naturally interpreted by relying on the standard -algebra operations of complementation, nite intersection and nite union.
Since a formula corresponds to a measurable set, it makes sense to enrich
the language of propositional logic with new formulas expressing conditions on
the measure of such sets. By adapting Wagner's notion of counting operator [
De nition 1 (Formulas of CPL0). The formulas of CPL0 are de ned by the following grammar:
A ::= i j :A j A ^ B j A _ B j CqA j DqA where i 2 N and q 2 Q[0;1].
In the following, let ( C) indicate the -algebra generated by the set of all
n-cylinders, which is the smallest -algebra containing C and which is Borel.
Moreover, let denote the standard cylinder measure over ( C), which can be
de ned as the unique measure on ( C) such that Cyl(i) = 12 , see [
J K
J:AK = 2! JAK JA ^ BK = JAK \ JBK JA _ BK = JAK [ JBK
J CqAK =
Two CPL0-formulas, A and B, are said logically equivalent, noted A B, when JAK = JBK. A formula A is valid when JAK = 2!.
The two counting quanti ers are inter-de nable, as can be easily shown semantically:
CqA :DqA
DqA :CqA: (1) Observe that they are not dual in the sense of standard modal operators: CqA is not equivalent to :Dq:A. Notably, using these quanti ers, it is even possible to express that a formula A is satis ed with probability strictly greater than q or with probability no smaller than q, as (resp.) D1 q:A and C1 q:A. The example below can help clarifying the intuitive meaning of the semantics of CPL0. 1 Example 1. Let us consider the counting formula C 2 A, where A = B _ C, Bme=as0ur^e :411aannddaCre=m:u0tu^al1ly. Tdhisejotiwnto. mHeeanscuer,able sets, JBK and JCK, both have 1 (JAK) 1= (JBK) + (JCK) = 12 , which means that JC 2 AK = 2!, and so the formula C 2 A is valid. 2.2
The Proof Theory of CPL0 We introduce a one-sided, single-succedent sequent calculus, and prove that it is sound and complete with respect to the semantics of CPL0. The language of this calculus is constituted by labelled formulas of the form b A or b A, where A and b are respectively a counting and a Boolean formula. Intuitively, a labelled formula b A (resp. b A) is true when the set of valuations satisfying b is included in (resp. includes) the interpretation of A. De nition 3 (Boolean Formulas). Boolean formulas are de ned by the following grammar:
b; c ::= xi j > j ? j :b j b ^ c j b _ c: where i 2 N. The interpretation of a Boolean formula b, JbK 2 B(2!), is inductively de ned as follows:
JxiK = Cyl(i) J>K = 2!
J?K = ; Labelled formulas are de ned as follows:
J:bK = 2! JbK Jb ^ cK = JbK \ JcK Jb _ cK = JbK [ JcK: De nition 4 (Labelled Formula). A labelled formula is an expression of one of the forms b A, b A, where b is Boolean formula and A is a counting formula. A labelled sequent is a sequent of the form ` L, where L is a labelled formula.
We also introduce a special class of formulas, that we call external hypotheses. Such formulas express semantic properties of Boolean formulas or conditions to be checked inside B(2!). In the following, we use b c as shorthand for JbK JcK. De nition 5 (External Hypothesis). An external hypothesis is either an expression of the form b c or of the form (JbK).q, where . 2 f ; >; ; <; =g, b; c are Boolean formulas and q 2 Q[0;1].
The measure of the interpretation of a Boolean formula, (JbK), can be related to the number ]SAT(b) of the valuations making b true as follows: Lemma 1. For each Boolean formula b containing the propositional variables x0; : : : ; xn 1, (JbK) = ]SAT(b) 2 n: Proof. Any valuation : fx0; : : : ; xn 1g ! 2 is associated to a measurable set X( ) 2 B(2!) by letting X( )=ff j 8i<nf (i) = (xi)g = Tin=01 Cyl(i) (xi), where Cyl(i) (xi) is Cyl(i) if (xi) = 1 and Cyl(i) otherwise. Observe that (X( )) = 2 n. For any b, we have that JbK = S b X( ) (this is easily checked by induction on b). Since for all distinct , 0, X( )\X( 0) = ;, we conclude that ]SAT(b) 2 n = P b 2 n = P b (X( )) = S b X( ) = (JbK).
The calculus is de ned by the rules in Figure 1. Let `CPL0 L indicate that ` L is derivable by the given rules. In Figure 2 we provide an example of derivation in CPL0.1 The use of external hypotheses, that is, of genuinely semantic conditions, as premisses of syntactic rules might seem somehow unsatisfactory. However, such premisses do make sense from a computational viewpoint: they correspond to the idea that, when searching for a proof of a counting formula, one might need to call for an oracle for values of the form (JbK) in fact, by Lemma 1, an oracle for ]SAT(b) . This intuition will be made clear in the next subsection, where we discuss an algorithm for CPL0-validity.
A labelled formula b A (resp. b A) is valid, noted b A (resp. b A), when JbK JAK (resp. JAK JbK). A sequent ` L is valid when L. As anticipated, the proof system just introduced is sound and complete with respect to the semantics of CPL0: a labelled formula is valid if and only if it is provable. Soundness can be established by a standard induction on the derivation height. The proof of completeness is less straightforward and described in full detail in [1, x A.2]. The fundamental ingredient is the introduction of a decomposition relation between nite sets of sequents, which allows one to decompose the validity of a complex statement (for example, b A _ B) into that of a nite set of less complex statements (such as, c A; d B, given that b c_ d holds). One can show then that a complex valid sequent is decomposable into a nite set of non-decomposable valid sequents, and, from the provability of the latter, climb back to the validity of the original sequent using the rules of CPL0.
1 Observe that the last four counting rules in Fig. 1 make an arbitrarily chosen label b appear in the conclusion. Intuitively, this is coherent with the semantics of counting formulas, which are interpreted as either 2! or ;, which are (resp.) superset or subset of any given set.
b xn ` b
n Ax1 ` c
A
` c ` b A ` b ` bA _ B
B ` b A ^ B ` d ` b
A ` b R1_
R1^ ` c ` c
A ` b A ` b `(JbbK) =A0 R
(JcK) q CqA
(JcK) < q DqA
A A :A b :c R : ` b ` b
` b ` b RC RD b c _ d R Fig. 2. Derivation of ` >
C 21 (0 ^ :1) _ (:0 ^ 1) in CPL0 As suggested before, a proof that a quanti ed formula like CqA or DqA is valid can be seen as obtained by invoking an oracle, which provides a suitable measurement (JbK), for a Boolean formula b. As shown by Lemma 1, these measurements correspond to actually counting the number of valuations satisfying the corresponding formula. It is possible to make this intuition precise by showing that, in CPL0, validity can be decided by a polytime algorithm having access to an oracle for the problem ]SAT of counting the models of a Boolean formula.
A formula of CPL0, call it A, is said to be closed if it is either of the form CqB or DqB or it is a negation, conjunction, or disjunction of closed formulas. It can be easily checked by induction on the structure of closed formulas that for any closed A, either JAK = 2! or JAK = ;. We de ne, by mutual recursion, two polytime algorithms Bool and Val: for each formula A of CPL0, Bool(A) computes a Boolean formula bA such that JAK = JbAK, and, for all closed formula A, Val(A) = 1 if and only if JAK = 2! and Val(A) = 0 if and only if JAK = ;. The two algorithms are de ned in Figure 3. Notice that the algorithm Val makes use of a ]SAT oracle.
We recall that the class P]SAT is made of those problems which can be decided in polytime having access to a ]SAT oracle. One can easily be convinced that the algorithms Bool and Val both belong to P]SAT, which leads to the following:
Bool(n) = xn Bool(A1 ^ A2) = Bool(A1) ^ Bool(A2) Bool(A1 _ A2) = Bool(A1) _ Bool(A2)
Bool(:A1) = :Bool(A1) Bool(CqA1) = Val(CqA1) Bool(DqA1) = Val(DqA1) Val(A1 ^ A2) = Val(A1) AND Val(A2) Val(A1 _ A2) = Val(A1) OR Val(A2)
Val(:A1) = NOT Val(A1) Val(CqA1) = let b = Bool(A1) in let n = ]Val(b) in
]SA2Tn(b) q Val(DqA1) = let b = Bool(A1) in let n = ]Val(b) in ]SA2Tn(b) < q where ]Val(b) is the number of propositional variables in b.
On Multivariate Counting Propositional Logic In this section we introduce propositional counting logic CPL, which extends counting quanti ers to a multivariate case, as discussed below. In Section 4 it will be shown that this logic yield a characterization of the full counting hierarchy.
As it is well-known, counting problems are not restricted to those in P]SAT.
For instance, one can consider problems concerning relations between valuations
of di erent groups of variables, like MajMajSAT [
To express these kinds of problems, we will consider a language in which propositional atoms and counting quanti ers are named (we use a; b; c; : : : for names); counting quanti cations, indicated as CqaA or DqaA, now depend on the number of valuations of propositional atoms with name a satisfying A. De nition 6 (Formulas of CPL). The formulas of CPL are de ned by the following grammar:
A ::= ia j :A j A ^ B j A _ B j CqaA j DqaA where i 2 N, a is a name, and q 2 Q[0;1].
Named quanti ers, Cqa and Dqa, bind the occurrences of the name a in A. Given a formula A of CPL, we let FN(A) indicate the set of names occurring free (i.e. not bound) in A.
Names can be used to distinguish between distinct groups of propositional variables. For example, the propositional formula F = (x1 _ y1) ^ (x2 _ y2), containing two groups of variables x = fx1; x2g and y = fy1; y2g, can be expressed in CPL using two distinct names a; b as G = (1a _ 1b) ^ (2a _ 2b). Since the intuitive meaning of CqaA is that A is true in at least q of the valuations of 1 1 the variables with name a, we can take the CPL-formula Ca2 Cb2 G as expressing the MajMajSAT problem for F (which happens to have a positive answer, in this case).
While the formulas CqaA and DqaA have a rather intuitive meaning, the semantics of CPL-formulas is slightly subtler than in the case of CPL0. The interpretation of a formula A now depends on the choice of a nite set of names X FN(A), and consists in a measurable set A X belonging to the Borel algebra B (2!)X . Hence, the quanti ers Cqa and DJqaKmust correspond to operations allowing one to pass from B (2!)X[fag to B (2!)X . To de ne such operations we need the following technical notion: given two disjoint nite sets of names X; Y , for any f 2 (2!)X , and X (2!)X[Y , the f -projection of X is the set f (X ) = fg 2 (2!)Y j f + g 2 X g (2!)Y , where (f + g)( ) is f ( ), if 2 X and g( ) if 2 Y .
De nition 7 (Semantics of CPL). For each formula A of CPL, and nite set of names such that X FN(A), the interpretation of A, JAKX (2!)X , is inductively de ned as follows:
JiaKX = ff j f (a)(i) = 1g JA ^ BKX = JAKX \ JBKX JA _ BKX = JAKX [ JBKX
J:AKX = (2!)X JCqaAKX = ff j JDqaAKX = ff j
A X
J K f (JAKX[fag)
qg ( f (JAKX[fag) < qg: That all sets JAKX are measurable, namely that JAKX 2 B (2!)X , is not an obvious fact (as it crucially relies on some properties of f -projections), and is proved in detail in [1, x 4]. Logical equivalence in CPL is de ned relatively to a set of names X, by letting A X B if and only if FN(A); FN(B) X and JAKX = JBKX .
Similarly to what has been shown in the previous section, one can introduce a sound and complete labelled calculus for CPL. In this case, labelled formulas involve a named Boolean formula (i.e, built from named Boolean variables, such as xia). Sequents are of the form `X L, with FN(L) X. Most rules of CPL are straightforward generalizations of those for CPL0, except for the counting rules, which are understandably more complex (see the example in Figure 4), and rely on the notion of a-decomposition for Boolean formulas.2 In spite of this involved de nition, soundness and completeness for this calculus can be still proved generalizing the corresponding arguments for CPL0.
`X[fag c
A
b X Wifei j (JdiKfag) qg RC *
`X b CqaA
* where Wi ei ^ di is an a-decomposition of c
We have already seen that the problem MajMajSAT, which is complete for CH2 =
PPPP, is \captured" by formulas of the form CqaCbrA, where A is quanti
erfree. We will extend this result to all levels of CH by considering CPL-formulas
containing an arbitrary number of counting quanti ers. We will proceed in three
steps. First, we will show that any formula of CPL can be put in prenex normal
form, that is, that all counting quanti ers can be moved at top-level. Next, we
will prove that the D quanti er, which has no counterpart in Wagner's problems,
can be eliminated. Finally, using Wagner's Theorem [
The existence of deep and mutual interactions between classical propositional
logic and computational complexity is well-known. For instance, checking the
satis ability of PL-formulas is the paradigmatic NP-complete problem [
Nevertheless, if we move to a probabilistic framework, such a plain
correspondence seems lost, as no analogous logical counterpart has yet been found
for the counting complexity classes and hierarchy, introduced from the 1970s
on by Valiant [
In the rest of this section we will relate such results to CPL, showing that the validity of the formulas of CPL yields a new family of complete problems for CHn, hence providing a logical characterization of CH. 4.2
Prenex Normal Forms Let us introduce prenex normal forms in the language of CPL: De nition 8 (PNF). A formula of CPL is an n-ary prenex normal form (or simply a prenex normal form, PNF for short) if it can be written as 41 : : : 4nA, where, for every i 2 f1; : : : ; ng, 4i is either Cqa or Dqa (for arbitrary a and q), and A is quanti er-free. The formula A is said to be the matrix of the PNF. To convert a formula of CPL into an equivalent PNF, some intermediate lemmas are needed.3 Preliminarily, notice that for every formula A of CPL, name a, and nite set X, such that FN(A) X and a 62 X, if q = 0, then JCqaAKX = (2!)X and JDqaAKX = ;X .
The lemma below shows that counting quanti ers occurring inside any conjunction or disjunction can be extruded from it.
Lemma 2. Let a 62 FN(A) and q > 0. Then, for every X such that FN(A) [ FN(B) X and a 62 X, the following equivalences hold:
X Cqa(A ^ B)
X Dqa(:A _ B) 3 Their proofs can be found in [1, x C].
Remarkably, a corresponding lemma does not hold for CPL0, due to the impossibility of renaming variables (on which Lemma 2 relies).
We then consider negation. In this case, the inter-de nability of Cq and Dq in CPL0 (Equation 1) can be generalized to CPL, and this allows one to get rid of negations which lie between any occurrences of a counting quanti er and the formula's root.
Lemma 3. For every q 2 Q[0;1], name a, and X such that FN(A) and a 62 X, :DqaA X CqaA and :CqaA X DqaA hold.
X [ fag, Therefore, using Lemma 2 and Lemma 3, we can conclude that every formula of CPL can be put in PNF, as desired.
Proposition 3. For every formula A of CPL there is a PNF B, such that for every X with FN(A)[FN(B) X, A X B holds. Moreover, B can be computed in polynomial time from A. 4.3
Positive Prenex Normal Forms Reducing formulas to PNF is close to what we need, but there is one last step to make, namely getting rid of the quanti er D, which does not have any counterpart in Wagner's construction. In other words, we need to reduce CPL-formulas to prenex normal forms of a special kind : De nition 9 (PPNF). A formula of CPL is said to be a positive prenex normal form (PPNF, for short) when it is both PNF and D-free.
The gist to convert formulas into (equivalent) PPNF, consists in two main steps: (i) converting each instance of D into one of C, using Lemma 3, and (ii) applying the lemma below which states that C enjoys a speci c, weak form of self duality, to push the negation inside the matrix.
Lemma 4 (Epsilon Lemma). For every formula A of CPL and q 2 Q[0;1], there is a p 2 Q[0;1] such that, for every X with FN(A) X and a 62 X: :CqaA X Cpa:A: Moreover, p can be computed from q in polynomial time. Proof (Sketch4). Let bA be a Boolean formula satisfying JAKX[fag = JbAKX[fag, a-decomposable as Win di ^ ei, and let k be maximum such that xka occurs in bA. Let [0; 1]k be the set of those rational numbers r 2 [0; 1] which can be written as a nite sum of the form Pk
i=0 bi 2i. For all i 2 f0; : : : ; ng, (JdiKfag) 2 [0; 1]k, where bi 2 f0; 1g, and for all f : X ! 2!, also f (JAKX[fag) 2 [0; 1]k. Let now be 2 (k+1) if q 2 [0; 1]k and q 6= 1, be 2 (k+1) if q = 1 and let = 0 if q 62 [0; 1]k. In all cases, q + 62 [0; 1]k so, by means of some simple computation, 1 (q+ ):AKX : it is possible to conclude that J:CqaAKX = JCa Actually, the value of p is very close to 1 q, the di erence between the two being easily computable from the formula A. So, any negation occurring in the counting pre x of a PNF formula, can be pushed back into the matrix. 4 For full details, see [1, Lemma 13].
Proposition 4. For every formula A of CPL there is a PPNF B such that for every X, with FN(A) [ FN(B) X, A X B holds. Moreover, B can be computed from A in polynomial time. 4.4
CPL and the Counting Hierarchy
As anticipated, in [
Suppose L to be a subset of Sn, where S is a set, that 1 m < n, and that
b 2 N. We de ne CbmL as the following subset of Sn m:
f(an; : : : ; am+1) j #(f(am; : : : ; a1) j (an; : : : ; a1) 2 Lg)
bg :
Let T and F indicate the usual true and false formulas of PL. For any natural
number n 2 N, let T F n be the subset of PLn+1 containing all tuples in the form
(A; t1; : : : ; tn), where A is a propositional formula in CNF with at most n free
variables, and t1; : : : ; tn 2 fT; Fg render A true. Finally, for every k 2 N, we
denote as W k the language consisting of all (binary encodings of) tuples of the
form (A; m1; : : : ; mk; b1; : : : ; bk) such that A 2 Cbm11 Cbmkk T F P mi .
Theorem 1 (Wagner, Th.7 [
Observe that elements of W k can be seen as alternative representations for PPNF formulas of CPL, once any mi is replaced by minf1; 2mbii g. Consequently, Corollary 1. The closed and valid k-ary PPNFs, whose matrix is in CNF, dene a complete set for CHk. 5
Related Works
The literature on logics enabling some forms of probabilistic reasoning is vast,
yet most proposals are not related to computational aspects. In the last decades,
several probabilistic logics have been developed in the realm of modal logic,
starting from the pioneering works by Nilsson [
As we have seen, CH was rst de ned by Wagner in [
Conclusion To the best of our knowledge, CPL is the rst logical system extending propositional logic with counting quanti ers. Our main source of inspiration comes from computational complexity, namely from Wagner's counting operator on classes. By the way, we believe that the main contribution of the paper is not the introduction of counting logics per se, but the investigation of its connections with counting classes. Indeed, we have shown that counting quanti ers play nicely with propositional logic in characterizing CH, and thus relate nicely with some old and recent results in complexity theory. In our opinion, CPL naturally appears as the probabilistic counterpart of QPL.
Due to space reasons, we left out some important applications of counting
logics to other branches of computer science, such as the theory of programming
languages. In particular, it is possible to design type systems for the randomized
-calculus by extending simple types with counting quanti ers,5 and to de ne a
probabilistic counterpart of the Curry-Howard correspondence [