Pith. sign in

REVIEW 3 major objections 3 minor 20 references

A Decidable Bundled Fragment of First-Order Modal Logic Without Finite Model Property

T0 review · 3 major / 3 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper proves that the bundled fragment of first-order modal logic combining existential-with-necessity (∃□) and necessity-with-universal (□∃) formulas is decidable over increasing domain models, even though it lacks the finite model…

desk verdict A genuinely new decidability result with a promising Skolem-forest technique, but the completeness proof's limit-model truth lemma has a gap that needs repair before the result is established. read the letter →

arxiv 2506.01421 v1 pith:B7JQWV6E submitted 2025-06-02 cs.LO

Varad Joshi , Anantha Padmanabha This is my paper
classification cs.LO MSC 03B4503B2568Q17
keywords bundledfragmentsfirst-ordermodallogicdecidabilityfinitemodelpropertyincreasingdomainmodelstableauproceduresskolem-forestsatisfiability
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper answers an open question in the classification of bundled fragments of first-order modal logic. It proves that the fragment combining ∃□ and □∃ is decidable over increasing domain models, despite the fact that it does not have the finite model property: some satisfiable formulas force an infinite domain even when only finitely many worlds are needed. The decidability proof is a tableau procedure whose finite nodes carry a finite labelled forest, called a skolem-forest, that records which local-domain elements need witnesses for nested ∀∃ formulas and when the witness chain can be cut off because an atom repeats. When the model extracted from a tableau does not yet satisfy the root formula, the forest is extended by copying a repeated subtree with fresh variables, producing an infinite sequence of finite tableaux whose union yields a genuine infinite model. This gives a 2NExpTime upper bound and turns the trichotomy of Liu et al. (2023) into a dichotomy for increasing domain models.

What carries the argument

The load-bearing object is the skolem-forest, a finite labelled forest associated with a tableau node that contains a unique nested ∀ formula of the form ∀xψ. Each tree in the forest has as its root a variable from the current local domain, and each edge from a variable z to a child records that a fresh variable was created as a witness for some existential subformula ∃yβ that must hold for z; vertices are labelled by atoms of ψ. The forest's cutoff condition stops a tree when the atom at a leaf repeats among two earlier ancestors on the same root-to-leaf path, guaranteeing finiteness while still encoding enough information to generate witnesses in the limit. Its role is to make every node of the tableau finite and to provide the template for the repair operation that copies a repeated subtree onto a leaf, producing the infinite sequence of tableaux whose union gives the intended model.

What would settle it

Run the tableau-repair procedure on the formula φ1 from Section 3, which is satisfiable and forces an infinite domain. If the sequence of finite tableaux ever reaches a stage where some leaf variable's required witness is never supplied in the union model, or where a leaf is labelled by both a literal and its negation, then the completeness direction is refuted; the paper predicts instead that every leaf violation is repaired by copying subtrees, so checking that every existential requirement at every leaf is met in the limit model settles the matter.

Watch

Extended reading notes

Core claim

The central claim is that the satisfiability problem for the ∃□ + □∃ bundled fragment of first-order modal logic over increasing domain models is decidable. The proof works by constructing, for every satisfiable formula, an open tableau whose nodes hold sets of subformulas together with a finite skolem-forest: each tree in the forest is rooted at a local-domain element, and edges record that a child variable was introduced as a witness for an existential subformula sitting inside a nested universal formula. The forest stops growing along a root-to-leaf path once the same atom occurs twice among earlier ancestors, which keeps the tableau finite despite the fact that the models themselves may be infinite. If the model read off from a finite open tableau fails to satisfy the root formula, the tableau is repaired by copying the subtree rooted at the repeated atom onto the deficient leaf, with all copied variables renamed fresh; iterating this repair gives a sequence of finite open tableaux whose union is a model satisfying the formula. Theorem 9 states that an open tableau exists if and only if the root formula is satisfiable, and Corollary 15 concludes that satisfiability is decidable with a nondeterministic double-exponential-time upper bound.

Load-bearing premise

The load-bearing assumption is that the limit model obtained by taking the union of the infinite sequence of repaired tableau models satisfies the original root formula; the manuscript's proof of that fact cites a lemma that only detects failures inside finite stages, so a full induction on instantiated subformulas showing that no failure survives in the limit is required.

Editorial extensions

If this is right

  • The bundled-fragment trichotomy of Liu et al. (2023) collapses to a dichotomy for increasing domain models, since the only combination whose decidability status was open is now known to be decidable.
  • Every satisfiable ∃□+□∃ formula admits an open tableau, and Lemma 10 bounds the skolem-forest at each node by n · m^{2^{O(m)}} in terms of domain size n and formula length m, yielding the 2NExpTime decision procedure of Corollary 15.
  • Decidability is not obtained through the finite model property; instead the construction deliberately builds infinite models as unions of an infinite sequence of finite tableau repairs, so the fragment becomes a rare example of a decidable first-order-logic extension that still forces infinite domains.
  • The paper proposes the skolem-forest technique as a reusable tool for other first-order modal fragments that lack the finite model property, citing the two-variable term modal logic with equality as a candidate where the same idea might apply.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the completeness gap in the written proof of Claim 14 is closed by a direct induction on instantiated subformulas, the repair-and-limit construction would provide a general template for proving completeness of tableau systems whose models are deliberately infinite generated by non-terminating repair sequences.
  • The same forest-with-repetition scheme may transfer to the □∃ fragment over constant domain models, which the paper leaves open; a natural test would be to run the repair construction on the constant-domain analogue of the paper's infinite-model formula and see whether the atom-repetition cutoff survives the change in domain discipline.
  • The result suggests that any lower bound for this fragment must come from formula-size encoding rather than from forced infinitude itself; the authors' suspicion that the problem is 2ExpSpace-complete, if confirmed, would show that the infinite-domain feature costs at most a single exponential blow-up over the stated upper bound.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 3 minor

Summary. The paper studies the bundled fragment of first-order modal logic that allows the quantifier-modal combinations ∃□ and □∃, over increasing-domain models. It claims to settle the case left open by Liu et al. 2023 by proving that this fragment is decidable even though it fails the finite model property. The proof introduces a tableau calculus in which each world-node carries a finite 'skolem forest' that records witnesses for nested ∀∃ alternations. Soundness is argued via rule-by-rule preservation of satisfiability together with a bounded-size skolem-forest lemma. Completeness is argued by an infinite repair sequence of tableaux: whenever a leaf witness is missing, the tableau is extended, and the root formula is claimed to hold in the limit model. The main result is Theorem 9, with Corollary 15 giving a 2NExpTime upper bound.

Significance. If the proof can be completed, this is a substantial result: it collapses the trichotomy of Liu et al. to a dichotomy over increasing-domain models, and it gives a rare example of a decidable first-order modal fragment without the finite model property. The skolem-forest construction is a novel pseudo-finite witness mechanism that may be reusable in other settings. The paper does not fit parameters or assume the target result; it relies on the published trichotomy and non-finite-model theorems of Liu et al. The main weakness is that the completeness direction, which is the core of the paper, is not established as written: the limit-model truth lemma is missing, and the proof of Claim 14 contains a load-bearing inference that is not licensed by the stated Lemma 13.

major comments (3)
  1. [Appendix D, proof of Claim 14, final paragraph (∀yψ case)] The inference 'by Lemma 13, M, w, ι |= ψ[y/z]' is not justified. Lemma 13 only says that if a formula is false at a node in the associated fixed-tableau model, then there is a descendant leaf violation involving some nested ∀ subformula; it does not prove truth. Moreover, ψ[y/z] is a substitution instance that need not belong to SF+(θ), so the structural induction on φ ∈ SF+(θ) cannot be applied to it. The completeness direction of Theorem 9 therefore requires a separate limit-model truth lemma, for example an induction over all formulas and substitution instances that appear during the repair sequence, using the fact that every leaf violation is eventually repaired by Lemma 12. This lemma is not supplied.
  2. [Section 6, Lemma 13 vs. Claim 14] Lemma 13 is stated and proved for the model M_T associated with a fixed open tableau T, using reverse induction on the height of T. Claim 14, however, is applied to the limit model M = ⋃_i M_i, whose domains and valuations are infinite unions over the repair sequence. No analogue of Lemma 13 is proved for this limit model, and the height induction does not directly transfer to the limit. The proof must either establish the needed failure-characterization property for the limit model or show that the finite-stage lemmas can be used uniformly to derive a contradiction from M, w, ι ⊭ ψ[y/z].
  3. [Appendix C, Lemma 12] Lemma 12 is load-bearing for the existence of the infinite repair sequence, but its proof is only a sketch. In particular, the final step that adds intermediate nodes to ensure all rule applications are valid is described as 'a tedious but routine induction' without presenting the induction invariant. Since the completeness argument depends on the repaired tableau remaining an open tableau and on the newly added formulas being propagated correctly, this step should be written out in full or at least with a precise invariant.
minor comments (3)
  1. [Figure 1] The meaning of the symbol ⋆ is given only in the caption; it would be clearer to include a legend inside the figure, since the table is central to the claimed trichotomy-to-dichotomy result.
  2. [Throughout] There are several typos and grammatical slips, including 'fragemtns' in Section 1, 'intution' in Appendix A, 'antecedant' in Section 5, 'is also is also' in Appendix D, and the garbled sentence in the proof sketch of Lemma 10 beginning 'For every z ∈ S, we make z as a root and assign them the atom that corresponds to what σ(z) prove in that in the same model Γ′ will also be valid.'
  3. [Corollary 15] The step from bounded labels at each tableau node to a 2NExpTime decision procedure is too quick. The authors should state a bound on the depth and branching of the saturated tableau that they intend to search, or formulate an explicit nondeterministic algorithm that guesses a finite tableau of doubly exponential size.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the tableau decidability proof is self-contained and does not reduce to fitted inputs or self-citation chains.

full rationale

The paper's central claim, Theorem 9, is an iff statement between the existence of an open tableau and satisfiability in an increasing domain model. Neither direction is assumed by construction: the tableau rules are defined syntactically from the bundled fragment, and the soundness direction proves rule-by-rule preservation of satisfiability; the completeness direction constructs a limit model from an open tableau and attempts to prove the truth lemma. The paper does not fit any parameters from the target formula and then relabel them as predictions. The reliance on Liu et al. 2023 is limited to the trichotomy and the non-finite-model-property theorem, which are independent published results; the fact that one co-author overlaps is not load-bearing because the present decidability proof does not invoke the target result from that prior work. Lemma 10, the bounded Skolem forest lemma, is proved from the semantics of satisfiability rather than assumed. The only notable issue is a stated proof gap in Claim 14: the universal-quantifier case concludes truth from Lemma 13, which only describes what happens when a formula is false, and the substitution instance may fall outside the induction set SF+(θ). That is a correctness or completeness-proof concern, not circularity, because it does not make the theorem equivalent to its inputs. Accordingly, the circularity score is 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper introduces no new model-theoretic entities such as forces or dimensions; the Skolem forest is a proof-theoretic artifact, not a semantic primitive. The main assumptions are domain monotonicity and the syntactic uniqueness of nested ∀ formulas, both of which are stated. No free parameters are fitted to data.

assumptions (4)
  • domain assumption The decidability result is restricted to increasing domain models, where each transition only enlarges the local domain.
    All definitions and proofs in the paper are for increasing domain models. The constant domain case is left open, as stated in Section 7.
  • standard math Every FOML formula can be rewritten in negation normal form and in clean form (no variable occurs both bound and free, each variable quantified at most once).
    Used throughout the tableau to manage witness variables; standard renaming is assumed without proof.
  • domain assumption The syntax of the ∃□+□∃ fragment ensures that at each world there is at most one nested ∀ formula (a formula ∀xψ where ψ contains an existential or universal quantifier in its scope).
    This is used to make the (nested ∀-rule) well-defined. It follows from the fragment's grammar (no □∀ or ∀□ bundles are allowed), but it is a structural assumption that is argued informally in Section 3.
  • standard math The standard tableau rules for ∧, ∨, ∃, ∀, and ♢ preserve satisfiability in the usual way.
    The soundness proof sketches these cases as standard; no novel metamathematical principle is invoked.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Decidable Bundled Fragment of First-Order Modal Logic Without Finite Model Property." pith.science (2026). https://pith.science/paper/B7JQWV6E

@misc{pith2026250601421,
  author       = {Pith},
  title        = {Pith review of: A Decidable Bundled Fragment of First-Order Modal Logic Without Finite Model Property},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/B7JQWV6E}},
  note         = {Machine review of arXiv:2506.01421}
}
read the original abstract

The satisfiability problem for First-order Modal Logic (\FOML) is undecidable even for simple fragments like having only unary predicates, two variables etc. Recently a new way to identify decidable fragments of \FOML has been introduced called the "bundled fragments", where the quantifiers and modalities are restricted to appear together. Since there are many ways to bundle the quantifiers together, some of them lead to (un)decidable fragments. In (Liu et.al, 2023) the authors prove a `trichotomy', where they show that every bundled fragment falls into one of the following three categories: (1) Those that satisfy "finite model property" (and hence decidable), (2) Those that are undecidable, and (3) Those that do not satisfy "finite model property" (whose decidability is left open). In this paper we collapse the trichotomy into a dichotomy over "increasing domain models" by proving that the one combination that falls into the last category is indeed decidable.

Figures

Figures reproduced from arXiv: 2506.01421 by the authors.

Figure 1
Figure 1. Reproducing part of the table from (Liu et al. 2023, Fig￾ure 1) for the increasing domain models. Here ⋆ indicates that the presence/absence of the particular fragment is not relevant. Note that the classification is exhaustive. But then there are other natural bundled fragments (4 in total and their duals: like every ∀/∃ should be suc￾ceeded/preceded by □ operator) and the combinations thereof. For instance a formu… view at source ↗
Figure 2
Figure 2. Tableau rules for ∃□ + □∃ [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Short notations for all subformulas of φ1. The variables in brackets indicate the free variables of the corresponding subfor￾mulas. A Appendix to Section 3 “∃□ + □∃ fragment” In this section we illustrate the key ideas of our tableau con￾struction for the formula φ1. From Theorem 6 it is clear that φ1 is satisfiable only in infinite models. We now explain how to get a finite witness for φ1 from which we can extract … view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Model M0 constructed from the tableau obtained for φ1 outlined in Appendix A [PITH_FULL_IMAGE:figures/full_fig_p014_4.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

20 extracted references · 19 canonical work pages

  1. [1]

    write newline

    " write newline "" before.all 'output.state := FUNCTION fin.entry add.period write newline FUNCTION new.block output.state before.all = 'skip after.block 'output.state := if FUNCTION new.sentence output.state after.block = 'skip output.state before.all = 'skip after.sentence 'output.state := if if FUNCTION not #0 #1 if FUNCTION and 'skip pop #0 if FUNCTIO...

  2. [2]

    Belardinelli, F., and Lomuscio, A. 2009. Quantified epistemic logics for reasoning about knowledge in multi-agent systems. Artificial Intelligence 173(9-10):982--1013

    work page 2009

  3. [3]

    Belardinelli, F., and Lomuscio, A. 2012. Interactions between knowledge and time in a first-order logic for multi-agent systems: completeness results. Journal of Artificial Intelligence Research 45:1--45

    work page 2012

  4. [4]

    o rger, E.; Gr \

    B \"o rger, E.; Gr \"a del, E.; and Gurevich, Y. 2001. The classical decision problem . Springer Science & Business Media

    work page 2001

  5. [5]

    Dixon, C.; Fisher, M.; Konev, B.; and Lisitsa, A. 2008. Practical first-order temporal reasoning. In 2008 15th International Symposium on Temporal Representation and Reasoning , 156--163. IEEE

    work page 2008

  6. [6]

    M., and Shehtman, V

    Gabbay, D. M., and Shehtman, V. B. 1993. Undecidability of modal and intermediate first-order logics with two individual variables. J. Symbolic Logic 58(3):800--823

    work page 1993

  7. [7]

    Gradel, E., and Walukiewicz, I. 1999. Guarded fixed point logic. In Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158) , 45--54. IEEE

    work page 1999

  8. [8]

    Hodkinson, I.; Wolter, F.; and Zakharyaschev, M. 2002a. Decidable and undecidable fragments of first-order branching temporal logics. In Proceedings 17th annual IEEE symposium on logic in computer science , 393--402. IEEE

    work page

Show all 20 references
  1. [9]

    Hodkinson, I.; Wolter, F.; and Zakharyaschev, M. 2002b. Decidable and undecidable fragments of first-order branching temporal logics. In Proceedings LICS 2002 , 393--402

    2002

  2. [10]

    E., and Cresswell, M

    Hughes, G. E., and Cresswell, M. J. 1996. A New Introduction to Modal Logic . Routledge

    1996

  3. [11]

    Kontchakov, R.; Kurucz, A.; and Zakharyaschev, M. 2005. Undecidability of first-order intuitionistic and modal logics with two variables. Bull. Symbolic Logic 11(3):428--438

    2005

  4. [12]

    Kripke, S. A. 1962. The undecidability of monadic modal quantification theory. Mathematical Logic Quarterly 8(2):113--116

    1962

  5. [13]

    Li, Y., and Wang, Y. 2019. Multi-agent knowing how via multi-step plans: a dynamic epistemic planning based approach. In Logic, Rationality, and Interaction: 7th International Workshop, LORI 2019, Chongqing, China, October 18--21, 2019, Proceedings 7 , 126--139. Springer

    2019

  6. [14]

    Liu, M.; Padmanabha, A.; Ramanujam, R.; and Wang, Y. 2022. Generalized bundled fragments for first-order modal logic. In 47th International symposium on mathematical foundations of computer science (MFCS 2022) . Schloss Dagstuhl-Leibniz-Zentrum f \"u r Informatik

    2022

  7. [15]

    Liu, M.; Padmanabha, A.; Ramanujam, R.; and Wang, Y. 2023. Are bundles good deals for first-order modal logic? Information and Computation 105062

    2023

  8. [16]

    Padmanabha, A., and Ramanujam, R. 2023. A decidable fragment of first order modal logic: two variable term modal logic. ACM Transactions on Computational Logic 24(4):1--38

    2023

  9. [17]

    Padmanabha, A.; Ramanujam, R.; and Wang, Y. 2018. Bundled fragments of first-order modal logic: (un)decidability. In Ganguly, S., and Pandya, P. K., eds., 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December...

    2018

  10. [18]

    Vardi, M. Y. 1997. Why is modal logic so robustly decidable? In Descriptive Complexity and Finite Models: Proceedings of a DIMACS Workshop, January 14-17, 1996, Princeton University , volume 31, 149. American Mathematical Soc

    1997

  11. [19]

    Wang, Y. 2017. A new modal framework for epistemic logic. In Proceedings of TARK 2017 , 515--534

    2017

  12. [20]

    Wolter, F., and Zakharyaschev, M. 2001. Decidable fragments of first-order modal logics. J. Symb. Log. 66(3):1415--1438

    2001

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.