On Counting Propositional Logic and Wagner's Hierarchy

We introduce and study counting propositional logic, an extension 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 underlying decision problem perfectly matches the appropriate level of Wagner's counting hierarchy.