Predicate logics of decidable fragments of arithmetic (Q1406364)

For a first-order theory \(T\), let \( {\mathcal L}(T) = \{\varphi\mid \text{for any interpretation } f T\vdash f(\varphi)\} \) be the set of predicate formulas, Pre be Presburger arithmetic, Sko be Skolem arithmetic, and DO be the discrete order theory. The main result of the paper is a proof of the inclusions \[ \text{PC}\subset{\mathcal L}(\text{Sko})\subset{\mathcal L}(\text{Pre})\subset {\mathcal L}(\text{DO})\subset \text{FIN}, \] where FIN is the set of formulas being true in all finite models.