  We study counting propositional logic as an extension of propositional logic
with counting quantifiers. We prove that the complexity of the underlying
decision problem perfectly matches the appropriate level of Wagner's counting
hierarchy, but also that the resulting logic admits a satisfactory
proof-theoretical treatment. From the latter, a type system for a probabilistic
lambda-calculus is derived in the spirit of the Curry-Howard correspondence,
showing the potential of counting propositional logic as a useful tool in
several fields of theoretical computer science.
