Fluted Fragment

Origin. Quine (1969), Purdy (1996). Variables in strict order. No variable reordering in atoms. Decidable fragment of FOL. Between monadic and full FOL.

Models. Variables x₁, x₂, ... appear in fixed order. Atom Rxy: x before y. No R(y,x) if R(x,y) present. Regular structure enables decidability.

Formalism.

Variable ordering: Variables: x₁, x₂, x₃, ... In any atom R(xᵢ₁,...,xᵢₖ): i₁ < i₂ < ... < iₖ, and the indices must be consecutive and end at the innermost bound variable. Strictly increasing indices are necessary but not sufficient; see the suffix condition below.

Fluted formulas: φ ::= R(xᵢ₁,...,xᵢₖ) | ¬φ | φ ∧ ψ | ∃xₙφ where atom indices increasing, quantifiers in order.

Examples: R(x₁,x₂,x₃): fluted (1<2<3) R(x₂,x₁,x₃): NOT fluted (2>1) ∃x₁∃x₂R(x₁,x₂) ∧ S(x₂): fluted ∃x₂∃x₁R(x₁,x₂): NOT fluted (quantifier order)

Equivalently: Formulas in variables x₁,...,xₙ. Each atom uses a suffix of the variables currently in scope: in a context x₁,...,xₙ, a k-ary atom must be R(x_{n−k+1},...,xₙ). Quantifiers bind the innermost variable, so the suffix condition is maintained as the formula is built up.

Semantic: Standard FOL semantics. Syntactic restriction, not semantic.

Complexity: Satisfiability decidable. Non-elementary lower bound. Contains monadic FOL.

Symbols.

Metatheory. Quine isolated the fragment while pursuing variable-free notation, but its metatheory was settled only recently, and the earlier literature is unreliable: Purdy (1996, 2002) claimed an exponential-size model property and NEXPTIME-completeness, and Pratt-Hartmann, Szwast and Tendera (2019) refuted both. What holds is this. The fluted fragment has the finite model property, so satisfiability and finite satisfiability coincide and the fragment is decidable. Complexity rises with the variable bound rather than sitting at any fixed level: for m ≥ 2, satisfiability for FLᵐ is ⌊m/2⌋-NEXPTIME-hard and, for m ≥ 3, in (m−2)-NEXPTIME — the bounds coincide for m ≤ 4 and leave a gap beyond — so the fragment as a whole has non-elementary complexity and no elementary decision procedure exists. It properly contains monadic first-order logic, since every unary atom trivially satisfies the suffix condition, and it is incomparable with both the two-variable fragment and the guarded fragment — it admits predicates of unbounded arity, which FO² does not, while FO² admits argument reversal, which it does not.

Applies to. Decidable fragments. Complexity theory. Logic and automata. Restricted reasoning.

Limitations. Argument order is fixed, so a relation cannot be applied to its arguments in the other order: R(x₂,x₁) is not a formula, converses are not expressible, and symmetry, asymmetry and antisymmetry cannot be stated of a given relation without introducing a separate symbol and losing the connection between them. Transitivity is likewise out of reach, so orders and reachability are not treatable. The standard fragment carries no equality. Decidability holds at a complexity that forecloses computational use: ⌊m/2⌋-NEXPTIME-hardness for m variables means the cost is non-elementary in the fragment as a whole, worse than the guarded fragment's 2EXPTIME and worse than FO²'s NEXPTIME. Worst, being fluted is a property of formulas and not of what they express — a sentence logically equivalent to a fluted one need not itself be fluted, the fragment is not closed under prenexing or under renaming of variables, and there is no semantic invariance characterizing it in the way guarded bisimulation characterizes the guarded fragment.

© 2026 Lingenic LLC