REVIEW 1 major objections 3 minor 12 references
On double-membership graphs of models of Anti-Foundation
T0 review · 1 major / 3 minor · reviewed 2026-08-14 · deepseek-v4-flash
Pith's one-line read The double-membership graph of a model of Anti-Foundation has exactly the connected components of the graphs that live inside that model, and its complete theory is the set of consistency statements the model satisfies.
desk verdict A well-written, niche paper with genuinely new results and one easily fixed proof gap in Corollary 4.7. 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 two load-bearing devices are flat systems of equations and regions. Anti-Foundation in the form of the Solution Lemma (Definition 1.1) says every flat system {x_i = S_i} has a unique solution; Proposition 2.3 uses this to turn any graph G internal to M into an isomorphic copy of G inside M1 that is a union of regions and is an M-set, where the region of a is the set of points reachable from a by D in the sense of M. This one proposition carries the component classification and also, via the sentence μ(φ) = 'there is a loopless point whose neighbours form a model of φ', translates internal consistency statements into first-order sentences of the graph. The proof of Theorem 4.14 then runs an Ehrenfeucht-Fraïssé game in which the Duplicator answers each move by replicating the ≡k-class of a region, using Lemma 4.5 to replace an internal graph satisfying φ by an isomorphic union of regions in the other model.
What would settle it
Find a model M of ZFA whose D-graph has a connected component not isomorphic to any connected component of a graph internal to M, which would falsify Theorem 2.4; or find two models M and N of ZFA satisfying exactly the same consistency statements whose D-graphs are not elementarily equivalent, which would falsify Theorem 4.14.
Extended reading notes
Core claim
The central discovery is a precise correspondence between the external double-membership graph M1 of a model M of ZFA and the internal graphs of M. Theorem 2.4 states that the connected components of M1, taken in the metatheory, are up to isomorphism exactly the connected components of graphs in the sense of M, each appearing infinitely often. The second main theorem, Theorem 4.14, states that for models M and N of ZFA, M1 ≡ N1 if and only if M and N satisfy the same consistency statements—i.e. the same sentences of the form 'the L1-sentence φ has a model'—and equivalently the same sentences μ(φ) asserting that some loopless point has a neighbour set that is a model of φ. A corollary is that the common theory of all D-graphs is incomplete, its completions are indexed by consistent collections of consistency statements, and every completion is neostability-wild: each of its models interprets arbitrarily large finite fragments of ZFC with parameters.
Load-bearing premise
The proof needs the existence half of the Anti-Foundation Axiom—every flat system of equations has a solution—and without such solutions the constructions that embed internal graphs into the double-membership graph collapse.
Editorial extensions
If this is right
- Component classification reduces the existence question to internal graph theory: an isomorphism type appears as a component of M1 exactly when some connected graph of that type exists inside M, and it appears infinitely many times.
- Because each completion is realized by continuum-many countable pairwise non-isomorphic models and some countable elementarily equivalent graph is not a reduct, the D-graph and SD-graph classes are not ℵ0-categorical and their theories are not the theories of a single structure up to isomorphism.
- Every model of every D-graph theory interprets arbitrarily large finite fragments of ZFC, so these theories have the strict order property, TP2, and the independence property for every k; the class is wild in neostability terms.
- The negative answer to Question 5 means that being elementarily equivalent to a reduct does not guarantee being a reduct: there are countable graph structures with the same first-order theory that no model of ZFA produces.
Reading between the lines
- Because the paper notes that uniqueness of solutions is never used, the component classification and the consistency-statement correspondence should survive if ZFA is weakened to the existence-only axiom AFA1 (axiom X); the same statements can be tested there.
- The proof strategy of Theorem 4.14 resembles a Gaifman/Hanf argument, so one could presumably axiomatize the completions by all local sentences rather than only the μ(φ) subclass, though such an axiomatization would likely be less informative than Corollary 4.15.
- The construction in Theorem 4.16—deleting infinite-diameter components—suggests a general recipe for building elementarily equivalent non-reducts for other reducts of set theory, as long as an internal-graph-existence principle analogous to Proposition 2.3 holds.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper studies the double-membership graphs (D-graphs) and single-double-membership graphs (SD-graphs) of models of ZFA, i.e. the reducts obtained from the relations x∈y∧y∈x and its symmetrization. The main results are: (i) a characterization of the connected components of D-graphs as exactly the metatheoretic connected components of graphs in the sense of M, each appearing infinitely often (Theorem 2.4); (ii) the existence of 2^ℵ0 non-isomorphic countable D-graphs elementarily equivalent to a given one, and 2^ℵ0 countable models of each of their theories (Corollary 3.5); (iii) the incompleteness of the common theory of D-graphs and a description of its completions in terms of consistency statements (Theorem 4.14, Corollary 4.15); and (iv) a negative answer to the question whether every countable structure elementarily equivalent to an SD-graph (or D-graph) of a model of ZFA is itself such a reduct (Corollary 4.17). The proofs use the Solution Lemma form of AFA, type-counting, and Ehrenfeucht-Fraïssé games.
Significance. If the results hold, they substantially advance the model-theoretic study of non-well-founded set-theoretic graphs initiated in [ADC17], giving a structural description of connected components and a classification of the theories involved in terms of consistency statements. The paper also contains a negative result showing that the class of D-graphs (and SD-graphs) is not closed under elementary equivalence among countable structures, and that these theories are wild from the neostability perspective. A particular strength is the use of the Solution Lemma to transfer arbitrary internal graphs into actual connected components, and the self-contained EF-game argument in Theorem 4.16. The proofs are detailed and largely self-contained, with standard references cited for background facts. However, one load-bearing step in the consistency-statement correspondence is not proved as stated, as detailed below.
major comments (1)
- [§4, Corollary 4.7] The proof of Corollary 4.7 applies Lemma 4.5 to ϕ := θ′, but Lemma 4.5 is proved only for ϕ ∈ Φ, i.e., L1-sentences that imply ∀x∀y(D(x,y)→D(y,x)). Fact 4.6 does not guarantee that θ′ lies in Φ: an LNBG-sentence such as ∃x∃y(E(x,y)∧¬E(y,x)) is consistent and has no symmetric model, so its translation θ′ is consistent in L1 but is not in Φ. For such θ′, M⊨Con(θ) need not imply M1⊨μ(θ′), because the neighbour set of any point in M1 is symmetric. Consequently the proof of the equivalence (2)⇔(3) in Theorem 4.14, as well as Corollaries 4.8, 4.11, and 4.15, is incomplete as written. This is repairable: replacing θ′ by θ′∧∀x∀y(D(x,y)→D(y,x)) preserves consistency equivalence, since the graph interpretation in Fact 4.6 is always symmetric, and brings the sentence into Φ. The authors should state this modification explicitly and verify that all later applications go through with the strengthened sentence.
minor comments (3)
- [§4, Theorem 4.16] The definition 'r_j := (3j−1)/2' appears to be a typo; the subsequent inclusion argument requires r_{j+1} ≥ 3r_j+1, which holds for r_j = (3^j−1)/2, not for the linear expression written.
- [§1, Remark 1.3] The phrase 'models of ZFC with Foundation replaced by AFA1' should be 'models of ZFC without Foundation and with AFA1' to avoid ambiguity about whether Foundation is kept.
- [§4, Fact 4.10] The notation '~ψ' for the associated arithmetical statement is awkward; using a tilde accent (e.g. ψ̃) or a different symbol would improve readability.
Circularity Check
No significant circularity: the main theorems are derived from AFA and standard model theory; self-citations are background only.
full rationale
The paper's central results are derived in-paper. Theorem 2.4 characterises connected components of D-graphs via Proposition 2.3, which is proved from the Solution Lemma by solving a flat system built from an M-graph; this is a genuine construction, not a restatement of the conclusion. Lemma 3.2 cites [ADC17, Theorem 4] as an optional shortcut, but it also follows from Proposition 2.3, so the self-citation is not load-bearing. The completeness/consistency characterisation in Theorem 4.14 is established by an Ehrenfeucht-Fraïssé strategy using Lemma 4.5 and standard interpretability facts (Hodges), together with external results of Rosser and Smorynski for the incompleteness of the common theory. No parameter is fitted and no earlier result is renamed as a prediction. The equivalence M1≡N1 iff M,N satisfy the same consistency statements is proved rather than assumed, and the consistency statements themselves are independent inputs (sentences in other languages interpreted into graphs). The few citations to the first author's prior work [ADC17] provide background or weaker special cases; removing them would not collapse the derivations. A possible technical caveat about whether the translation θ′ of Fact 4.6 satisfies the symmetry condition of Lemma 4.5 when applied in Corollary 4.7 is a correctness concern, not a circularity: it concerns whether a step of the proof is valid, not whether the conclusion is assumed as an input.
Assumptions & free parameters
assumptions (7)
- domain assumption The ambient metatheory is ZFC + Con(ZFC).
- domain assumption The object theory is ZFA, whose Anti-Foundation Axiom is used in the form of the Solution Lemma (Definition 1.1).
- standard math Rosser's Theorem and Fact 4.10 (Smorynski 1985, Chapter 7) are available.
- standard math ZFC proves the completeness theorem, so internal Con(theta) is equivalent to existence of a set model.
- standard math Fact 3.4: every partial type over empty of a countable theory is realized in a countable model.
- standard math Rieger's permutation model construction (as in Kunen IV.18) yields a model of ZFC without Foundation with a prescribed membership permutation.
- standard math Hodges' Theorem 5.5.1: every digraph is interpretable in a graph, uniformly, preserving consistency (Fact 4.6).
Cite this review
Pith. "Pith review of On double-membership graphs of models of Anti-Foundation." pith.science (2026). https://pith.science/paper/VFTVCHGD
@misc{pith2026190802708,
author = {Pith},
title = {Pith review of: On double-membership graphs of models of Anti-Foundation},
year = {2026},
howpublished = {\url{https://pith.science/paper/VFTVCHGD}},
note = {Machine review of arXiv:1908.02708}
}
abstract
We answer some questions about graphs which are reducts of countable models of Anti-Foundation, obtained by considering the binary relation of double-membership $x\in y\in x$. We show that there are continuum-many such graphs, and study their connected components. We describe their complete theories and prove that each has continuum-many countable models, some of which are not reducts of models of Anti-Foundation.
Figures
Reference graph
Works this paper leans on
-
[1]
P. Aczel . Non-Wellfounded Sets, volume 14 of CSLI Lecture Notes . CSLI Publications (1988)
work page 1988
-
[2]
Undirecting membership in models of ZFA
B. Adam-Day and P. Cameron . Undirecting membership in models of ZFA . Preprint available at https://arxiv.org/abs/1708.07943 (submitted, 2017)
work page Pith review arXiv 2017
-
[3]
J. Barwise and L. S. Moss . Vicious Circles, volume 60 of CSLI Lecture Notes . CSLI Publications (1996)
work page 1996
-
[4]
P. Cameron . The Random Graph . In The Mathematics of Paul Erd o s , edited by R. L. Graham , J. Ne set ril and S. Butler , volume 2, pages 353--378. Springer (2013)
work page 2013
-
[5]
H.-D. Ebbinghaus and J. Flum . Finite model theory. Springer Monographs in Mathematics. Springer-Verlag (1995)
work page 1995
-
[6]
U. Felgner . Comparison of the axioms of local and universal choice. Fundamenta Mathematicae, 71:43--62 (1971)
work page 1971
-
[7]
M. Forti and F. Honsell . Set theory with free construction principles. Annali della Scuola Normale Superiore di Pisa --- Classe di Scienze , 10:493--522 (1983)
work page 1983
-
[8]
W. Hodges . Model Theory, volume 42 of Encyclopedia of Mathematics and its Applications. Cambridge University Press (1993)
work page 1993
Show all 12 references
-
[9]
K. Kunen . Set theory, volume 102 of Studies in logic and the foundations of mathematics. North Holland (1980)
1980
-
[10]
M. Otto . Finite model theory. https://www.karlin.mff.cuni.cz/ krajicek/otto.pdf (2006)
2006
-
[11]
L. Rieger . A contribution to G\"odel's axiomatic set theory, I . Czechoslovak Mathematical Journal, 07:323--357 (1957)
1957
-
[12]
Smorynski
C. Smorynski . Self-reference and modal logic. Universitext. Springer (1985)
1985
Reviewed August 14, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.