On Counting Propositional Logic and Wagner’s Hierarchy? ?? Melissa Antonelli, Ugo Dal Lago, and Paolo Pistone Università di Bologna {melissa.antonelli2,ugo.dallago,paolo.pistone2}@unibo.it Abstract. We introduce and study counting propositional logic, an ex- tension of propositional logic with counting quantifiers. This new kind of quantification 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 underly- ing decision problem perfectly matches the appropriate level of Wagner’s counting hierarchy. Keywords: Propositional Logic · Counting Hierarchy · Computational Com- plexity 1 Introduction 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 first example of a nontrivial NP-complete problem [11]; moreover, formal systems for classical and intuitionistic propositional logic correspond to type systems for λ-calculi and re- lated formalisms [16, 34]. These lines of research have further evolved in various directions, resulting in active sub-areas of computer science. In particular, vari- ations of propositional logic have been put in relation with complexity classes other than P and NP, as well as with type systems other than the simply typed λ-calculus. For instance, the complexity of deciding quantified propositional for- mulas is well known to match the appropriate level of the polynomial hierarchy (PH, for short) [27, 28, 35, 42, 10]. Nevertheless, some aspects of the theory of computation have not found a precise logical counterpart, at least so far. One such development concerns the ? Copyright c 2021 for this paper by its authors. Use permitted under Creative Com- mon License Attribution 4.0 International (CC BY 4.0). ?? Supported by ERC CoG “DIAPASoN”, GA 818616 and ANR PRC project “PPS”, ANR-19-CE48-0014. 2 M. Antonelli et al. counting classes of complexity and the related counting hierarchy (CH, for short), as introduced by Valiant [38] and Wagner [39–41], which are deeply connected to randomized complexity classes, such as PP. In fact, Wagner’s CH has been treated logically by means of tools from descriptive complexity and finite model theory [22]. However, to the best of the authors’ knowledge, there is no counter- part of counting classes in the realm of propositional logic. In this paper we aim at bridging the gap by introducing a new quanti- fied propositional logic, called counting propositional logic (CPL, for short). To present this logic in a more intuitive way, we start by defining a univari- ate 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 quantifiers, 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 quantified propositional logic (QPL, for short) and PH. The presentation is structured as follows. First, we introduce the syntax, se- mantics, and proof theory of counting logics. Specifically, 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 com- plexity 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 establish- ing 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 [40]. 2 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 gen- eral 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 On Counting Propositional Logic and Wagner’s Hierarchy 3 this way of interpreting formulas by a more quantitative semantics: the inter- pretation of a formula will be the measurable set of all valuations that satisfy it. Specifically, 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ω “making A true”. Such sets can be easily seen to belong to the standard Borel algebra B(2ω ) over 2ω , thus yielding a genuinely quanti- tative semantics. In particular, atomic propositions are interpreted by cylinder sets [8] of the following form: Cyl(i) = {f ∈ 2ω | f (i) = 1}. and non-atomic propositions are naturally interpreted by relying on the standard σ-algebra operations of complementation, finite intersection and finite 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 [40, 41], we introduce two quantifiers, Cq , Dq , where q ranges over Q[0,1] , so that the formulas Cq A and Dq A express that A is satisfied by a given portion of all its 1 possible interpretations. For example, the formula C 2 A expresses the fact that A is satisfied by at least half of its valutations, namely A is true with probability at 3 least 12 . Equally, the formula D 4 A expresses the fact that A is satisfied by strictly less than three-fourths of its valutations, meaning that the probability for A to be true is strictly smaller than 34 . Semantically, this amounts at respectively 1 checking that µ JAK ≥ 2 and µ JAK < 34 , where µ is the standard Borel   measure on B(2ω ). Definition 1 (Formulas of CPL0 ). The formulas of CPL0 are defined by the following grammar: A ::= i | ¬A | A ∧ B | A ∨ B | Cq A | Dq A where i ∈ N and q ∈ 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 defined as the unique measure on σ( C) such that µ Cyl(i) = 21 , see [8]. Definition 2 (Semantics of CPL0 ). For each formula A of CPL0 its inter- pretation is the measurable set, JAK ∈ B(2ω ), inductively defined as follows: ( JiK = Cyl(i) q 2ω if µ(JAK) ≥ q ω JC AK = J¬AK = 2 − JAK ∅ otherwise JA ∧ BK = JAK ∩ JBK ( q 2ω if µ(JAK) < q JA ∨ BK = JAK ∪ JBK JD AK = ∅ otherwise. 4 M. Antonelli et al. 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 quantifiers are inter-definable, as can be easily shown se- mantically: Cq A ≡ ¬Dq A Dq A ≡ ¬Cq A. (1) Observe that they are not dual in the sense of standard modal operators: Cq A is not equivalent to ¬Dq ¬A. Notably, using these quantifiers, it is even possible to express that a formula A is satisfied 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, B = 0 ∧ ¬1 and C = ¬0 ∧ 1. The two measurable sets, JBK and JCK, both have measure 14 and are mutually disjoint. Hence, µ(JAK) = µ(JBK) + µ(JCK) = 12 , 1 1 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. Definition 3 (Boolean Formulas). Boolean formulas are defined by the fol- lowing grammar: b, c ::= xi | > | ⊥ | ¬ b | b ∧ c | b ∨ c. where i ∈ N. The interpretation of a Boolean formula b, J bK ∈ B(2ω ), is induc- tively defined as follows: Jxi K = Cyl(i) J¬ bK = 2ω J bK ω J>K = 2 J b ∧ cK = J bK ∩ J cK J⊥K = ∅ J b ∨ cK = J bK ∪ J cK. Labelled formulas are defined as follows: Definition 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 J bK ⊆ J cK. On Counting Propositional Logic and Wagner’s Hierarchy 5 Definition 5 (External Hypothesis). An external hypothesis is either an expression of the form b  c or of the form µ(J bK).q, where . ∈ {≥, >, ≤, <, =}, b, c are Boolean formulas and q ∈ Q[0,1] . The measure of the interpretation of a Boolean formula, µ(J bK), 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 , µ(J bK) = ]SAT( b) · 2−n . Proof. Any valuation θ : {x0 , . . . , xn−1 } → 2 is associated to a measurable set Tn−1 X(θ) ∈ B(2ω ) by letting X(θ)={f | ∀i  C 2 (0 ∧ ¬1) ∨ (¬0 ∧ 1) *as µ J(x0 ∧ ¬x1 ) ∨ (¬x0 ∧ x1 )K ≥ 1  2 1  Fig. 2. Derivation of ` >  C 2 (0 ∧ ¬1) ∨ (¬0 ∧ 1) in CPL0 2.3 CPL0 -Validity is in P]SAT As suggested before, a proof that a quantified formula like Cq A or Dq A is valid can be seen as obtained by invoking an oracle, which provides a suitable measurement µ(J bK), for a Boolean formula b. As shown by Lemma 1, these On Counting Propositional Logic and Wagner’s Hierarchy 7 measurements correspond to actually counting the number of valuations satis- fying 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 Cq B or Dq B 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 define, 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 = J bA K, 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 defined 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: Proposition 2. CPL0 -validity is in P]SAT . Bool(n) = xn Val(A1 ∧ A2 ) = Val(A1 ) AN D Val(A2 ) Bool(A1 ∧ A2 ) = Bool(A1 ) ∧ Bool(A2 ) Val(A1 ∨ A2 ) = Val(A1 ) OR Val(A2 ) Bool(A1 ∨ A2 ) = Bool(A1 ) ∨ Bool(A2 ) Val(¬A1 ) = N OT Val(A1 ) Bool(¬A1 ) = ¬Bool(A1 ) q Val(C A1 ) = let b = Bool(A1 ) in q q Bool(C A1 ) = Val(C A1 ) let n = ]Val( b) in q q Bool(D A1 ) = Val(D A1 ) ]SAT( b) ≥q 2n q Val(D A1 ) = let b = Bool(A1 ) in let n = ]Val( b) in ]SAT( b) 0. Then, for every X such that FN(A) ∪ FN(B) ⊆ X and a 6∈ X, the following equivalences hold: A ∧ Cqa B ≡X Cqa (A ∧ B) A ∨ Cqa B ≡X Cqa (A ∨ B) A ∧ Dqa B ≡X Dqa (¬A ∨ B) A ∨ Dqa B ≡X Dqa (¬A ∧ B). 3 Their proofs can be found in [1, § C]. On Counting Propositional Logic and Wagner’s Hierarchy 11 Remarkably, a corresponding lemma does not hold for CPL0 , due to the impos- sibility of renaming variables (on which Lemma 2 relies). We then consider negation. In this case, the inter-definability 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 quantifier and the formula’s root. Lemma 3. For every q ∈ Q[0,1] , name a, and X such that FN(A) ⊆ X ∪ {a}, and a 6∈ X, ¬Dqa A ≡X Cqa A and ¬Cqa A ≡X Dqa A hold. 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 quantifier D, which does not have any counter- part in Wagner’s construction. In other words, we need to reduce CPL-formulas to prenex normal forms of a special kind : Definition 9 (PPNF). A formula of CPL is said to be a positive prenex nor- mal 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 specific, weak form of self duality, to push the negation inside the matrix. Lemma 4 (Epsilon Lemma). For every formula A of CPL and q ∈ Q[0,1] , there is a p ∈ Q[0,1] such that, for every X with FN(A) ⊆ X and a 6∈ X: ¬Cqa A ≡X Cpa ¬A. Moreover, p can be computed from q in polynomial time. Proof (Sketch4 ). Let WnbA be a Boolean formula satisfying JAKX∪{a} = J bA KX∪{a} , a-decomposable as i 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 ∈ [0, 1] which can be written as Pk a finite sum of the form i=0 bi · 2i . For all i ∈ {0, . . . , n}, µ(J diK{a} ) ∈ [0, 1]k , where bi ∈ {0, 1}, and for all f : X → 2ω , also µ Πf (JAKX∪{a} ) ∈ [0, 1]k . Let now  be 2−(k+1) if q ∈ [0, 1]k and q 6= 1,  be 2−(k+1) if q = 1 and let  = 0 if q 6∈ [0, 1]k . In all cases, q +  6∈ [0, 1]k so, by means of some simple computation, 1−(q+) it is possible to conclude that J¬Cqa AKX = JCa ¬AKX . Actually, the value of p is very close to 1 − q, the difference between the two being easily computable from the formula A. So, any negation occurring in the counting prefix of a PNF formula, can be pushed back into the matrix. 4 For full details, see [1, Lemma 13]. 12 M. Antonelli et al. 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 [40] Wagner not only introduced his counting operator and hierarchy, but also defined complete problems for each level of CH. Below, we present a slightly weaker version of Wagner’s Theorem [40, pp. 338-339], which perfectly fits our needs. Suppose L to be a subset of S n , where S is a set, that 1 ≤ m < n, and that b ∈ N. We define Cbm L as the following subset of S n−m : {(an , . . . , am+1 ) | #({(am , . . . , a1 ) | (an , . . . , a1 ) ∈ L}) ≥ b} . Let T and F indicate the usual true and false formulas of PL. For any natural number n ∈ 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 ∈ {T, F} render A true. Finally, for every k ∈ N, we denote as W k the language consisting of all (binary encodings P of) tuples of the form (A, m1 , . . . , mk , b1 , . . . , bk ) such that A ∈ Cbm11 · · · Cbmkk T F mi . Theorem 1 (Wagner, Th.7 [40]). For every k, the language W k is complete for CHk . Observe that elements of W k can be seen as alternative representations for PPNF formulas of CPL, once any mi is replaced by min{1, 2mbii }. Consequently, Corollary 1. The closed and valid k-ary PPNFs, whose matrix is in CNF, de- fine 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 [30, 31]. In particular, in the 1990s, some noteworthy probability logics were (independently) introduced both by Bacchus [6, 4, 5] and by Fagin, Halpern, and Megiddo [14, 18, 13, 19]. Another class of probabilistic modal logics have been designed to model Markov chains and similar structures, see for instance [20, 23, 24]. A notable example is Riesz modal logic [15], which admits a sound and complete proof system. Remarkably, this is the only sequent calculus for probability logic we are aware of, while complete axiomatic systems have been provided for both the probability logics quoted above [6, 14]. By the way, our calculi are actually inspired by labelled systems, such as G3K∗ and G3P∗ , as presented for example in [29, 17]. On Counting Propositional Logic and Wagner’s Hierarchy 13 As we have seen, CH was first defined by Wagner in [39, 41, 40] and, inde- pendently, by Pareberry and Schnitger [33]. It was conceived as an extension of Meyer and Stockmeyer’s PH [27, 28] aiming at characterizing natural prob- lems in which counting is involved. There are two main, equivalent [37] ways to define CH: the original characterization in terms of alternating quantifiers [40], and the one based on oracles [36]. Notably, Wagner’s operator was not the only “probabilistic” (class) quantifiers introduced in the 1980s (consider, for instance, Papadimitriou’s probabilistic quantifier [32], Zachos and Heller’s random quanti- fier [44], or Zachos’ overwhelming and majority quantifiers [43]). However, to the best of the authors’ knowledge, all these operators are counting quantifiers on (classes of) languages, rather than stricto sensu logical ones. One remarkable ex- ception is represented by Kontinen’s work [22], in which second-order quantifiers are defined in the style of descriptive complexity. 6 Conclusion To the best of our knowledge, CPL is the first logical system extending propo- sitional logic with counting quantifiers. 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 connec- tions with counting classes. Indeed, we have shown that counting quantifiers 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 quantifiers,5 and to define a probabilistic counterpart of the Curry-Howard correspondence [16, 34] relating typing derivations with derivations in CPL.6 Moreover, the proof theory of CPL has just been briefly delineated and the dynamics (i.e. the cut-elimination proce- dure) of the introduced formal systems deserves further investigation. Promising results also concern the possibility to inject “counting” quantifiers into the lan- guage of arithmetic. In particular, in [2] we have investigated an extension of standard Peano Arithmetics with measure quantifiers, which can be seen as a natural generalization of the quantifiers of CPL0 to the language of arithmetic. The extension of counting quantifiers to arithmetic looks particularly promising, as it suggests ways of characterizing in a “logical” way explicit lower bounds for counting problems [26], as well as the possibility of defining new logical systems capturing probabilistic complexity classes like BPP (see [21]). 5 Notice that while several type systems for randomized λ-calculi and guaranteeing various forms of termination properties have been introduced in the last years, [12, 9, 3], none of these systems is explicitly logic-oriented. 6 Some achievements in this direction have been presented in [1, § 6]. 14 M. Antonelli et al. References 1. Antonelli, M., Dal Lago, U., Pistone, P.: On Counting Propositional Logic (2021), available at: https://arxiv.org/abs/2103.12862 2. Antonelli, M., Dal Lago, U., Pistone, P.: On Measure Quantifiers in First-Order Arithmetic (2021), to appear in Proceedings of Computability in Europe 2021 (CiE2021); long version available at: https://arxiv.org/abs/2104.12124 3. Avanzini, M., Dal Lago, U., Ghyselen, A.: Type-based complexity analysis of prob- abilistic functional programs. In: Proceedings of the 34th Annual ACM/IEEE Sym- posium on Logic in Computer Science (LICS). pp. 1–13. IEEE, Vancouver, BC, Canada, Canada (2019) 4. Bacchus, F.: Lp, a logic for representing and reasoning with statistical knowledge. Computational Intelligence 6(4), 209–231 (1990) 5. Bacchus, F.: On probability distributions over possible worlds. Machine Intelligence and Pattern Recognition 9, 217–226 (1990) 6. Bacchus, F.: Representing and Reasoning with Probabilistic Knowledge. MIT Press (1990) 7. Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability. IOS Press (2009) 8. Billingsley, P.: Probability and Measure. Wiley (1995) 9. Breuvart, F., Dal Lago, U.: On intersection types and probabilisitic lambda calculi. In: PPDP ’18: Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming. pp. 1–13. No. 8 (2018) 10. Büning, H., Bubeck, U.: Theory of quantified Boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. IOS Press (2009) 11. Cook, S.: The complexity of theorem-proving procedures. In: STOC ’71. pp. 151– 158 (1971) 12. Dal Lago, U., Grellois, U.: Probabilistic termination by monadic affine sized typing. ACM Trans. Program. Lang. Syst. 41(2), 10–65 (2019) 13. Fagin, R., Halpern, J.: Reasoning about knowledge and probability. Journal of ACM 41(2), 340–367 (1994) 14. Fagin, R., Halpern, J., Megiddo, N.: A logic for reasoning about probabilities. Inf. Comput. 87(1/2), 78–128 (1990) 15. Furber, R., Mardare, R., Mio, M.: Probabilistic logics based on Riesz spaces. LMCS 16(1) (2020) 16. Girard, J.Y.: Proof and Types. Cambridge University Press (1989) 17. Girlando, M., Negri, S., Sbardolini, G.: Uniform labelled calculi for conditional and counterfactual logics. In: WoLLIC 2019. pp. 248–263 (2019) 18. Halpern, J.: An analysis of first-order logics for probability. Artificial Intelligence 46(3), 311–350 (1990) 19. Halpern, J.: Reasoning About Uncertainty. MIT Press (2003) 20. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512–535 (1994) 21. Jerábek, E.: Approximate counting in Bounded Arithmetic. J. Symb. Log. 72(3), 959–993 (2007) 22. Kontinen, J.: A logical characterization of the Counting Hierarchy. TOCL (2009) 23. Kozen, D.: Semantics of probabilistic programs. JCSS 53(3), 165–198 (1982) 24. Lehmann, D., Shelah, S.: Reasoning with time and chance. Inf. Control. 53(3), 165 – 198 (1982) On Counting Propositional Logic and Wagner’s Hierarchy 15 25. van Melkebeek, D.: A survey on lower bounds for satisfiability and related prob- lems. FnT-TCS 2, 197–303 (2007) 26. van Melkebeek, D., Watson, T.: A Quantum Time-Space Lower Bound for the Counting Hierarchy, available at: https://minds.wisconsin.edu/handle/1793/60568 27. Meyer, A., Stockmeyer, L.: The equivalence problem for regular expressions with squaring requires exponential space. In: SWAT. pp. 125–129 (1972) 28. Meyer, A., Stockmeyer, L.: Word problems requiring exponential time (preliminary report). In: STOC’73. pp. 1–9 (1973) 29. Negri, S., von Plato, J.: Proof Analysis: A Contribution to Hilbert’s Last Problem. Cambridge University Press (2011) 30. Nilsson, N.: Probabilistic logic. Artificial Intelligence 28(1), 71–87 (1986) 31. Nilsson, N.: Probabilistic logic revisited. Artificial Intelligence 59(1/2), 39–42 (1993) 32. Papadimitriou, C.: Games against nature. JCSS 31(2), 288–301 (1985) 33. Parberry, I., Schnitger, G.: Parallel computation with threshold functions. JCSS 36, 278–302 (1988) 34. Sorensen, M., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism, vol. 149. Elsevier (2006) 35. Stockmeyer, L.: The Polynomial-Time Hiearchy. Theor. Comput. Sci. 3, 1–22 (1977) 36. Torán, J.: An oracle characterization of the Counting Hierarchy. In: Proceedings. Structure in Complexity Theory Third Annual Conference. pp. 213–223 (1988) 37. Torán, J.: Complexity classes defined by counting quantifiers. Journal of the ACM 38(3), 753–774 (1991) 38. Valiant, L.: The complexity of computing the permanent. Theor. Comput. Sci. 8(2), 189–201 (1979) 39. Wagner, K.: Compact descriptions and the counting polynomial-time hierarchy. In: Frege Conference 1984: Proceedings of the International Conference held at Schwerin. pp. 383–392 (1984) 40. Wagner, K.: The complexity of combinatorial problems with succinct input repre- sentation. Acta Informatica 23, 325–356 (1986) 41. Wagner, K.: Some observations on the connection between counting and recursion. Theor. Comput. Sci. 47, 131–147 (1986) 42. Wrathall, C.: Complete sets and the Polynomial-Time Hierarchy. Theor. Comput. Sci. 3(1), 23–33 (1976) 43. Zachos, S.: Probabilistic quantifiers and games. JCSS 36(3), 433–451 (1988) 44. Zachos, S., Heller, H.: A decisive characterization of BPP. Information and Control pp. 125–135 (1986)