Questions: Decidable Fragments of First-Order Logic

Question 1

First-order logic with only two variable names (x and y, reused freely) is decidable. What happens if you add a third variable name?

• A. The three-variable fragment is still decidable, just harder — it becomes EXPTIME-complete instead of NEXPTIME-complete
• B. Adding a third variable restores full FOL expressiveness and undecidability
• C. The three-variable fragment is decidable but only for finite models
• D. Three variables make the fragment decidable for satisfiability but undecidable for validity

Answer: (B)

The two-variable fragment (FO²) is decidable (NEXPTIME-complete) — a surprising result given that two variables can express substantial relational structure. But adding a third variable name (FO³) is enough to encode Turing machine computations, restoring undecidability. This illustrates how sharply the decidability boundary cuts: a single variable can tip a fragment from decidable to undecidable by enabling simulation of computation. The two-variable result is not a curiosity but the precise boundary of what the quantifier variable count alone can achieve.

Question 2

Modal logic is decidable. What is the connection between modal logic's decidability and the theory of decidable fragments of first-order logic?

• A. Modal logic is unrelated to FOL — its decidability comes from different proof-theoretic grounds
• B. Modal logic translates into a restricted fragment of FOL via the standard translation, and decidability of modal logic corresponds to decidability of that FOL fragment
• C. Modal logic is decidable only for propositional (zero-order) formulas, not when quantifiers are present
• D. Modal logic's Kripke semantics is inherently finite, making all satisfiability problems trivially decidable

Answer: (B)

Modal logic has a standard translation into FOL: modal formulas become FOL formulas with two variables ranging over worlds, and accessibility becomes a binary predicate. The resulting FOL fragment falls within the decidable two-variable fragment (FO²). Modal logic's decidability is therefore a consequence of its being a syntactic restriction that corresponds to a known decidable FOL fragment. This connection explains why temporal logic and description logics — also expressible as FOL fragments — can be automated.

Question 3

Monadic first-order logic — where all predicates take exactly one argument — is decidable.

• T. True
• F. False

Answer: True

Löwenheim proved in 1915 that the monadic fragment of FOL is decidable. With only unary predicates, you can classify objects into categories (is-red(x), is-large(x)) but cannot express relational structure between objects (is-connected-to(x,y), is-parent-of(x,y)). This limits the combinatorial complexity enough that satisfiability remains decidable. The moment you introduce binary predicates, you can start encoding relational structure that enables computation simulation, and undecidability becomes possible.

Question 4

Since full first-order logic is undecidable, most fragments of first-order logic obtained by restricting the set of allowed formulas are also undecidable.

• T. True
• F. False

Answer: False

Undecidability of full FOL means there exists no algorithm for the full language — not that every restriction is also undecidable. Many practically important fragments are decidable: monadic FOL (Löwenheim, 1915), the Bernays-Schönfinkel class (∃*∀*), the Ackermann class (∃*∀∃*), the two-variable fragment, and propositional logic itself. Restricting predicate arity, quantifier prefix, or variable count can block the encoding of Turing machine computations, recovering decidability. The entire field of decidable fragments demonstrates that undecidability lives in specific logical features, not in FOL-style reasoning as such.

Question 5

What determines whether a fragment of first-order logic is decidable or undecidable, and why does the ability to encode Turing machine computations matter?

Model answer: A fragment of FOL is undecidable if it can simulate arbitrary Turing machine computations — because satisfiability of a formula in that fragment can then encode the halting problem, which has no algorithmic solution. Restrictions that prevent such simulation can recover decidability. Key restrictions include: limiting predicates to unary only (monadic fragment, no relational structure between objects), limiting quantifier alternation (∃*∀* prefix allows finite satisfiability checking), or limiting the number of variable names to two (FO²). When none of these restrictions block all computation-encoding paths, undecidability follows by reduction from the halting problem.

The core insight is that FOL's undecidability is not inherent to having quantifiers or predicates per se — it requires enough expressive power to write down a formula that is satisfiable if and only if a Turing machine halts. Fragments that lack binary predicates, restrict quantifier alternation, or cap variable names may lack the resources to perform this encoding. The practical payoff: description logics, temporal logics, and database query languages all sit in decidable FOL fragments, making automated reasoning over them possible.