=Paper=
{{Paper
|id=Vol-3072/paper9
|storemode=property
|title=On Counting Propositional Logic and Wagner's Hierarchy
|pdfUrl=https://ceur-ws.org/Vol-3072/paper9.pdf
|volume=Vol-3072
|authors=Melissa Antonelli,Ugo Dal Lago,Paolo Pistone
|dblpUrl=https://dblp.org/rec/conf/ictcs/AntonelliLP21
}}
==On Counting Propositional Logic and Wagner's Hierarchy==
https://ceur-ws.org/Vol-3072/paper9.pdf
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)