A Sound and Complete Calculus for Probability Inequalities

We give a sound an complete multiple-conclusion calculus \(\$\vdash\) for finitely additive probability inequalities. In particular, we show $$\mathbf{\sim} \Gamma \$\vdash \mathbf{\sim} \Phi \equiv \forall \mathcal{P} \in probabilities. \sum \phi \leftarrow \Phi.\ \mathcal{P} \phi \leq \sum \gamma \leftarrow \Gamma.\ \mathcal{P} \gamma $$ ... where $\sim \Gamma$ is the negation of all of the formulae in $\Gamma$ (and similarly for $\sim\Phi$). We prove this by using an abstract form of MaxSAT. We also show $$MaxSAT (\mathbf{\sim} \Gamma\ @\ \Phi) + c\leq length\ \Gamma \equiv \forall \mathcal{P} \in probabilities. \left(\sum \phi \leftarrow \Phi.\ \mathcal{P} \phi\right) + c \leq \sum \gamma \leftarrow \Gamma.\ \mathcal{P} \gamma $$ Finally, we establish a collapse theorem, which asserts that $\left(\sum \phi \leftarrow \Phi.\ \mathcal{P} \phi\right) + c \leq \sum \gamma \leftarrow \Gamma.\ \mathcal{P} \gamma$ holds for all probabilities $\mathcal{P}$ if and only if $\left(\sum \phi \leftarrow \Phi.\ \delta \phi\right) + c \leq \sum \gamma \leftarrow \Gamma.\ \delta \gamma$ holds for all binary-valued probabilities $\delta$.