CounterexampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Transfinite induction fails if the least element is exempted from the hypothesis

Statement refuted

Refuted claim: the hypothesis of Transfinite induction may be checked only at elements other than the least element of the well-order: for a well-order $W$ with least element $m$ , if $W_{< a} \subseteq S$ implies $a \in S$ for every $a \neq m$ , then $S = W$ .

The witness is $W = ω$ with its usual order and $S = ω ∖ {0}$ (The natural numbers $N$ (von Neumann), Initial segment of a well-order). The implication holds at every $a \neq 0$ vacuously, because then $0 < a$ while $0 \notin S$ , so $W_{< a}$ is never contained in $S$ ; yet at $a = 0$ the initial segment $W_{< 0} = \emptyset$ is contained in $S$ while $0 \notin S$ . So the hypothesis of the theorem holds at every element except the least and fails at the least, and the conclusion $S = W$ is false. Hence the restriction to $a \neq m$ is not a valid form of the theorem: the least element needs no separate base case because the hypothesis applied there is the base case. No choice principle is used.

Facts & Assumptions

Given: The von Neumann naturals $N = ω$ with $0 = \emptyset$ , the additive order of Order on the natural numbers, the subset $S = ω ∖ {0}$ , and a well-order $(W, <)$ with least element $m$ as in the refuted claim, specialised below to $W = ω$ with its usual order.

[F1]

Transfinite induction: if $(W, <)$ is a well-order and $W_{< a} \subseteq S$ implies $a \in S$ for every $a \in W$ , then $S = W$ (Transfinite induction).

[F2]

For a well-order $(W, <)$ , $W_{< a} = {x \in W : x < a}$ (Initial segment of a well-order).

[F3]

For all naturals $m, n$ : $m < n$ if and only if $m \in n$ ; $n = {m \in N : m < n}$ ; $0 \leq n$ for every $n$ and $0 \in n$ whenever $n \neq 0$ (On $N$ the order is membership: $m < n ⟺ m \in n$ ).

[F4]

$0 = \emptyset$ and $σ (n) = n \cup {n}$ in $ω = N$ , and $0 \neq 1$ (The natural numbers $N$ (von Neumann)).

[F5]

The order of $N$ is defined by $m \leq n$ if and only if $m + k = n$ for some natural $k$ , with $m < n$ meaning $m \leq n$ and $m \neq n$ , and it is a linear order (Order on the natural numbers, $\leq$ is a linear order on $N$ ).

[F6]

Every nonempty subset of $N$ has a least element (The well-ordering principle).

[F7]

A well-order is a total order in which every nonempty subset has a least element (Well-order and well-ordered set).

Counterexample

technique · direct

1.1F3F5F6F7

The set $W = ω$ with its usual order is a well-order, and $0$ is its least element: the order of [F5] is linear, and every nonempty subset of $N$ has a least element by [F6], so $(ω, <)$ is a well-order in the sense of [F7]; and $0 \leq n$ for every $n$ by [F3], so $0$ is the least element.

1.2F2F3F4

Under the identification of membership with the order, $W_{< a} = a$ for every $a \in ω$ : $W_{< a} = {m \in ω : m < a}$ by [F2], and ${m \in N : m < a} = a$ by [F3]. In particular $W_{< 0} = \emptyset$ , since $0 = \emptyset$ by [F4].

1.3F4

$S = ω ∖ {0}$ is a subset of $W$ with $0 \notin S$ and $S \neq W$ , because $0 \in W$ by [F4].

2.1step 1.3F3

For every $a \in ω$ with $a \neq 0$ the implication $W_{< a} \subseteq S \Rightarrow a \in S$ holds vacuously: $0 < a$ by [F3], so $0 \in W_{< a}$ while $0 \notin S$ by step 1.3, and therefore $W_{< a}$ is not contained in $S$ .

2.2step 1.2step 1.3

At the least element $a = 0$ the hypothesis fails: $W_{< 0} = \emptyset \subseteq S$ by step 1.2, while $0 \notin S$ by step 1.3, so $W_{< 0} \subseteq S$ holds and $0 \in S$ does not.

3.1step 1.1step 1.3step 2.1step 2.2F1∎

The refuted claim is therefore false: the well-order $W = ω$ has least element $0$ by step 1.1, the implication $W_{< a} \subseteq S \Rightarrow a \in S$ holds for every $a \neq 0$ by step 2.1, yet $S \neq W$ by step 1.3, so the conclusion $S = W$ fails. The hypothesis of [F1] is exactly the statement at every $a \in W$ , including $a = 0$ , and step 2.2 shows that the instance at the least element is what supplies the base case; exempting it removes precisely the step that forces $0 \in S$ . No choice principle is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 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

A. Marks, Set Theory (Berkeley lecture notes, 2026) (standard reference, not scraped)
J. T. Moore, MATH 6870: Set Theory (Cornell lecture notes) (standard reference, not scraped)