### Abstract

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$.

### License

BSD License

### Topics

- Mathematics/Probability theory
- Logic/General logic/Classical propositional logic
- Logic/General logic

### Session Probability_Inequality_Completeness

- Probability_Inequality_Completeness

### Depends on

- Suppes' Theorem For Probability Logic

## Cite

×

Probability_Inequality_Completeness-AFP

    @article{Probability_Inequality_Completeness-AFP,
      author  = {Matthew Doty},
      title   = {A Sound and Complete Calculus for Probability Inequalities},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Probability_Inequality_Completeness.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Mar 7, 2023 : Isabelle2022