Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)
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.

The empty set is bounded and has no supremum

Statement refuted

Refuted claim: every subset of R\mathbb{R} has a supremum in R\mathbb{R} (FALSE: every subset of R\mathbb{R} has a supremum).

The witness here is ∅\emptyset, and it fails for the opposite reason to the unbounded witness An unbounded set has no supremum: the naturals inside R\mathbb{R}. The empty set is bounded, in fact bounded above and below by every real number at once (Lower bound, bounded below, bounded set), so the set of its upper bounds is all of R\mathbb{R}. A supremum would be a least element of that set, and R\mathbb{R} has no least element, because w−1<ww - 1 < w for every ww. What fails is therefore the nonemptiness hypothesis of the least-upper-bound property (Complete ordered field (least-upper-bound property)), not boundedness.

Facts & Assumptions

Given: The complete ordered field R\mathbb{R} and its empty subset ∅\emptyset.

[L1]

Upper bound, lower bound, bounded, supremum: uu is an upper bound of XX when x≤ux \le u for every x∈Xx \in X and ℓ\ell is a lower bound when ℓ≤x\ell \le x for every x∈Xx \in X; XX is bounded when it has both; and a supremum of XX is an upper bound uu of XX with u≤u′u \le u' for every upper bound u′u' of XX (Complete ordered field (least-upper-bound property), Lower bound, bounded below, bounded set).

[L2]

Order: 0<10 < 1; adding a constant preserves the order, so 0<10 < 1 gives w−1<ww - 1 < w for every ww; and trichotomy holds, so a<ba < b and b≤ab \le a cannot both be true (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Ordered field, Complete ordered field (least-upper-bound property)).

[L3]

The refuted claim: every S⊆RS \subseteq \mathbb{R} has a supremum in R\mathbb{R} (FALSE: every subset of R\mathbb{R} has a supremum).

Counterexample

technique · direct
1.1

Every w∈Rw \in \mathbb{R} is both an upper bound and a lower bound of ∅\emptyset: the defining condition quantifies over no elements and so holds vacuously. In particular ∅\emptyset is bounded, and its set of upper bounds is all of R\mathbb{R}.

L1
1.2

Let w∈Rw \in \mathbb{R} be an arbitrary upper bound of ∅\emptyset.

assume-hyp
2.1

The number w−1w - 1 is also an upper bound of ∅\emptyset, by 1.1, and w−1<ww - 1 < w, since 0<10 < 1 gives w−1<(w−1)+1=ww - 1 < (w - 1) + 1 = w on adding w−1w - 1 to both sides.

step 1.1step 1.2L2
3.1

Hence w≤w−1w \le w - 1 fails by trichotomy, so ww is not ≤\le every upper bound of ∅\emptyset and is therefore not a supremum of ∅\emptyset; as ww was an arbitrary upper bound, and every real is one, no real number is a supremum of ∅\emptyset.

step 2.1step 1.2L1L2
4.1

So ∅\emptyset is a bounded subset of R\mathbb{R} with no supremum in R\mathbb{R}: the claim that every subset of R\mathbb{R} has a supremum is refuted, this time by a set that is bounded but not nonempty, and the nonemptiness hypothesis of the least-upper-bound property cannot be dropped either.

step 3.1step 1.1L3∎

Remarks

  • The same argument, applied to lower bounds, shows that ∅\emptyset has no infimum either: every real is a lower bound and there is no greatest real, since w<w+1w < w + 1 for every ww.
  • Together with An unbounded set has no supremum: the naturals inside R\mathbb{R} this shows that both hypotheses of the least-upper-bound property are load bearing, and that they fail independently: ∅\emptyset is bounded and not nonempty, while the naturals inside R\mathbb{R} are nonempty and not bounded above. Neither witness alone would establish that.
  • Some texts repair the refuted claim by declaring sup⁡∅=−∞\sup \emptyset = -\infty in the extended reals. That convention is consistent and is discussed in Conventions: sup⁡∅\sup \emptyset, unbounded sets, and the extended reals; this library does not adopt it, because −∞-\infty is not an element of R\mathbb{R}.
  • The convention sup⁡∅=−∞\sup \emptyset = -\infty is exactly the assertion that the empty set has a least upper bound in a larger ordered set in which every element bounds ∅\emptyset above and −∞-\infty is least. That larger set is not a field, which is why Conventions: sup⁡∅\sup \emptyset, unbounded sets, and the extended reals keeps it out of the statements proved here rather than adopting it by default.

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: 13 results over 8 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