ExampleConstruction: AI-adaptedVerification: 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.

$(\emptyset, \emptyset) = {{\emptyset}}$ and $(\emptyset, {\emptyset}) = {{\emptyset}, {\emptyset, {\emptyset}}}$ , with the characterising property checked on them

Example

Unfolding the Kuratowski definition at the two smallest sets gives

$(\emptyset, \emptyset) = {{\emptyset}}, (\emptyset, {\emptyset}) = {{\emptyset}, {\emptyset, {\emptyset}}},$

and these two sets are distinct, as the characterising property requires, since $\emptyset \neq {\emptyset}$ .

Facts & Assumptions

Given: the sets $\emptyset$ and ${\emptyset}$ .

[L1]

$(a, b) : = {{a}, {a, b}}$ (The Kuratowski ordered pair $(a, b) : = {{a}, {a, b}}$ ).

[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}$ ).

[L3]

$(a, b) = (c, d)$ if and only if $a = c$ and $b = d$ ( $(a, b) = (c, d)$ if and only if $a = c$ and $b = d$ ).

[L4]

There is exactly one set with no elements (There is exactly one set with no elements, written $\emptyset$ ).

[L5]

If every $z$ satisfies $z \in x$ if and only if $z \in y$ , then $x = y$ (The Axiom of Extensionality: $\forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \to x = y)$ ).

Verification

technique · direct

1.1

$\emptyset \neq {\emptyset}$ , because ${\emptyset}$ has $\emptyset$ as an element and the empty set has none.

L2L4

1.2

$(\emptyset, \emptyset) = {{\emptyset}, {\emptyset, \emptyset}}$ by the definition, and ${\emptyset, \emptyset} = {\emptyset}$ , so both members of the outer pair are ${\emptyset}$ and the outer pair is ${{\emptyset}}$ .

L1L2L5

1.3

$(\emptyset, {\emptyset}) = {{\emptyset}, {\emptyset, {\emptyset}}}$ directly by the definition, with no collapse, since $\emptyset \neq {\emptyset}$ keeps the inner pair a set with two elements.

L1L2

2.1

The two pairs are distinct: their first coordinates agree but their second coordinates are $\emptyset$ and ${\emptyset}$ , which differ, so the characterising property forbids equality. This is visible in the computed sets as well, since ${\emptyset, {\emptyset}}$ is an element of the second and not of the first.

L3L5step 1.1step 1.2step 1.3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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

Ordered pair (Wikipedia) (standard reference, not scraped)
B. Kaya, MATH 320 Set Theory (METU), Def. 1 and Lemma 1 (standard reference, not scraped)
C. Wilson, A Brief Introduction to ZFC (Chicago REU 2016), Def. 2.6 (standard reference, not scraped)

(∅,∅)={{∅}}(∅,∅)={{∅}} and (∅,{∅})={{∅},{∅,{∅}}}(∅,{∅})={{∅},{∅,{∅}}}, with the characterising property checked on them