On Counting Propositional Logic

TL;DR

This paper explores counting propositional logic, establishing its decision problem complexity within Wagner's hierarchy and demonstrating its proof-theoretical and practical applications, including a type system for probabilistic lambda-calculus.

Contribution

It introduces counting propositional logic, analyzes its complexity, and develops a proof system and a type system for probabilistic lambda-calculus based on it.

Findings

Decision problem matches Wagner's counting hierarchy

Logic admits a satisfactory proof-theoretical treatment

Derives a type system for probabilistic lambda-calculus

Abstract

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.