REVIEW 3 major objections 5 minor 2 references
The flattening operator in team-based logics
T0 review · 3 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash
Pith's one-line read Adding the flattening operator F to team semantics: full logics absorb it, while unary inclusion and anonymity logics become strictly more expressive.
desk verdict Systematic study of the flattening operator with several plausible safety results, but both headline expressivity increases rest on proofs that do not work. 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 paper's central object is the operator F defined by M ⊨ₓ Fφ iff every singleton sub-team {s} satisfies φ; F always produces flat formulas and is idempotent. Alongside it, the paper considers the flattening φf of a formula, determined by axioms (entailment, flatness, and distributivity over connectives and quantifiers); for dependence, anonymity, inclusion, and independence atoms these axioms force φf ≡ ⊤, while for exclusion atoms two choices remain and the paper selects ⊤. For the safety results, the machinery is a pair of translations: formulas of FO(⊆,F) are translated into positive greatest fixed-point logic with a new relation symbol for the team, and formulas of FO(=(·,·),F) are translated into downwards-closed existential second-order logic, yielding equivalence with the underlying logics. For the unary-anonymity separation, the load-bearing device is a lemma asserting that teams closed under a sufficiently rich set of automorphisms cannot distinguish a formula of FO(Υ1) from its flattening, so the FO(Υ1,F) sentence separating Aₙ and Bₙ has no FO(Υ1) equivalent. The unary-inclusion separation instead reuses a graph-connectedness argument from the earlier literature on safety of atoms.
What would settle it
Take a nonempty model M and a team X closed under the automorphism family used in the paper's Lemma 5.7, with some s ∈ X such that s(x₁) = s(x₂) = a. To prove M ⊨ₓ x₁ Υ x₂ the lemma requires an automorphism f with f(a) = a and f(a) ≠ a, which no injective map can provide; checking whether this instance invalidates the induction step settles whether the lemma, and with it the FO(Υ₁,F) separation claim, stands.
Extended reading notes
Core claim
Team semantics evaluates formulas on sets of assignments, and a formula is flat when team satisfaction reduces to satisfaction by singleton teams. The flattening operator F forces this property on any formula: M ⊨ₓ Fφ iff M ⊨{s} φ for every s ∈ X. The paper's central claim is a systematic map of where this operator is safe. For full dependence logic, full inclusion logic (at the level of sentences), exclusion logic, independence logic, constancy logic, and FO(∼), every formula of the logic extended by F is equivalent to one without F; the translations go through existential second-order logic and positive greatest fixed-point logic. In contrast, for the unary fragments of inclusion and anonymity logic, F is not safe: an explicit FO(⊆1,F) sentence says a graph is disconnected, and an explicit FO(Υ1,F) sentence holds on the disjoint union of two odd cycles Aₙ but fails on a single even cycle Bₙ, while no FO(Υ1) formula can separate those models. Consequently the flattening operator and the syntactic flattening φf, which the paper characterises axiomatically, are not the same operation: for sentences they need not coincide, with a counterexample in anonymity logic.
Load-bearing premise
The unary-anonymity separation relies on a lemma that assumes, for any two points, an automorphism fixing the first and moving the second, but such an automorphism cannot exist when the two points are the same, so the assumption is unsatisfiable for nonempty models as written, and the proof does not treat teams in which the two variables take the same value.
Editorial extensions
If this is right
- In full dependence, exclusion, and independence logic, flattening can be used freely: every formula of the extended logic has an equivalent formula without F.
- Full inclusion logic with F translates into positive greatest fixed-point logic, so at the level of sentences FO(⊆,F) and FO(⊆) define the same classes of models.
- Unary inclusion logic with F can express non-connectedness of graphs, a property not expressible in unary inclusion logic alone.
- Unary anonymity logic with F separates the graph families Aₙ (two cycles of length 2n+1) from Bₙ (one cycle of length 2n+2), while unary anonymity logic alone cannot.
- Boolean-negation logic FO(∼) absorbs F without gaining expressive power.
Reading between the lines
- If the pattern holds for all fixed-arity fragments, the flattening operator acts as a uniform way to climb the arity hierarchy of team logics without moving to larger atoms; the paper conjectures this for the remaining fragments.
- Because Fφ only checks singleton teams, the operator could be a tool for translating team-satisfaction problems into single-assignment checks, potentially simplifying model checking and SAT encodings for fragments where F is absent.
- The non-uniqueness of the flattening of exclusion atoms suggests that inclusion/exclusion duality may require a convention when flattening is axiomatised; a different choice, such as x ≠ y, would change the canonical flattening and might affect comparisons with flat formulas.
- Open separation questions, such as whether F increases the power of unary exclusion logic or unary constancy logic, could be tested with the same graph-family technique; the paper's summary figure leaves those comparisons unresolved.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper studies Hodges' flattening operator F in team semantics, where M⊨_X Fφ iff every singleton assignment of X satisfies φ. It proposes an axiomatic definition of formula flattening, proves safety results for dependence, exclusion, independence, constancy, and FO(∼), and claims that F strictly increases the expressive power of unary inclusion logic and unary anonymity logic. It also claims sentence-level equivalences FO(⊆,F)≡FO(⊆) and FO(Υ,F)≡FO(Υ). The main proofs use translations to GFP+ and ESO, plus an automorphism-closure lemma.
Significance. The topic is well chosen: the flattening operator has been largely ignored since Hodges, and a systematic map of when F changes expressivity would be a useful contribution. The axiomatic treatment in Section 3 and the safety proofs for FO(=(·,·)), FO(|), FO(⊥), FO(=(·)), and FO(∼) are valuable and appear plausible. However, the two headline non-safety results — the unary anonymity separation and the sentence-level equivalence for FO(⊆,F) — rest on the errors detailed below, so the paper's central claims are not currently established.
major comments (3)
- [§5.1, proof of Theorem 5.1] The F-case defines φ*(R,x) = ∀y(¬R y ∨ θ(x,y)). This formula contains R in the scope of a negation, so R does not occur only positively as the theorem requires. Consequently the translation is not a GFP+-formula, and the appeal to the Galliani–Hella theorem in Corollary 5.2(i) is invalid. The same formula is reused in Lemma 5.9, so the dependence-logic result also needs a proof that the ESO formula is in the required class.
- [§5.3.2, Lemma 5.7] The hypothesis 'for any two points m1,m2∈M there exists f∈F with f(m1)=m1 and f(m2)≠m2' is unsatisfiable on any nonempty model when m1=m2, since it would require f(m)=m and f(m)≠m simultaneously. If the intended reading is 'distinct points', the anonymity-atom case still fails for assignments with s(x1)=s(x2): no automorphism fixing m can separate the two coordinates, so the required s' need not exist in Cl_F(X). In addition, on the even cycles B_n used in Corollary 5.8, antipodal vertices have the property that every automorphism fixing one also fixes the other, so the lemma's hypothesis is not met on B_n. Corollary 5.8 is therefore unsupported.
- [§5.3.1, Proposition 5.6] The proof is an informal narrative ('By construction, it is clear') and does not supply the induction or case analysis needed to verify that the FO(Υ1,F)-sentence is true on A_n and false on B_n for all n. Since this proposition is the positive half of the claimed unary-anonymity expressivity increase, a rigorous proof is required.
minor comments (5)
- [§3, Proposition 3.1(ii)] The proof chooses b'≠b and says the domain is non-empty by assumption; this only gives |M|≥1. The proof needs a standing assumption of at least two elements, or an explicit argument for singleton models.
- [§5.1, display (5.1)] The notation M⊨_s ψ*(S,x)[(s(x)=t)/S(t)] is not defined; substitution into a relation atom S(t) should be explained, and the relationship between the tuple variable y in θ and the tuple s(x) in the proof should be made explicit.
- [§5.4, proof of Lemma 5.9] The sentence 'the formula φ* that we need to take is exactly the same as for the translation from FO(⊆,F) to GFP+' is too terse; since the earlier formula is not in GFP+, the reader cannot tell which properties of φ* are being preserved for the ESO argument.
- [§5.6, proof of Proposition 5.17] The symbol 'M|=_X' should be 'M⊨_X', and the equivalence for first-order formulas should be justified by flatness of first-order formulas.
- [Conclusion] The term 'inconstancy logic' is mentioned in the conclusion but never defined in the paper; either define it or remove the reference.
Circularity Check
No significant circularity: the core results are deductive translations relying on independent external theorems; the Lemma 5.7 concern is a correctness issue, not a circularity.
full rationale
The paper's derivation chain does not fit any of the circular patterns. The flattening operator is defined independently in Definition 4.2, and its properties are proved semantically rather than assumed. The expressivity results are reductions to or from established results: Theorem 5.1 is a structural induction extending the Galliani-Hella translation to GFP+, Corollary 5.10 uses the Kontinen-Väänänen ESO-to-dependence translations, Corollary 5.11 uses Galliani's independence-logic theorem, and Proposition 5.17 uses Lück's normal form. Although the Kontinen-Väänänen papers share authors with this paper, they are prior published theorems with stated hypotheses that do not include the target results, so they count as independent support under the reviewing rules. Proposition 5.4 explicitly lifts Galliani's non-connectedness example, which is a citation of external evidence rather than a definitional smuggling of the conclusion. The one serious problem is Lemma 5.7: the stated magma condition is unsatisfiable for equal points, and the anonymity-atom step collapses for assignments with s(x1)=s(x2). This undermines Corollary 5.8, but the flaw is a mathematical error in a proof, not a self-referential definition, fitted prediction, or imported uniqueness theorem; it belongs on the correctness ledger, not the circularity ledger. Accordingly the circularity score is 0.
Assumptions & free parameters
assumptions (6)
- domain assumption Models have non-empty domains (invoked in the proof of Prop 3.1(ii): 'non-empty by assumption in this article').
- ad hoc to paper Lemma 5.7's magma condition: for any m1,m2∈M there is f∈F with f(m1)=m1 and f(m2)≠m2.
- standard math Galliani-Hella theorem: inclusion logic FO(⊆) is equivalent to the positive greatest fixed-point logic GFP+ for sentences (used in Theorem 5.1 and Cor 5.2).
- standard math Lück's normal form for FO(∼): every formula is equivalent to a finite disjunction of conjunctions of first-order formulas and Eβ (Prop 5.16).
- standard math Galliani's normal form for constancy logic (Prop 5.13).
- standard math Väänänen's translation of dependence logic to ESO and the ESO-definability of downward closed ESO formulas (KV09, KV11).
Cite this review
Pith. "Pith review of The flattening operator in team-based logics." pith.science (2026). https://pith.science/paper/B3TZ66ZJ
@misc{pith2026250521149,
author = {Pith},
title = {Pith review of: The flattening operator in team-based logics},
year = {2026},
howpublished = {\url{https://pith.science/paper/B3TZ66ZJ}},
note = {Machine review of arXiv:2505.21149}
}
read the original abstract
We propose a systematic study of the so-called flattening operator in team semantics. This operator was first introduced by Hodges in 1997, and has not been studied in more detail since. We begin a systematic study of the expressive power this operator adds to the most well-known team-based logics, such as dependence logic, anonymity logic, inclusion logic and exclusion logic.
Figures
Reference graph
Works this paper leans on
-
[115]
Modular SAT-based techniques for reasoning tasks in team semantics
doi: 10.1215/00294527-2019-0033 (cit. on p. 1). [Cor+19] Jukka Corander, Antti Hyttinen, Juha Kontinen, Johan Pensar, and Jouko Väänänen. “A logical approach to context-specific independence”. In:Annals of Pure and Applied Logic 170.9 (2019), pp. 975–992.doi: 10.1016/j.apal.2019.04.004 (cit. on p. 1). [Dur+18a] Arnaud Durand, Miika Hannula, Juha Kontinen,...
work page Pith review arXiv 2019
-
[2018]
url: https://urn.fi/URN:ISBN:978-952-03-0912-1 (cit. on p. 5). [Vää22] Jouko Väänänen. “An atom’s worth of anonymity”. In:Logic Journal of the IGPL 31.6 (2022), pp. 1078–1083.doi: 10.1093/jigpal/jzac074 (cit. on p. 5). [Vää07] Jouko Väänänen.Dependence logic: a new approach to independence friendly logic. London Mathematical Society Student Texts. Cambrid...
Reviewed August 7, 2026 · model on record in the stance chip above.
Discussion (0). Sign in to comment.