## Abstract

We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, originating in the work of W.V. Quine. We show that the satisfiability problem for this fragment has non-elementary complexity, thus refuting an earlier published claim by W.C. Purdy that it is in NExpTime. More precisely, we consider

*FL*, the intersection of the fluted fragment and the^{m}*m*-variable fragment of first-order logic, for all*m*≥ 1. We show that, for*m*≥ 2, this sub-fragment forces*m*/2-tuply exponentially large models, and that its satisfiability problem is*m*/2-NExpTime-hard. We further establish that, for*m*≥ 3, any satisfiable*FL*formula has a model of at most (^{m}-*m*-2)-tuply exponential size, whence the satisfiability (= finite satisfiability) problem for this fragment is in (*m*-2)-NExpTime. Together with other, known, complexity results, this provides tight complexity bounds for*FL*for all^{m}*m*≤4.Original language | English |
---|---|

Pages (from-to) | 1020-1048 |

Number of pages | 29 |

Journal | The Journal of Symbolic Logic |

Volume | 84 |

Issue number | 3 |

Early online date | 6 Jun 2019 |

DOIs | |

Publication status | Published - 16 Sep 2019 |

## Keywords

- satisfiability
- complexity
- first-order logic
- fluted fragment