On the decision problem for quantified probability logics (Q6970366)

This paper studies the decidability of probability logics that contain quantifiers. It asks and answers questions about maximal fragments that are decidable and minimal fragments that are undecidable.\N\NThe introduction (Section 1) does a good job motivating and explaining the problem in general terms. It then lays out what is known about the decidability problems for the logic QPL\(^e\).\N\NSection 2 then formally introduces this logic and precisely states the relevant theorems. The language of this logic is a Boolean one augmented with a symbol for probability, \(\mu\), the symbols of ordered fields and quantifiers, \(\forall\) and \(\exists\). Basic formulae of this language are expression of the form\N\begin{align*}\Nf(\mu(\phi_1),\dots,\mu(\phi_m))\leq g(\mu(\phi_{m+1}),\dots,\mu(\phi_{m+n})),\N\end{align*}\Nwhere \(f\) and \(g\) are polynomials with integer coefficients and the \(\phi\) are Boolean terms. The set of all of formulae is then constructed by applying the classical first-order logic constructions. One example is\N\begin{align*}\N\Theta(X) = \mu(X)\neq 0\wedge \forall Y(\mu(X\wedge Y)\neq 0\rightarrow \mu(X\wedge \neg Y)=0).\N\end{align*}\N\NSection 3 introduces a natural one-sorted fragment \(\mathcal L_1\) of Halpern's ``first-order'' logic of probability of type 1. \(\mathcal L_1\) is obtained from applying two restrictions. (1) Quantifiers cannot be applied to reals. (2) \(\mu\) may only apply to quantifier-free first-order formulae. So, nesting of \(\mu\) is forbidden.\N\NSection 4 briefly describes a variant of \(\mathcal L_1\), \(\mathcal L_2\). The main new ingredient is a function \(\pi\) mapping elements of the domain of a structure, \(D\), to a set of possible worlds, \(\Omega\). A function \(p\) then describes discrete probabilities on \(\Omega\).\N\NThe main result in Section 5 is that the \(\Sigma_2\text{-}\mathrm{TH}(\mathcal K_{\mathrm{fin}})\) is hereditarily undecidable for QPL\(^e\), where \(\mathcal K_{\mathrm{fin}}\) is the union of the class of all spaces with at most \(n\) events. This fragment is hence \(\Pi_1^0\)-complete.\N\NSection 6 establishes the same undecidability and completeness result for the logic \(\mathcal L_1\).\N\NSection 7 establishes a version of undecidability and completeness result for the logic \(\mathcal L_2\).\N\NSection 8 shows the decidability of the \(\Pi_2\) fragments for the logics \(\mathcal L_1\) and \(\mathcal L_2\).\N\NSomewhat surprisingly, the author offers no conclusions. There's hence also no outlook on possible future research. I also want to mention that there are very few examples in the paper.