pith. sign in

arxiv: 1906.09131 · v1 · pith:74AQ3JNEnew · submitted 2019-06-21 · 💻 cs.LO

The Fluted Fragment with Transitivity

Ian Pratt-Hartmann , Lidia Tendera This is my paper

Pith reviewed 2026-05-25 18:47 UTC · model grok-4.3

classification 💻 cs.LO
keywords fluted fragmenttransitive relationssatisfiability problemfinite model propertyundecidabilitytwo-variable fragment
0
0 comments X

The pith

The fluted fragment has the finite model property with one transitive relation but is undecidable with three.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper examines the satisfiability problem for the fluted fragment of first-order logic after transitive relations are added. It establishes that the logic has the finite model property when restricted to a single transitive relation. This property yields decidability for satisfiability in that setting. The same paper shows that undecidability already holds for the two-variable fragment once three transitive relations are present. The results therefore mark a precise threshold in the number of transitive relations that separates the decidable case from the undecidable case.

Core claim

The fluted fragment with transitive relations enjoys the finite model property when only one transitive relation is available. On the other hand the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations.

What carries the argument

The fluted fragment, a syntactic fragment of first-order logic that restricts the order of variable occurrences, extended by transitive relations under standard model semantics.

If this is right

  • Satisfiability remains decidable for the full fluted fragment when limited to one transitive relation.
  • Undecidability applies even when formulas are restricted to two variables once three transitive relations appear.
  • The finite model property is the route to decidability in the single-relation case.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The sharp change between one and three relations may indicate how transitivity interacts with the ordered-variable syntax of the fragment.
  • Comparable thresholds could be checked in other variable-restricted fragments that incorporate transitive relations.

Load-bearing premise

The proofs rely on the precise syntactic definition of the fluted fragment and the standard semantics of transitive relations being applied without additional hidden restrictions on models or formulas.

What would settle it

A fluted formula using exactly one transitive relation that has only infinite models, or an effective decision procedure for satisfiability in the presence of three transitive relations.

read the original abstract

We study the satisfiability problem for the fluted fragment extended with transitive relations. We show that the logic enjoys the finite model property when only one transitive relation is available. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The manuscript studies the satisfiability problem for the fluted fragment of first-order logic extended by transitive relations. It claims that the fragment enjoys the finite model property when only a single transitive relation is present, and that satisfiability is already undecidable for its two-variable subfragment once three transitive relations are allowed.

Significance. If the proofs are correct, the results sharpen the known decidability boundary for fluted logic under transitivity constraints. The finite-model-property result supplies a positive algorithmic consequence for the one-transitive case; the undecidability result demonstrates that the boundary is tight once three transitive relations appear. Both outcomes are directly relevant to the model theory of description logics and modal logics that incorporate transitive modalities.

minor comments (3)
  1. [Abstract] The abstract states the two main theorems but does not indicate the precise syntactic restrictions or the number of variables used in each proof; a single sentence clarifying the variable count for the FMP result would improve readability.
  2. [Section 2] The definition of the fluted fragment (presumably recalled in §2) should explicitly restate the quantifier-ordering condition so that the interaction with transitivity axioms is immediately visible without external reference.
  3. [Undecidability section] In the undecidability reduction, the construction that encodes three transitive relations into a two-variable fluted formula should be accompanied by a short diagram or table showing how the original relations are simulated; the current textual description is dense.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our results on the finite model property for the fluted fragment with a single transitive relation and the undecidability result for the two-variable fragment with three transitive relations. The assessment aligns with the manuscript's claims. No major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper establishes the finite model property for the fluted fragment with one transitive relation and undecidability for its two-variable subfragment with three transitive relations via direct model-theoretic arguments. No equations, parameter fittings, self-definitional reductions, or load-bearing self-citations appear in the provided material. The claims rest on the standard semantics and precise syntax of the fragment without any reduction of outputs to inputs by construction. This is the expected non-finding for a pure decidability proof in logic.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The results rest on the standard definition of transitivity as a first-order property and the syntactic restrictions that define the fluted fragment; no free parameters or invented entities are introduced.

axioms (2)
  • standard math Transitivity is the first-order property ∀x∀y∀z (R(x,y) ∧ R(y,z) → R(x,z))
    Invoked as the meaning of each transitive relation in the extension.
  • domain assumption The fluted fragment is the set of first-order formulas obeying the fluting variable-order restriction
    The base logic whose extension is studied.

pith-pipeline@v0.9.0 · 5564 in / 1251 out tokens · 21348 ms · 2026-05-25T18:47:19.216920+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

26 extracted references · 26 canonical work pages

  1. [1]

    Baader, D

    F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel - Schneider, editors. The Description Logic Handbook: Theory, Implementation, and Applications . Cambridge University Press, 2003

    work page 2003

  2. [2]

    o rger, E. Gr \

    E. B \"o rger, E. Gr \"a del, and Y. Gurevich. The Classical Decision Problem . Springer, 1997

    work page 1997

  3. [3]

    Gr \"a del, P

    E. Gr \"a del, P. Kolaitis, and M. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic , 3(1):53--69, 1997

    work page 1997

  4. [4]

    A. Herzig. A new decidable fragment of first order logic. In Abstracts of the 3rd L ogical B iennial S ummer S chool and C onference in H onour of S. C.Kleene , June 1990

    work page 1990

  5. [5]

    Kazakov and I

    Y. Kazakov and I. Pratt-Hartmann. A note on the complexity of the satisfiability problem for graded modal logic. In Logic in Computer Science , pages 407--416. IEEE, 2009

    work page 2009

  6. [6]

    Kiero \' n ski

    E. Kiero \' n ski. On the complexity of the two-variable guarded fragment with transitive guards. Information and Computation , 204:1663--1703, 2006

    work page 2006

  7. [7]

    Kiero\' n ski, J

    E. Kiero\' n ski, J. Michalyszyn, I. Pratt-Hartmann, and L. Tendera. Two-variable first-order logic with equivalence closure. SIAM Journal on Computing , 43(3):1012--1063, 2014

    work page 2014

  8. [8]

    Kiero\' n ski and M

    E. Kiero\' n ski and M. Otto. Small substructures and decidability issues for first-order logic with two variables. Journal of Symbolic Logic , 77:729--765, 2012

    work page 2012

  9. [9]

    Kiero\' n ski and L

    E. Kiero\' n ski and L. Tendera. On finite satisfiability of two-variable first-order logic with equivalence relations. In Logic in Computer Science . IEEE, 2009

    work page 2009

  10. [10]

    Kiero\' n ski and L

    E. Kiero\' n ski and L. Tendera. Finite satisfiability of the two-variable guarded fragment with transitive guards and related variants. ACM Transactions on Computational Logic , 19(2):8:1--8:34, 2018

    work page 2018

  11. [11]

    R. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing , 6:467--480, 1980

    work page 1980

  12. [12]

    A. Noah. Predicate-functors and the limits of decidability in logic. Notre Dame Journal of Formal Logic , 21(4):701--707, 1980

    work page 1980

  13. [13]

    Pratt-Hartmann

    I. Pratt-Hartmann. Finite satisfiability for two-variable, first-order logic with one transitive relation is decidable. Mathematical Logic Quarterly , 64(6):218--248, 2018

    work page 2018

  14. [14]

    Pratt-Hartmann

    I. Pratt-Hartmann. The finite satisfiability problem for two-variable, first-order logic with one transitive relation is decidable. Mathematical Logic Quarterly , 64(3):218--248, 2018

    work page 2018

  15. [15]

    Pratt - Hartmann, W

    I. Pratt - Hartmann, W. Szwast, and L. Tendera. Quine's fluted fragment is non-elementary. In 25th EACSL Annual Conference on Computer Science Logic, CSL , volume 62 of LIPIcs , pages 39:1--39:21. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016

    work page 2016

  16. [16]

    Pratt - Hartmann, W

    I. Pratt - Hartmann, W. Szwast, and L. Tendera. The fluted fragment revisited. Journal of Symbolic Logic , 2019. (Forthcoming)

    work page 2019

  17. [17]

    W. C. Purdy. Fluted formulas and the limits of decidability. Journal of Symbolic Logic , 61(2):608--620, 1996

    work page 1996

  18. [18]

    W. C. Purdy. Complexity and nicety of fluted logic. Studia Logica , 71:177--198, 2002

    work page 2002

  19. [19]

    W. V. Quine. On the limits of decision. In Proceedings of the 14th International Congress of Philosophy , volume III, pages 57--62. University of Vienna, 1969

    work page 1969

  20. [20]

    W. V. Quine. The variable. In The Ways of Paradox , pages 272--282. Harvard University Press, revised and enlarged edition, 1976

    work page 1976

  21. [21]

    S. Schmitz. Complexity hierarchies beyond E lementary. ACM Transactions on Computation Theory , 8(1:3):1--36, 2016

    work page 2016

  22. [22]

    D. Scott. A decision method for validity of sentences in two variables. Journal of Symbolic Logic , 27:477, 1962

    work page 1962

  23. [23]

    Szwast and L

    W. Szwast and L. Tendera. The guarded fragment with transitive guards. Annals of Pure and Applied Logic , 128:227--276, 2004

    work page 2004

  24. [24]

    Szwast and L

    W. Szwast and L. Tendera. On the satisfiability problem for fragments of the two-variable logic with one transitive relation. Journal of Logic and Computation , 2019. Forthcoming

    work page 2019

  25. [25]

    L. Tendera. Decidability frontier for fragments of first-order logic with transitivity. In Proceedings of the 31st International Workshop on Description Logics co-located with 16th International Conference on Principles of Knowledge Representation and Reasoning (KR 2018) , 2018. URL: http://ceur-ws.org/Vol-2211/paper-02.pdf

    work page 2018

  26. [26]

    M. Vardi. On the complexity of bounded-variable queries. In Proceedings of the Fourteenth ACM SIGACT-SIGMOD-SIGART S ymposium on P rinciples of D atabase S ystems , pages 266--276, 1995

    work page 1995