REVIEW 3 major objections 6 minor 14 references
Undecidability of the elementary theory of Young--Fibonacci lattice
T0 review · 3 major / 6 minor · reviewed 2026-08-12 · deepseek-v4-flash
Pith's one-line read The elementary theory of the Young–Fibonacci lattice is undecidable and not finitely axiomatizable.
desk verdict The Young-Fibonacci analogue of Wires's theorem is likely correct and the strategy is right, but two unproved load-bearing assertions and a terse transfer step mean the paper needs a serious referee and a careful revision before I'd trust the proof. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The load-bearing mechanism is a first-order interpretation of arithmetic on the spine formed by the vertices $1^n$ for $n\ge 0$ in the Young–Fibonacci lattice. The paper first defines the child relation and the set of words with no digit $2$; with the constant $2$ it can separate the otherwise indistinguishable words $2$ and $11$, define the families $1^n$, $1^n2$, $1^n21$, and then use order and length formulas to express digit counts, addition, and multiplication on the $1^n$ chain. The undecidability of the positive $\Sigma_1$-theory of arithmetic then transfers to the theory of $\langle YF,\geqslant,2\rangle$. The secondary mechanism is the bijection $b$ from words to natural numbers, built from the prime factorization of the block structure of a word; showing this bijection is definable gives the maximal definability property.
What would settle it
Enumerate the immediate predecessors of all words of a fixed digit sum $n\ge 3$ in the Young–Fibonacci lattice and compare the predecessor sets; if any two distinct words share the same set, the proof of Proposition 6 fails, and with it the arithmetic interpretation that carries both main theorems.
Extended reading notes
Core claim
The paper's central claim, stated as Theorem 2 and Theorem 3, is that the elementary theory of the Young–Fibonacci lattice is undecidable and non-finitely axiomatizable, while the structure $\langle YF,\geqslant,2\rangle$ has the maximal definability property. The proof works by interpreting the arithmetic structure $\langle\mathbb{N}_0,+,\times\rangle$ in the lattice: the vertices $1^n$ are used as the numbers, and the paper builds first-order formulas that express $n=m+\ell$ and $n=m\ell$ for these vertices. Because the positive $\Sigma_1$-theory of arithmetic is undecidable, the lattice theory inherits undecidability; completeness then gives non-finite axiomatizability. For maximal definability, the paper defines a bijection $b:YF\to\mathbb{N}_0$ from the lattice onto the natural numbers and shows it is first-order definable, which makes every subset of every power of the lattice definable.
Load-bearing premise
The proof that every vertex is first-order definable rests on the assertion, justified in the paper only by 'it is easy to notice,' that no two distinct words with the same digit sum $n\ge 3$ ever have the same set of immediate predecessors; if that assertion fails, the induction defining singletons collapses and with it the interpretation of arithmetic.
Editorial extensions
If this is right
- No algorithm can decide the truth of arbitrary first-order sentences about the Young–Fibonacci lattice.
- The theory has no finite axiomatization, so no finite list of axioms captures all its true sentences.
- The expanded structure $\langle YF,\geqslant,2\rangle$ can define every relation on the lattice, not just order and equality.
- The explicit formulas for addition and multiplication give a translation from arithmetical sentences to lattice sentences, making concrete undecidable problems available in the lattice language.
Reading between the lines
- The same encoding strategy may work for any graded lattice with a definable unbounded chain that behaves like the $1^n$ spine; the paper's formula constructions are a template for such transfers.
- Since the constant $2$ is needed only to break the automorphism swapping $2$ and $11$, the pure poset language $\langle YF,\geqslant\rangle$ alone may still be undecidable but would require a separate argument that treats the two vertices symmetrically.
- The bijection $b$ from words to numbers may give a way to compute the definability rank of particular lattice subsets by reading off the complexity of the corresponding number-theoretic predicates, if the quantifier complexity of the bijection formulas is analyzed.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper claims to prove that the elementary theory of the Young–Fibonacci lattice is undecidable and non-finitely axiomatizable (Theorem 2), and that the structure ⟨YF, ⩾, 2⟩ has the maximal definability property (Theorem 3). The proof strategy follows Wires's work on Young's lattice: the author first defines singletons and then defines addition and multiplication on the subset {1^n : n ≥ 0}, obtaining an interpretation of arithmetic in YF*. Undecidability is then transferred from Matiyasevich's theorem, and maximal definability is obtained by constructing a definable bijection b: YF → N0 and importing a definability result for the prime-exponent relation from Wires's paper.
Significance. If the proof is completed, the paper would extend Wires's undecidability and maximal-definability results from Young's lattice to the Young–Fibonacci lattice, a natural and widely studied differential poset. The overall architecture is plausible and the paper contains many explicit definability formulas, which is a strength. However, several load-bearing structural assertions are either unproved or imported without justification, and numerous displayed formulas contain apparent typos or undefined symbols. The central ideas are promising, but the manuscript in its current form is not self-contained enough for the claims to be accepted as proven.
major comments (3)
- [Proposition 6] Proposition 6 asserts, with only 'it is easy to notice', that for |u| = n ≥ 3 no other rank-n vertex has the same set of parents. This injectivity is load-bearing: the displayed formula id_u(v) defines the class of vertices whose set of lower covers is exactly {u_1, ..., u_k}, and without injectivity this class may be strictly larger than {u}. The induction defining all singletons therefore collapses, and with it the interpretation of arithmetic used for Theorems 1 and 2. A rigorous proof must be supplied, including the exact treatment of words with no digit 1, since the parent-set computation depends on the convention for such words.
- [Proposition 38] Proposition 38, the definability of the prime-exponent relation, is imported from Wires [5, section 4] with no proof and no explanation of why a result for Young's lattice transfers to Young–Fibonacci lattice. This proposition is used essentially in Propositions 44, 47, and 48 to define the bijection b and to prove Theorem 3. The author should either prove Proposition 38 directly from the already-established addition and multiplication definability (e.g., via a standard arithmetic coding of exponentiation and divisibility) or state precisely which theorem of Wires applies to YF and why.
- [Theorems 1 and 2] Theorem 1 establishes undecidability of the Σ_{m+1}-theory of YF*, the structure with constant 2, while Theorem 2 claims undecidability of the elementary theory of YF, the structure without that constant. Since {2} is not definable in YF (as the automorphism in Remark 2 shows), undecidability of Th(YF*) does not automatically imply undecidability of Th(YF). The proof as written only cites [4] and does not supply the needed reduction. One can repair this by observing that for every formula φ(2), YF* ⊨ φ(2) iff YF ⊨ ∀x(Def_{2,11}(x) → φ(x)), but this argument is absent and must be added for Theorem 2 to follow.
minor comments (6)
- [Proposition 2] The terminology 'u is a child of v' is confusing because the formula r(u,v) has u ≥ v, so u is the upper cover; later 'parents' are identified with lower covers. Please adjust the terminology or clarify the intended reading.
- [Proposition 17] The displayed formula for ϕ_{1n,2n} contains the undefined symbol ϕ'_2; it should presumably be ϕ'_{1n,2n} from Proposition 16.
- [Proposition 20] As typeset, the formula for ϕ# uses ϕ_{2n,2n+1}(w,w') after fixing w' by ϕ_{1n,2n}(u,w'), which forces w' = 2^n and w' = 2^{n+1} simultaneously; the variable order or the relation used needs to be corrected.
- [Proposition 25] The formula for ϕ_r(u) contains 'u ⩾̸ v' where r(u,v) already implies u ≥ v, making the conjunct false; the intended condition is probably 'v ⩾̸ w' to express that the two parents are distinct.
- [Remark 6 and Proposition 34] The exponent notation 'nm−1/2(m2−m)' is ambiguous; please add parentheses, e.g., nm − (m^2 − m)/2, to clarify the intended exponent.
- [Throughout] The paper never defines 'maximal definability property'; a precise definition or a direct reference to Wires's definition should be included so that Theorem 3 is meaningful to the reader.
Circularity Check
No circularity: the paper genuinely interprets arithmetic into the Young–Fibonacci lattice; the only flagged gap is an unproved combinatorial parent-set fact, which is a correctness issue rather than a circular reduction.
full rationale
The derivation chain is an explicit first-order interpretation of ⟨N0,+,×⟩ into YF*: addition (φ+), multiplication (φ×), and the bijection graph (φb) are built from the lattice order and the added constant 2 via explicit formulas, with no fitted parameters and no step that assumes the target undecidability or definability result. The transfers from arithmetic to the lattice theory use Matiyasevich's theorem and Tarski–Mostowski–Robinson, which are external and independent. The one load-bearing passage that lacks support is Proposition 6, where the singleton-definability induction relies on the assertion that distinct vertices of the same rank n≥3 have distinct parent sets; the proof only says 'it is easy to notice'. This is an omitted proof of a combinatorial fact, and if false the singleton-definability induction would collapse, but it is not a circularity: the assertion is about the lattice's parent sets, not an assumption of the theorem being proved. Proposition 38 is imported from Wires's paper [5], an external independent work, and is used as a lemma in the definability construction rather than as a self-supporting citation. Therefore no circular step is exhibited, and the circularity score is 0.
Assumptions & free parameters
assumptions (4)
- domain assumption In the Young-Fibonacci lattice, distinct vertices of rank at least 3 have distinct parent sets.
- standard math The positive Σ1-theory of (N0, +, ×) is undecidable (Matiyasevich).
- domain assumption The prime-exponent relation {(1^n, 1^m, 1^l) : p_n appears in the factorization of l with exponent m} is definable in YF*, as asserted to follow from Wires [5], Section 4.
- standard math Transfer theorems of Tarski, Mostowski, and Robinson [4] allow undecidability of the theory with constant 2 to imply undecidability and non-finite axiomatizability for the constant-free theory.
Cite this review
Pith. "Pith review of Undecidability of the elementary theory of Young--Fibonacci lattice." pith.science (2026). https://pith.science/paper/DTC36KM5
@misc{pith2026241117739,
author = {Pith},
title = {Pith review of: Undecidability of the elementary theory of Young--Fibonacci lattice},
year = {2026},
howpublished = {\url{https://pith.science/paper/DTC36KM5}},
note = {Machine review of arXiv:2411.17739}
}
abstract
For a poset $(P,\leqslant)$ we consider the first-order theory, that is defined by set $P$ and relation $\leqslant$. The problem of undecidability of combinatorial theories attracts significant attention. Recently A. Wires proved the undecidability of the elementary theory of Young lattice and also established the maximal definability property of this theory. The purpose of this article is to obtain the same results for another graded lattice, which has much in common with Young lattice: Young--Fibonacci lattice. As Wires does for Young lattice, for the proof of undecidability we define Arithmetic into this theory.
Reference graph
Works this paper leans on
-
[4]
Robinson,Undecidable The- ories
Alfred Tarski, Andrzej Mostowski, Raphael M. Robinson,Undecidable The- ories. North-Holland, Amsterdam, 1953
work page 1953
-
[1]
С. В. Фомин. Обобщенное соответствие Робинсона – Шенстеда – Кнута. Зап. научн. сем. ЛОМИ, 155 (1986), 156-175
work page 1986
-
[2]
R. P. Stanley.Differential posets. J. Amer. Math. Soc. 1 (1988), pp. 919-961
work page 1988
-
[3]
Yuri Matiyasevich.Hilbert’s Tenth Problem. MIT Press, Cambridge, 1993
work page 1993
-
[5]
Annals of Pure and Applied Logic 173 (2022), paper 103075
Alexander Wires.Complexity in Young’s lattice. Annals of Pure and Applied Logic 173 (2022), paper 103075
work page 2022
-
[6]
Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword Ordering
Simon Halfon, Philippe Schnoebelen, Georg Zetzsche. Decidability, com- plexity, and the expressiveness of first-order logic over the subword ordering, arXiv:1701.07470v1 [cs.LO], 2017
work page Pith review arXiv 2017
-
[7]
Jaroslav Jeˇ zek, Ralph Mckenzie.Definability in the lattice of equational the- ories of semigroups, I, Semigroup Forum 46 (1993), pp. 199-245
work page 1993
-
[8]
Jaroslav Jeˇ zek, Ralph Mckenzie.Definability in substructure orderings I: finite semilattices, Algebra Univers. 61 (2009), pp. 59-75
work page 2009
Show all 14 references
-
[9]
Jaroslav Jeˇ zek, Ralph Mckenzie.Definability in substructure orderings II: finite ordered setsOrder 27 (2010), pp. 115-145
2010
-
[10]
61 (2009), pp
Jaroslav Jeˇ zek, Ralph Mckenzie.Definability in substructure orderings III: finite distributive lattices, Algebra Univers. 61 (2009), pp. 283-300
2009
-
[11]
Kudinov, Victor L
Oleg V. Kudinov, Victor L. Selivanov, Lyudmilla V. Yartseva.Definability in the subword order, in: Proc. CiE-2010, in: LNCS, vol. 6158, Springer, 2010, pp. 246-255
2010
-
[12]
Kudinov, Victor L
Oleg V. Kudinov, Victor L. Selivanov.A Gandy theorem for abstract struc- tures and applications to first-order definability, in: Proc. of CiE-2009, in: LNCS, vol. 5635, Springer, Berlin, 2009, pp. 290-299
2009
-
[13]
Kudinov, Victor L
Oleg V. Kudinov, Victor L. Selivanov.Definability in the infix order on words, in: Proc. of DLT-2009, in: LNCS, vol. 5583, Springer, Berlin, 2009, pp. 454-465
2009
-
[14]
´Ad´ am Kunos.Definability in the embeddability ordering of finite directed graphs, II, Order 36 (2019), pp. 291-311. 20
2019
Reviewed August 12, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.