Alphabeta Math
False statementConstruction: Literature-sourcedVerification: 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.

FALSE: for every formula φ\varphi of the language of set theory there is a set {x:φ(x)}\{\, x : \varphi(x) \,\}

Statement

False statement. For every formula φ(x)\varphi(x) of the language of set theory (The first-order language of set theory: \in, ==, formulas with parameters, and class abbreviations) there is a set whose elements are exactly the sets satisfying φ\varphi; that is, every instance of

yx(xyφ(x))\exists y\,\forall x\,\bigl(x \in y \leftrightarrow \varphi(x)\bigr)

holds. This is the unrestricted comprehension schema, and it is the principle The Axiom Schema of Separation: for each formula φ\varphi, pˉxyz(zy(zxφ(z,pˉ)))\forall \bar p\,\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar p))) deliberately weakens.

Facts & Assumptions

Given: the claim above, asserted for every formula of the language (The first-order language of set theory: \in, ==, formulas with parameters, and class abbreviations).

[L1]

There is no set RR such that, for every set xx, xRx \in R holds if and only if xxx \notin x (There is no RR with xRxxx \in R \leftrightarrow x \notin x for every xx).

[L2]

There is no set UU such that yUy \in U for every set yy (There is no set UU with yUy \in U for every set yy).

Refutation

technique · contradiction
1.1

Suppose the schema holds for every formula of the language.

assume-contra
2.1

Instantiate it at the formula φ(x):=xx\varphi(x) := x \notin x: there is a set RR such that, for every set xx, xRx \in R holds if and only if xxx \notin x.

step 1.1
3.1

No such set exists, so the supposition fails and the schema is false. Instantiating instead at φ(x):=x=x\varphi(x) := x = x produces a set with every set as an element, which is impossible for the same underlying reason.

L1L2step 2.1discharge-contradiction

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 6 results over 4 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