A Note on “Disjunctive” Predicates
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
, or even
are excluded from the post-condition too. The question at hand is to identify the class of propositions
such that
and
implies
.
In our expanded VPHL paper, we explicitly limited the propositions we were considering to those of the form , for
(specifically excluding negation and
), 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 ,
implies that
for any
.
Lemma 4.2 For any non-probabilistic assertion ,
implies
and
for any
.
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?