Counting propositional logic was recently introduced in relation to randomized computation and shown able to logically characterize the full counting hierarchy [1]. This paper aims to clarify the nature and expressive power of its univariate fragment. On the one hand, we make the connection of our logic with stochastic experiments explicit, proving that any (and only) event(s) associated with dyadic distribution can be simulated in this formalism. On the other, we provide an efective procedure to measure the probability of counting formulas.
Because many artificial intelligence applications require the ability to reason with uncertain knowledge, it is important to seek appropriate generalizations of logic from this case. [2, p. 71] For probabilistic algorithms behavioral properties, like termination or equivalence, have quantitative nature, that is computation terminates with a certain probability, and programs simulate the desired function up to some probability of error (for instance, when dealing with learning algorithms). Then, how can such properties be studied within a logical system?
In a series of recent works [
The development of counting logics is part of an overall study aiming to analyze interactions between (quantitative) logic and probabilistic computation, in order to deepen our knowledge of both.
Our project was motivated by two main considerations. On the one hand, since their appearance in the 1970s, probabilistic computational models have become more and more pervasive in several fast-growing areas of computer science and technology, from statistical learning to approximate computing. On the other, the development of diferent computational models has considerably benefitted from the mutual interchanges existing between logic and TCS. Nevertheless, there is at least one crucial aspect of the theory of computation which was only marginally touched by such fruitful interactions, namely randomized computation. The global purpose of our study is to lay the foundation for a new approach to bridge this gap, and its key ingredient consists in considering new inherently quantitative logics, the language of which includes non-standard quantifiers able to “measure” the probability of their argument formulas.
So far, we have mostly focussed on a few specific aspects of the interaction between
quantitative logics and randomized computation:
• Complexity theory: classical propositional logic (PL, for short) provides the first example
of an NP-complete problem [
In standard PL formulas are interpreted as single truth-values. The core idea of our counting
semantics consists in modifying this intuition in a quantitative sense, associating formulas
with measurable sets of (satisfying) valuations. Specifically, given a counting formula , its
interpretation is taken to correspond to the set of all maps ∈ 2N “making true”. Any such
set belongs to the standard Borel algebra over 2N, B(2N), yielding a genuinely quantitative
semantics. In particular, atomic propositions correspond to cylinder sets [
We can then enrich our language with new formulas expressing the measure of such sets. By
adapting Wagner’s notion of counting operator [
:= i | ¬ | ∧ | ∨ | C | D,
where ∈ N and ∈ Q[
J K
J¬K = 2N − JK J1 ∧ 2K = J1K ∩ J2K J1 ∨ 2K = J1K ∪ J2K
J C =
K J D =
K
∅ {︃2N if C (JK) ≥
otherwise ∅ {︃2N if C (JK) < otherwise.
Notice that, in [
Our counting logics are strongly related to probabilistic reasoning and, indeed, CPL0 ofers a natural model to express the probability of events associated with Bernoulli distributions. In fact, we show that counting formulas can simulate experiments associated to any dyadic probability distribution.
In CPL0, we can easily express that a formula is true with precisely a certain probability. For clarity’s sake, we do so by means of auxiliary quantifiers, C and D, intuitively saying that their argument formula is true with probability (resp.) strictly greater or smaller (or equal) than the given index.
Notation 1. So-called white counting quantifiers are interpreted as follows: JC K :=
∅ {︃2N if C (J K) > otherwise
JD K :=
∅ {︃2N if C (J K) ≤ otherwise.
Clearly, these quantifiers do not extend the expressive power of CPL0, as definable in terms of primitive C and D,1 but due to them exact probability is expressed in a compact way. Example 1. For example, we formalize that the formula = 1 ∧ 2 is true with probability 14 as = C1/4(1 ∧ 2) ∧ D1/4(1 ∧ 2).
By their semantic definition, it is natural to interpret atomic formulas of CPL0 as infinite sequences of independently and uniformly distributed random bits – that is, more concretely, as infinite sequences of (independent) fair coin tosses – and, in general, counting formulas as formally representing experiments associated with specific probability distributions. For instance, the fact that, when tossing an unbiased coin twice, the probability that it returns head both times is 14 can be expressed in CPL0 by the formula above (which is also easily proved valid in our semantics). Generally speaking, counting formulas can simulate events associated with any dyadic probability distribution, but those related to non-dyadic ones only approximately.
In fact, we capture atomic sampling from a Bernoulli distribution of non-reducible parameter = 2 by molecular formulas of CPL0, while corersponding complex events are expressed combining such formulas in the usual way. To make this intuition less vague, let us consider the following simple example.
Example 2. Let a biased coin return head only 25% of the time. In this case, it is clear that a single toss cannot be formalized by an atomic formula of CPL0. Yet, it can be easily expressed using a molecular formula, namely one in the form (i ∧ j) (with , ∈ N fresh). Consequently, also properties concerning complex events can be captured in CPL0. For instance, that the probability for at least one of two subsequent biased tosses to return head is greater than 13 is formalized by the (valid) formula:
= C1/3(︀ (1 ∧ 2) ∨ (3 ∧ 4))︀ . 1For further details, see Appendix B.1, and, in particular, Proposition 2. In the same way, we can (quantitatively) simulate any discrete distribution with ♯ = 2.2 Something diferent happens when considering experiments related to non-dyadic distributions. Indeed, by Lemma 1 below, formulas of CPL0 can simulate these events – such as tossing a biased coin returning head with probability 31 – only in an approximate way.3 Lemma 1. For any formula of CPL0 , there exist , ∈ N, such that C (J K) = 2 .
In [
The skeleton of our procedure is as follows. Given a formula of CPL0, we first consider its (inner) not-quantified formulas. We do so by passing through a special form, the measure of which can be computed in a straightforward way (Lemma 3). We prove that any formula of CPL0 without quantifiers can be converted into such measurable form (Lemma 4). Notably, the procedure we ofer is efective, but not necessarily “feasible” as requiring argument formulas to be put in disjunctive normal form (DNF, for short). Finally, we can deal with nested quantifications: by measuring argument formulas, one can substitute the corresponding inner counting-quantified expression with either ⊤ or ⊥.
For simplicity, before defining so-called measurable normal forms, we introduce notational conventions and the so-called auxiliary, polite forms.
Notation 2. We use 1, 2... for literals, i.e. atomic formulas or their negations. Given = literal, we define as follows: = {︃j
if = ¬j
¬j if = j,
with ∈ N. We use ⊥ as a shorthand for ∧ and ⊤ for ∨ .
2Of course, any information concerning the nature of variables involved in the experiment is lost, but quantitative
aspects, that is events’ probability, are all preserved through the formalization. For further details, see Appendix B.2.
3Generalizations of CPL0 associated with a probability space (2N, (C ), ), where is not necessarily the measure
of i.i.d. sequences of random bits, are cursorily presented in Appendix B.2. Observe that, diferently from standard
CPL0, the logics presented in the quoted Appendix can naturally formalize also events related to (any) non-dyadic
Bernoulli distributions.
45IInnd[e1e]d,a,oCnPeLc0a-nfoervmenuliantroidsuscaeidsytontbaectviacalildewxphreenssJionKs=of 2thNeafnodr minvmaeliads(wh)en=J, Kw=he∅re. is a counting formula
without quantifiers and ∈ Q[
Lemma 2. Given a formula of CPL0 in DNF , there is a * such that * is in DPF and ≡ * .
Now, as anticipated, we introduce a special form, such that expressions in this form can be “measured” in a straightforward way. We start by defining contradictory pairs, that is formulas (in CPF) the conjunction of which is invalid.
Definition 3 (Contradictory Pair). Two formulas of CPL0 in CPF, = ⋀︀∈{1,...,} and = ⋀︀∈{1,...,} , are said to be mutually contradictory when there exist a ∈ {1, ..., } and a ∈ {1, ..., } such that = (or = ).
By Definition 1 plus basic measure theory, it is easy to see that the measure of the disjunction of two contradictory formulas in CPF is the sum of the measure of each disjunct (which, being themselves in CPF, are measurable as well). The generalization of this intuition leads to the definition below.
Definition 4 (Measurable Normal Form). A formula of CPL0 = ⋁︀∈{1,...,} is in measurable normal form (MNF, for short), if either ∈ {⊥, ⊤} or is in DPF and for each , ∈ {1, . . . , }, and are mutually contradictory.
Lemma 3. Given a formula of CPL0 in MNF, say = ⋁︀∈{1,...,} : . if = ⊤, then C (J K) = 1, . if = ⊥, then C (J K) = 0, . otherwise C (J K) = ∑︀∈{1,...,} C (JK). Observe that, as said, each disjunct is in CPF, so, again by basic measure theory, its measure is easily computable as well and any JK can efectively be measured. 6
We conclude our proof showing that each formula in DPF can actually be “converted” into MNF. To do so, we notice that two disjuncts can be mutually related in three ways only: (1) if one is a sub-formula of the other, the former is simply removed;7 (2) if they are a contradictory pair, the form is already as desired and the next pair is considered; (3) if one of the two disjuncts, say , contains a literal , such that neither or occurs in the other disjunct, say , we substitute with ′ = ∧ and ′′ = ∧ to be both taken into account again. Lemma 4. For each CPL0-formula in DPF , there is a formula in MNF * such that ≡ * . We conclude by putting Lemmas 4 and 2 and Lemma 3 together, so to obtain the desired procedure that, for any formula of CPL0, efectively computes the measure of its probability. 6For further details, see Corollary 1. 7A formula in CPF, say = ⋀︀∈{1,...,} , is said to be a sub-formula of another formula in CPF, say = ⋀︀′∈{1,...,} ′ , when (they are not a contradictory pairs or ∈ {⊥, ⊤} or ∈ {⊥, ⊤} and) for each ′ ∈ {1, . . . , }, there is a ∈ {1, . . . , }, such that = ′ . For example, a formula 1 ∧ 2 ∧ 3 is a sub-formula of 1 ∧ 2. 1–13
Preliminaries. In order to avoid clash in terminology, we briefly recap a few standard notions
from probability theory. An outcome or point is the result of a single execution of an experiment,
the sample space Ω is the set of all possible outcomes, and an event is a subset of Ω. Two events,
say 1 and 2, are disjoint or mutually exclusive, when they cannot happen at the same time,
that is 1 ∩ 2 = ∅. Two events are independent when the occurrence of one does not afect the
probability for the other to occur. A class of subsets of Ω is a ( -)field if containing Ω itself and
being closed under the formation of complements and (in)finite unions. A probability measure
Prob(· ) is a real-valued function defined on a field satisfying Kolmogorov’s axioms [
Following [
Proposition 1. If 0 = 1 = 12 , then for any cylinder of rank , call it C , there exist , ∈ N, such that C (C ) = 2 .
Going back to (C ), i.e. the smallest -algebra including C and which is Borel, a well-defined probability measure is assigned to it by generalizing in the natural way the measure defined above for a cylinder of rank .
B.1. Section 3.1 Proofs from Section 3.1.
Lemma 5. For every formula of CPL0 , and ∈ Q[
⇔ C (J¬ K) ▷ 1 − , with (◁, ▷) ∈ {(≥ , ≤ ), (≤ , ≥ ), (>, <), (<, >)}.
Proof. Let us consider the case ≤ , ≥ . By Definition 1 C (J¬ K) = C (2N − J K) = 1 − C (J K). So, trivially, C (J K) ≥ if 1 − C (J K) ≤ 1 − if C (J¬ K) ≤ 1 − . All the other cases are proved in a similar way.
Proposition 2. For any formula of CPL0 , and ∈ Q[
C¬ ≡ D1− C¬ ≡ ¬
C1−
D¬ ≡ C1− D¬ ≡ ¬
D1− . Proof. The proof relies on Definition 1 and Lemma 5:
JC¬ K =
∅ {︃2N if C (J¬ K) ≥
otherwise =
∅ = D1−
J
K {︃2N if C (J K) ≤ 1 −
otherwise JC¬ K = J¬D¬ K
= J¬C1− K B.2. Section 3.2 JD¬ K = =
∅ = C1−
J
K ∅ {︃2N if C (J¬ K) <
otherwise {︃2N if C (J K) > 1 −
otherwise JD¬ K = J¬C¬ K = J¬D1− K. Proof from Section 3.2. We prove that formulas of CPL0 are interpreted as events associated with dyadic distributions relying on Proposition 1. To do so, we show that any counting formula is interpreted as a cylinder of rank , for some ∈ N.
Lemma 6. For any formula of CPL0 , there is a cylinder of rank C , such that J K = C . Proof. The proof is by induction on the structure of : • = i for some ∈ N. Then JiK = (), which is a thin cylinder. • = ¬. By IH, there is a and a cylinder of rank , C , such that JK = C . Let ′ = 2 − C (≡ 2N − C ). Then, J¬K = 2N − JK = 2N − C = C′ , which is clearly a cylinder of rank as well. • = 1 ∧ 2. By IH, there exist 1, 2 ∈ N and cylinders of rank 1, 2, C1 and C2 , such that (resp.) J1K = C1 and J2K = C2 . Then, if 1 = 2, J K = J1K ∩ J2K = C1 ∩ C2 = C1∩2 , which is a cylinder of rank 1 as well. Otherwise, assume 1 > 2 (the case 2 > 1 is equivalent). Let 2′ consists of the sequences (1, . . . , 1 ) in 21 such that the truncated sequence (1, . . . , 2 ) is in 2. Then, C2 ≡ C′2 = { : ((1), . . . , (1)) ∈ 2′}. We conclude that J K = J1K∩J2K = C1 ∩C′2 = C1∩2′ , which is a cylinder of rank 1. • = 1 ∧ 2. Similar to the case above. • = C and = D. Then, either J K = 2N or J K = ∅, which are both cylinders of rank (in particular, in the former case = 0).
Proof of Lemma 1. By putting Proposition 1 and Lemma 6 together.
Notice also that a “syntactic” proof of Lemma 1 is obtained as a corollary of the results provided in Section 4. Non-Dyadic Bernoulli Distributions. As said, one can simulate events associated with non-dyadic distributions in an approximate way only.
Example 3. Let us consider a biased coin returning head only 13 of the time. We cannot simulate this event in CPL0, but “approximate” it with = 2 variables of CPL0 in the following sense. If = 2 we can down-approximate a single toss of the biased coin as:
= (1 ∧ 2) ∨ (︀ (¬1 ∧ 2) ∧ (3 ∧ 4))︀ .
Observe that disjuncts are mutually contradictory, so C (JK) = 156 . If = 3, (down)approximation is obtained as,
′ = (1 ∧ 2) ∨ (︀ (¬1 ∧ 2) ∧ (3 ∧ 4))︀ ∨ ︀( (¬1 ∧ 2) ∧ (¬3 ∧ 4) ∧ (5 ∧ 6))︀ . Then, C (J′K) = 2614 . In general, the more is increased, the more precise is the approximation of the desired event.
Although events associated with non-dyadic distributions cannot be expressed in CPL0 in a
precise way, when switching to (CPL⋆0 or) the measure-quantified language MQPA [
Generalizing CPL0. As seen, the semantics for CPL0 is associated with a canonical
cylinder space (2N, (C ), C ), where C is the standard measure C (()) = 12 for any ∈ N,
corresponding to tossing fair coins [
Definition 5. Extended formulas are defined by substituting standard counting quantifiers with C ⋆ and D ⋆ , the interpretation of which is now based on P* :
J ⋆ K = C
∅ {︃2N if ⋆(J K) ≥ otherwise
J ⋆ K = D
∅ {︃2N if ⋆(J K) < otherwise.
Then, CPL0-formulas C and D become special cases of extended ones, namely C ⋆ and D ⋆ (resp.), where ⋆ = C . On the other hand, in CPL⋆0 we can simulate experiments corresponding to tossing (arbitrarily) biased coins.
Example 4. Let us consider a biased coin, which returns head only 13 of the time. Then, letting ⋆(()) = 13 (for any ∈ N), we can express that the probability for subsequent tosses to be successful is greater than 19 as
= C1/⋆9(1 ∧ 2).
Clearly, since ⋆(︀ J1 ∧ 2K) = 31 · 31 , the formula is valid, i.e. JC1/*9(1 ∨ 2)K = 2N.
C.1. Section 4.1 Measurable Normal Form. ⊢ c ↣ ⊢ b ↣ ⋆(JcK) ≥ C ⋆ C↣⋆
One can even define a calculus LKCPL0⋆ for this extended semantics, with no substantial
change with respect to the proof system LKCPL0 , introduced in [
It is clear that ≡ * . We now consider ′ = ⋁︀∈{1,...,′} * and define * applying the following transformations: * if * = ⊥ for any ∈ {1, . . . , ′}, then * = ⊥. * otherwise, we consider each ∈ {1, . . . , ′} starting with = 1: . if = ⊤, then * = ⊤. . if = ⊥, then is removed and + 1 is considered. . if ∈ {⊤, ⊥}, we consider each pedex starting with the first ′ ̸= ∈ {1, . . . , ′}: . if and ′ contain exactly the same literals, then ′ is removed and the subsequent pedex (diferent from both ′, ) is considered. . otherwise, is (at least temporarily) left unchanged and the subsequent pedex (diferent from both ′, ) is considered.
Again it is clear that ≡ * . 8Actually, due to Notation 2, case . should already be considered as the first case * . Observe that for any formula in DPF, either ∈ {⊥, ⊤} or no instance of ⊥, ⊤ occurs in it. As anticipated in Section 4, it is easy to measure the probability of a formula in CPF. 21 .
Proposition 3. Given a formula in CPF: . if = ⊤, then C (JK) = 1, . if = ⊥, then C (JK) = 0, . otherwise, = ⋀︀∈{1,...,} and C (JK) = 21 .
Proof. Case ., . are trivial consequences of Definition 1 and basic measure theory. Case . relies on Definition 2. Since does not contain ⊥, ⊤ (or contradictions) or repetitions, by semantic definition, its literals have to be interpreted as independent events, the measure of which is known. Thus, for basic measure theory, C ︀( q ⋀︀∈{1,...,} y)︀ = C (︀ ⋂︀∈{1,...,}JK︀) = Proof of Lemma 3. As before, cases ., . hold by Definition 1 and basic measure theory. Case . is proved relying on Definition 4: for any ̸= ∈ {1, . . . , }, ( , ) is a contradictory pair. Then, by Definition 3, J K ∩ JK = ∅ for any , . So, we conclude C ︀( q ⋁︀∈{1,...,} y)︀ = C (︀ ⋃︀∈{1,...,}JK︀) = ∑︀∈{1,...,} C (JK).
Corollary 1. Given a formula of CPL0 in MNF, = ⋀︁ Proof. By Proposition 3 and Lemma 3.
We show how to convert a CPL0-formula in DPF into an equivalent Proof of Lemma 4. Given a formula of CPL0 in DPF = ⋁︀∈{1,...,} , we define a formula * in MNF such that ≡ * as follows: * if ∈ {⊥, ⊤}, then * = . * otherwise, we consider each ∈ {1, . . . , }, starting with = 1: . if there is a ̸= ∈ {1, . . . , } such that is a sub-formula of , then is removed and + 1 is considered. . otherwise, we consider each pedex ̸= ∈ {1, . . . , } starting from the first one: . if and are mutually contradictory, then + 1 is considered. . otherwise, for = ⋀︀∈{1,...,} and = ⋀︀′∈{1,...,′} ′ , we consider each ∈ {1, . . . , } starting with = 1: · if there is a ′ ∈ {1, . . . , ′} such that = ′ , then is left unchanged and + 1 is considered. · if there is no ′ ∈ {1, . . . , ′} such that = ′ , then is replaced by two formulas ′ = ∧ ′ and ′′ = ∧ ′ and .-. are applied again to both.
We consider each ′ ∈ {1, . . . , ′} starting with ′ = 1: · if there is a ∈ {1, . . . , } such that = ′ , then ′ is left unchanged
and ′ + 1 is considered. · if there is no ∈ {1, . . . , } such that = ′ , then is replaced by ′ = ∧ ′ and ′′ = ∧ ′ and .-. are applied again to both.
Then, we consider + 1.
When + 1 = , + 1 is considered (until also + 1 = ).