A Sound and Complete Calculus for Probability Inequalities (Q7361534)

From MaRDI portal

!

This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:

AFP entry Probability_Inequality_Completeness
Language Label Description Also known as
default for all languages
No label defined
    English
    A Sound and Complete Calculus for Probability Inequalities
    AFP entry Probability_Inequality_Completeness

      Statements

      20 February 2023
      0 references
      Matthew Doty
      0 references
      A Sound and Complete Calculus for Probability Inequalities (English)
      0 references
      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$.
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references