Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck 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, x∉x for every set x, there are no sets with x∈y∈x, and there are no sets with x∈y∈z∈x

Statement

Assume the Axiom of Foundation. Then:

  • (i) x∉x for every set x;
  • (ii) there are no sets x and y with x∈y and y∈x;
  • (iii) there are no sets x, y and z with x∈y, y∈z and z∈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

Given: the Axiom of Foundation.

[L2]

{x,y} is the set whose elements are exactly x and y, and {x}:={x,x} (The unordered pair {x,y} and the singleton {x}={x,x}).

Proof

technique · contradiction
1.1

Suppose the statement fails, so that at least one of the following holds: there is a set x with x∈x; there are sets x and y with x∈y and y∈x; there are sets x, y and z with x∈y, y∈z and z∈x.

assume-contra
2.1

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

L1L2step 1.1
2.2

Suppose x∈y and y∈x, and put S:={x,y}. Foundation supplies a member of S sharing no member with S, and that member is x or y. If it is x, then y∈x and y∈S make y a member of both; if it is y, then x∈y and x∈S make x a member of both.

L1L2step 1.1
2.3

Suppose x∈y, y∈z and z∈x, and put S:={x,y}∪{z}, whose members are exactly x, y and z. Foundation supplies a member of S sharing no member with S. If it is x, then z∈x and z∈S; if it is y, then x∈y and x∈S; if it is z, then y∈z and y∈S. In each case that member shares a member with S.

L1L2L3L4step 1.1
3.1

Each of the three suppositions contradicts the member Foundation supplies, so none of them holds: x∉x for every x, no sets satisfy x∈y∈x, and no sets satisfy x∈y∈z∈x.

step 2.1step 2.2step 2.3discharge-contradiction∎

Depends on

Used by

Dependency tree · two levels

10 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources