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. Decidable satisfiability. Non-elementary complexity. Contains monadic FOL. Tree-like models.

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

Limitations. Severe syntactic restriction. Non-elementary complexity. Limited expressiveness. Mainly theoretical interest.

© 2026 Lingenic LLC