A Sound and Complete Calculus for Probability Inequalities

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