Monodic fragments of probabilistic first-order logic

By classical results of Abadi and Halpern, validity for probabilistic first-order logic of type 2 (ProbFO) is Π₁²-complete and thus not recursively enumerable, and even small fragments of ProbFO are undecidable. In temporal first-order logic, which has similar computational properties, these problems have been addressed by imposing monodicity, that is, by allowing temporal operators to be applied only to formulas with at most one free variable. In this paper, we identify a monodic fragment of ProbFO and show that it enjoys favorable computational properties. Specifically, the valid sentences of monodic ProbFO are recursively enumerable and a slight variation of Halpern's axiom system for type-2 ProbFO on bounded domains is sound and complete for monodic ProbFO. Moreover, decidability can be obtained by restricting the FO part of monodic ProbFO to any decidable FO fragment. In some cases, which notably include the guarded fragment, our general constructions result in tight complexity bounds.