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?

  • $\begingroup$ I think you can think of the underlying model as an equivalence relation, and therefore it's not interesting to have alternating quantifiers. $\endgroup$
    – Pål GD
    Nov 11 '21 at 9:22
  • $\begingroup$ Thanks, indeed. But then is there anything meaningful I can express in the logic? $\endgroup$
    – gigabytes
    Nov 11 '21 at 9:23
  • $\begingroup$ Are you interested on applications in the database-field? In case you are interested, in the field of databases we use logical languages (first-order logics, fixpoint logics, etc), to write queries (over finite structures). Using only one variable we might ask some "interesting" (although limited) queries. E.g. to retrieve those People who are young and male (Young(x)^Male(x)), or even People who works for themselves (WorksFor(x,x)) -which is an example where not all predicates are binary-. $\endgroup$
    – 441Juggler
    Nov 12 '21 at 17:10

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.