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.
Which of the five completeness properties carry the Archimedean property on their own, and which must be handed it
The statement of For an ordered field the five completeness properties are equivalent, provided the Archimedean property is assumed alongside nested intervals and Cauchy completeness attaches the Archimedean property to two of its five clauses and not to the other three. This remark says exactly why, clause by clause, and records what is proved on this page rather than what is customary.
The three that carry it. Each of the following is proved here, with no Archimedean hypothesis anywhere in sight:
- (LUB) implies the Archimedean property. This is claim 1 of An ordered field with the least-upper-bound property has the nested interval property and is Archimedean, which is Every complete ordered field is Archimedean applied to the field: a complete ordered field is Archimedean, because otherwise the canonical naturals would be a nonempty set bounded above, and then , being smaller than , is not an upper bound of , so some exceeds it and exceeds .
- (BW) implies the Archimedean property, by Bolzano-Weierstrass alone forces the Archimedean property, so it needs no separate Archimedean hypothesis. If the canonical naturals were bounded they would form a bounded sequence, and every subsequence of it has consecutive terms at distance at least , so no subsequence converges.
- (MCT) implies the Archimedean property, by The monotone convergence property alone forces the Archimedean property, so it carries no separate Archimedean hypothesis. If the canonical naturals were bounded above they would be a nondecreasing bounded sequence, hence convergent, hence Cauchy, which the gap of between consecutive terms forbids.
The two that do not. Neither (NIP) nor (CC) implies the Archimedean property, and one field refutes both: the formal Laurent series field is not Archimedean ( is non-Archimedean, and the monomials are cofinal below its positive elements), has (CC) (Every Cauchy sequence in converges: is sequentially Cauchy complete) and has (NIP) in the shrinking form of The five completeness properties of an ordered field: least upper bound, monotone convergence, nested intervals, Bolzano-Weierstrass, and Cauchy completeness ( has the nested interval property for lengths tending to ). The consequences are the two false statements of this page, FALSE: the nested interval property alone implies the least-upper-bound property and FALSE: an ordered field in which every Cauchy sequence converges has the least-upper-bound property: without the Archimedean hypothesis neither clause 2 nor clause 4 of the equivalence theorem implies clause 1.
What distinguishes the two groups. (LUB), (BW) and (MCT) each quantify over an object that is assumed only to be bounded: a bounded set, a bounded sequence, a nondecreasing sequence bounded above. In a non-Archimedean field the canonical naturals are such an object, so each of the three can be tested against them directly, and each fails on them at once. (NIP) and (CC) quantify instead over data that are already forced together: nested intervals whose lengths tend to in the field, and sequences whose terms get arbitrarily close to each other in the field. In a non-Archimedean field that is a much stronger hypothesis than it looks, because "arbitrarily close" now means below every infinitesimal as well; so few sequences and few interval families qualify, and the ones that do converge for reasons that have nothing to do with the naturals being cofinal.
Two corollaries worth stating plainly.
- An Archimedean hypothesis is never needed alongside (LUB), (BW) or (MCT), and writing one there is not merely redundant but misleading, since it suggests the property is weaker than it is.
- The customary phrase "complete ordered field" is ambiguous in exactly one place, and that place is (CC). This library resolves it by reserving complete for the least-upper-bound property (Complete ordered field (least-upper-bound property)) and always writing Cauchy complete for the other, as Every Cauchy sequence in converges: is sequentially Cauchy complete does. A text that says "the reals are the unique complete ordered field" and means (CC) is stating something false, and is the counterexample.
A note on what is not claimed. Nothing above says that (NIP) and (CC) are equivalent to each other, or that either is equivalent to the Archimedean property's negation, or that is the only witness. What is proved is the implication pattern of For an ordered field the five completeness properties are equivalent, provided the Archimedean property is assumed alongside nested intervals and Cauchy completeness and the two failures just named.
Depends on
- The five completeness properties of an ordered field: least upper bound, monotone convergence, nested intervals, Bolzano-Weierstrass, and Cauchy completeness
- Archimedean ordered field
- For an ordered field the five completeness properties are equivalent, provided the Archimedean property is assumed alongside nested intervals and Cauchy completeness
- An ordered field with the least-upper-bound property has the nested interval property and is Archimedean
- Bolzano-Weierstrass alone forces the Archimedean property, so it needs no separate Archimedean hypothesis
- The monotone convergence property alone forces the Archimedean property, so it carries no separate Archimedean hypothesis
- FALSE: the nested interval property alone implies the least-upper-bound property
- FALSE: an ordered field in which every Cauchy sequence converges has the least-upper-bound property
- Every complete ordered field is Archimedean
- $\mathbb{R}((t^{-1}))$ is non-Archimedean, and the monomials $t^{-k}$ are cofinal below its positive elements
- Every Cauchy sequence in $\mathbb{R}((t^{-1}))$ converges: $K$ is sequentially Cauchy complete
- $\mathbb{R}((t^{-1}))$ has the nested interval property for lengths tending to $0$
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: 84 results over 21 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
- Archimedean property (Wikipedia) (standard reference, not scraped)
- Completeness of the real numbers (Wikipedia) (standard reference, not scraped)