Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Suppes' Theorem for Probabilit...


view this post on Zulip Email Gateway (Jan 25 2023 at 06:38):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

I’d like to announce a new AFP entry.

Suppes' Theorem for Probability Logic
by Matthew Doty

Abstract:
We develop finitely additive probability logic and prove a theorem of Patrick
Suppes that asserts that "Psi |- phi" in classical propositional logic if and
only if "(Sum psi <- Psi. 1 - P(psi)) >= 1 - P(phi)" holds for all probabilities
P. We also provide a novel dual form of Suppes' Theorem, which holds that
"(Sum phi <- Phi. P(phi)) <= P(psi)" for all probabilities P if and only
"(\/ Phi) |- psi" and all of the formulae in Phi are logically exclusive from one
another. Our proofs use Maximally Consistent Sets, and as a consequence, we obtain
two collapse theorems. In particular, we show "(Sum phi <- Phi. P(phi)) >= P(psi)"
holds for all probabilities P if and only if "(Sum phi <- Phi. delta(phi)) >=
delta(psi)" holds for all binary-valued probabilities delta, along with the dual
assertion that "(Sum phi <- Phi. P(phi)) <= P(psi)" holds for all probabilities
P if and only if "(Sum phi <- Phi. delta(phi)) <= delta(psi)" holds for all
binary-valued probabilities delta.

https://protect-eu.mimecast.com/s/0yKNCLAGWHRpDSBilNK?domain=isa-afp.org

Enjoy,
René


Last updated: Mar 29 2024 at 12:28 UTC