During my talk yesterday, somebody raised an important point when I discussed the Hoare rule for non-deterministic choice in the recursive semantics and claimed that the postcondition couldn’t be disjunctive: What if it was the negation of a conjunction?

I think I waved this away with a gesture towards the constructive Coq proof assistant, but that was in error (the Coq real number library actually posits the decidability of the reals).

In truth, propositions of the form $latex A \vee B$ $latex \neg (A \wedge B)$, or even $latex Pr(b) \neq p$ are excluded from the post-condition too. The question at hand is to identify the class of propositions $latex P$ such that $latex P(\Theta_1)$ and $latex P(\Theta_2)$ implies $latex P(\Theta_1 \oplus_p \Theta_2)$.

In our expanded VPHL paper, we explicitly limited the propositions we were considering to those of the form $latex Pr(b) \; \Box \; p$, for $latex \Box \in \{$ $latex \textless, \le, =, \ge, \textgreater \}$ (specifically excluding negation and $latex \neq$), and were therefore able to prove the following lemmas (from which the Hoare rule I introduced at PPS followed easily):

Lemma 4.1 For any *non-disjunctive* assertion $latex P$, $latex P(\Theta_1) \wedge P(\Theta_2)$ implies that $latex P(\Theta_1 \oplus_p \Theta_2)$ for any $latex p \in (0,1)$.

Lemma 4.2 For any *non-probabilistic* assertion $latex P$, $latex P(\Theta_1 \oplus_p \Theta_2)$ implies $latex P(\Theta_1)$ and $latex P(\Theta_2)$ for any $latex p \in (0,1)$.

But I’d be interested in the broader case: Has any work been done on showing what class of mathematical propositions are closed under the combination of distributions?