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ₖ Strictly increasing indices.

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 consecutive prefix of variables. Quantify outermost variables first.

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