Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-06 (claude-opus-5)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Under Foundation, xxx \notin x for every set xx, there are no sets with xyxx \in y \in x, and there are no sets with xyzxx \in y \in z \in x

Statement

Assume the Axiom of Foundation. Then:

  • (i) xxx \notin x for every set xx;
  • (ii) there are no sets xx and yy with xyx \in y and yxy \in x;
  • (iii) there are no sets xx, yy and zz with xyx \in y, yzy \in z and zxz \in x.

Cycles of length greater than three are not treated here: stating "there is no membership cycle of any finite length" needs a finite sequence, that is a function on a natural number, and neither notion is available at this point in the reading order.

Facts & Assumptions

Proof

technique · contradiction
1.1

Suppose the statement fails, so that at least one of the following holds: there is a set xx with xxx \in x; there are sets xx and yy with xyx \in y and yxy \in x; there are sets xx, yy and zz with xyx \in y, yzy \in z and zxz \in x.

assume-contra
2.1

Suppose xxx \in x and put S:={x}S := \{x\}. Its only member is xx, so SS has a member and Foundation applies; the member it supplies must be xx, so xx shares no member with SS. But xxx \in x and xSx \in S, so xx is a member of both.

L1L2step 1.1
2.2

Suppose xyx \in y and yxy \in x, and put S:={x,y}S := \{x,y\}. Foundation supplies a member of SS sharing no member with SS, and that member is xx or yy. If it is xx, then yxy \in x and ySy \in S make yy a member of both; if it is yy, then xyx \in y and xSx \in S make xx a member of both.

L1L2step 1.1
2.3

Suppose xyx \in y, yzy \in z and zxz \in x, and put S:={x,y}{z}S := \{x,y\} \cup \{z\}, whose members are exactly xx, yy and zz. Foundation supplies a member of SS sharing no member with SS. If it is xx, then zxz \in x and zSz \in S; if it is yy, then xyx \in y and xSx \in S; if it is zz, then yzy \in z and ySy \in S. In each case that member shares a member with SS.

L1L2L3L4step 1.1
3.1

Each of the three suppositions contradicts the member Foundation supplies, so none of them holds: xxx \notin x for every xx, no sets satisfy xyxx \in y \in x, and no sets satisfy xyzxx \in y \in z \in x.

step 2.1step 2.2step 2.3discharge-contradiction

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 12 results over 6 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources