Uses of of the one-variable fragment of first-order logic aka S5

Question

I'm looking at decidable fragments of first-order logic. It seems that FO(1), i.e. the one-variable fragment of first-order logic is equivalent to the modal logic S5. However, I cannot find a reference (everybody references a German article of 1933 which I cannot understand).

So I'm trying to understand what can be done with FO(1). It seems to me that it the same as the monadic fragment, i.e. where you only have monadic predicates and no binary relations, am I right? Can you tell me any interesting thing that can be expressed using no binary relations?

For example, I cannot find any meaningful sentence with a quantifier alternation since any nested quantifier would hide the outmost quantified variable.

So is there any interest in FO(1)/S5 by itself?

Answer 1

Certainly there're meaningful research went to one-variable fragment of some specific first-order logics, though surprisingly in general they're undecidable even without any binary relations in this fragment.

From a recent paper "The One-Variable Fragment of Corsi Logic" by Caicedo1 et al, the one-variable fragment of the first-order logic of linear intuitionistic Kripke models turns out to be decidable:

In this paper, we investigate the one-variable fragment of the first-order logic of linear intuitionistic Kripke models, axiomatized by Corsi in [7] as the extension of first-order intuitionistic logic with the prelinearity axiom schema (α → β) ∨ (β → α), and referred to here as Corsi logic. In particular, we prove that the modal counterpart of this one-variable fragment is the many-valued modal logic S5(G), with propositional connectives interpreted using the standard semantics of Gödel logic and $\square$ and $\Diamond$ interpreted as infima and suprema relative to [0, 1]-valued accessibility relations.

The logic S5(G) lacks the finite model property with respect to its standard Kripke semantics, but is complete with respect to a variety of monadic Heyting algebras that has this property (see [2]) and is hence decidable. We provide here an alternative decidability proof that also establishes co-NP-completeness.

Another one-variable fragment of the first-order logic of branching time temporal logic had been studied by Hodkinson et al in their somewhat old paper "Decidable and undecidable fragments of first-order branching temporal logics":

On the one hand, we show that the one-variable fragments of logics like first-order CTL*—such as the product of propositional CTL* with simple propositional modal logic S5, or even the one-variable bundled first-order temporal logic with sole temporal operator ‘some time in the future’—are undecidable. On the other hand, it is proved that by restricting applications of first-order quantifiers to state (i.e., path-independent) formulas, and applications of temporal operators and path quantifiers to formulas with at most one free variable, we can obtain decidable fragments.

So definitely there's interest in FO(1) fragments of certain first order logics.