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

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

Statement

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

∃y ∀x (x∈y↔φ(x))

holds. This is the unrestricted comprehension schema, and it is the principle The Axiom Schema of Separation: for each formula φ, ∀pˉ ∀x ∃y ∀z (z∈y↔(z∈x∧φ(z,pˉ))) deliberately weakens.

Facts & Assumptions

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

[L1]

There is no set R such that, for every set x, x∈R holds if and only if x∉x (There is no R with x∈R↔x∉x for every x).

[L2]

There is no set U such that y∈U for every set y (There is no set U with y∈U for every set y).

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):=x∉x: there is a set R such that, for every set x, x∈R holds if and only if x∉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 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 · two levels

5 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