Alphabeta Math
Session-authored (Fable 5 assisted)
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.

28 results · all verified · 17 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 11 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Construction of the Real Numbers via Dedekind Cuts

1 · Prerequisites

2 · Summary

Objective. This page constructs the real number field R\mathbb{R} via Dedekind cuts and proves that R\mathbb{R} is a totally ordered field with the least-upper-bound property. The natural numbers N\mathbb{N}, with their arithmetic and order, are the assumed starting point.

Foundations (N\mathbb{N} to Q\mathbb{Q}). The construction of the integers and the rationals is shared verbatim with the Cauchy-sequence construction, so we take it as given: Z\mathbb{Z} is built from N\mathbb{N} as a totally ordered commutative ring (The integers form a totally ordered ring), and Q\mathbb{Q} from Z\mathbb{Z} as a totally ordered, Archimedean field (The rationals form a totally ordered field, The rationals are Archimedean). Only the final passage from Q\mathbb{Q} to R\mathbb{R} differs between the two constructions, and it is the subject of this page.

The gap in Q\mathbb{Q}. Order-completeness fails in Q\mathbb{Q}: the set {q:q2<2}\{ q : q^2 < 2 \} is bounded above yet has no rational least upper bound. A Dedekind cut fills exactly such a gap, naming the missing bound by the rationals that lie below it.

Cuts and the reals. A Dedekind cut is a subset AQA \subseteq \mathbb{Q} that is nonempty and proper, downward closed, and without a greatest element (Dedekind cut): the set of all rationals lying strictly below a point of the line. The reals are defined to be the set of all cuts (The real numbers R\mathbb{R} as Dedekind cuts), ordered simply by inclusion (Order on the Dedekind reals), which is a total order (Inclusion totally orders the Dedekind reals).

Arithmetic. Addition is the sumset A+BA + B, with a subtle additive inverse A-A chosen so that A+(A)=0A + (-A) = 0^{*} (Addition, negation, and subtraction of Dedekind cuts, For a cut AA, A-A is a cut and A+(A)=0A + (-A) = 0^{*}). Multiplication is defined first on the nonnegative cuts and then extended by signs (Multiplication and reciprocals of Dedekind cuts, For a positive cut AA, the reciprocal A1A^{-1} satisfies AA1=1A \cdot A^{-1} = 1^{*}). These operations make R\mathbb{R} a field (The Dedekind reals form a field) into which Q\mathbb{Q} embeds densely, preserving sums, products, 00, 11 and the order (The rational cuts embed densely in R\mathbb{R}, preserving sums, products, 00, 11 and the order).

Order. Inclusion makes this field totally ordered (The Dedekind reals form a totally ordered field) and Archimedean (The Dedekind reals are Archimedean), so the rational cuts stay cofinal in R\mathbb{R}.

Destination. R\mathbb{R} is order-complete: every nonempty set of cuts bounded above has a least upper bound, obtained as nothing more than the union of the cuts (Dedekind completeness: the least-upper-bound property). This least-upper-bound property is the payoff of the construction, the order-theoretic counterpart of the Cauchy completeness delivered by the sequence construction (The reals are complete). It is also what a cut was designed to supply: each cut simply is the supremum of the rationals beneath it, so the holes in Q\mathbb{Q} are filled once and for all.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-24Open item page →

The integers as equivalence classes of pairs of naturals

Definition

On the set N×N\mathbb{N} \times \mathbb{N} of pairs of natural numbers, define

(a,b)(c,d)    a+d=b+c.(a,b) \sim (c,d) \iff a + d = b + c.

This is an equivalence relation (The integer-defining relation is an equivalence relation ). The integers are the quotient

Z:=(N×N)/,\mathbb{Z} := (\mathbb{N} \times \mathbb{N}) / \sim,

and we write [(a,b)][(a,b)] for the equivalence class of (a,b)(a,b).

Remarks

  • The pair (a,b)(a,b) encodes the formal difference aba - b; the defining relation a+d=b+ca + d = b + c is the equation "ab=cda - b = c - d" restated using only addition, which is all N\mathbb{N} has.
  • N\mathbb{N} and its arithmetic (commutativity, associativity, distributivity, cancellation of addition, the order) are taken as given background throughout this construction.
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The integer-defining relation is an equivalence relation

Statement

The relation (a,b)(c,d)    a+d=b+c(a,b) \sim (c,d) \iff a + d = b + c on N×N\mathbb{N} \times \mathbb{N} (The integers as equivalence classes of pairs of naturals) is an equivalence relation.

Facts & Assumptions

Given: The relation (a,b)(c,d)    a+d=b+c(a,b) \sim (c,d) \iff a + d = b + c on N×N\mathbb{N} \times \mathbb{N}.

[A1]

Addition on N\mathbb{N} is commutative and associative.

[A2]

Cancellation in N\mathbb{N}: if x+z=y+zx + z = y + z then x=yx = y.

Proof

technique · direct
1.1

Reflexivity: for any (a,b)(a,b) we have a+b=b+aa + b = b + a, so (a,b)(a,b)(a,b) \sim (a,b).

A1
1.2

Symmetry: suppose (a,b)(c,d)(a,b) \sim (c,d), i.e. a+d=b+ca + d = b + c. Then c+b=d+ac + b = d + a, which is the defining equation for (c,d)(a,b)(c,d) \sim (a,b).

A1
1.3

Suppose (a,b)(c,d)(a,b) \sim (c,d) and (c,d)(e,f)(c,d) \sim (e,f), i.e. a+d=b+ca + d = b + c and c+f=d+ec + f = d + e.

given
2.1

Adding the two equations: (a+d)+(c+f)=(b+c)+(d+e)(a + d) + (c + f) = (b + c) + (d + e).

step 1.3algebra
3.1

Regrouping both sides: (a+f)+(c+d)=(b+e)+(c+d)(a + f) + (c + d) = (b + e) + (c + d).

step 2.1A1
4.1

Cancelling (c+d)(c + d): a+f=b+ea + f = b + e, so (a,b)(e,f)(a,b) \sim (e,f); the relation is transitive.

step 3.1A2
5.1

The relation is reflexive, symmetric, and transitive, hence an equivalence relation.

step 1.1step 1.2step 4.1
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-24Open item page →

Arithmetic on the integers

Definition

On Z\mathbb{Z} (The integers as equivalence classes of pairs of naturals) define, on representatives,

[(a,b)]+[(c,d)]:=[(a+c,  b+d)],[(a,b)] + [(c,d)] := [(a+c,\; b+d)], [(a,b)][(c,d)]:=[(ac+bd,  ad+bc)],[(a,b)] \cdot [(c,d)] := [(ac+bd,\; ad+bc)], [(a,b)]:=[(b,a)],0:=[(0,0)],1:=[(1,0)].-[(a,b)] := [(b,a)], \qquad 0 := [(0,0)], \qquad 1 := [(1,0)].

These do not depend on the chosen representatives (Integer addition and negation are well defined , Integer multiplication is well defined ).

Remarks

  • The product formula is forced by the intended meaning: if (a,b)(a,b) stands for aba-b and (c,d)(c,d) for cdc-d, then (ab)(cd)=(ac+bd)(ad+bc)(a-b)(c-d) = (ac+bd) - (ad+bc).
  • Negation swaps the components: (ab)=ba-(a-b) = b-a.
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

Integer addition and negation are well defined

Statement

The operations [(a,b)]+[(c,d)]=[(a+c,b+d)][(a,b)] + [(c,d)] = [(a+c, b+d)] and [(a,b)]=[(b,a)]-[(a,b)] = [(b,a)] on Z\mathbb{Z} (Arithmetic on the integers) are independent of the chosen representatives.

Facts & Assumptions

Given: Pairs with (a,b)(a,b)(a,b) \sim (a',b') and (c,d)(c,d)(c,d) \sim (c',d') in the sense of The integers as equivalence classes of pairs of naturals.

[A1]

Addition on N\mathbb{N} is commutative and associative.

Proof

technique · direct
1.1

By hypothesis a+b=b+aa + b' = b + a'.

given
1.2

By hypothesis c+d=d+cc + d' = d + c'.

given
2.1

Adding the two equations: (a+b)+(c+d)=(b+a)+(d+c)(a + b') + (c + d') = (b + a') + (d + c').

step 1.1step 1.2algebra
2.2

Commuting the equation of step 1.1: b+a=a+bb + a' = a + b', which is the defining equation for (b,a)(b,a)(b,a) \sim (b',a'); negation is well defined.

step 1.1A1
3.1

Regrouping both sides: (a+c)+(b+d)=(b+d)+(a+c)(a+c) + (b'+d') = (b+d) + (a'+c'), which is the defining equation for (a+c,b+d)(a+c,b+d)(a+c,\, b+d) \sim (a'+c',\, b'+d'); addition is well defined.

step 2.1A1
4.1

Both operations are independent of representatives.

step 3.1step 2.2
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

Integer multiplication is well defined

Statement

The operation [(a,b)][(c,d)]=[(ac+bd,ad+bc)][(a,b)] \cdot [(c,d)] = [(ac+bd,\, ad+bc)] on Z\mathbb{Z} (Arithmetic on the integers) is independent of the chosen representatives.

Facts & Assumptions

Given: Pairs with (a,b)(a,b)(a,b) \sim (a',b') and (c,d)(c,d)(c,d) \sim (c',d') in the sense of The integers as equivalence classes of pairs of naturals.

[A1]

Addition on N\mathbb{N} is commutative and associative.

[A2]

Multiplication on N\mathbb{N} is commutative.

[A3]

Distributivity in N\mathbb{N}: x(y+z)=xy+xzx(y+z) = xy + xz.

Proof

technique · direct
1.1

By hypothesis a+b=b+aa + b' = b + a'; write ss for this common value.

given
1.2

Regrouping and factoring: (ac+bd)+(ad+bc)=c(a+b)+d(b+a)(ac+bd) + (a'd+b'c) = c(a+b') + d(b+a').

A1A2A3
1.3

Regrouping and factoring: (ad+bc)+(ac+bd)=d(a+b)+c(b+a)(ad+bc) + (a'c+b'd) = d(a+b') + c(b+a').

A1A2A3
2.1

By step 1.1 both right-hand sides equal cs+dscs + ds, so (ac+bd)+(ad+bc)=(ad+bc)+(ac+bd)(ac+bd) + (a'd+b'c) = (ad+bc) + (a'c+b'd).

step 1.1step 1.2step 1.3
3.1

That equation is precisely the defining relation (ac+bd,ad+bc)(ac+bd,ad+bc)(ac+bd,\, ad+bc) \sim (a'c+b'd,\, a'd+b'c): the product class is unchanged when the first factor's representative changes.

step 2.1
4.1

The product formula is symmetric in its two arguments: swapping (a,b)(c,d)(a,b) \leftrightarrow (c,d) sends (ac+bd,ad+bc)(ac+bd,\, ad+bc) to (ca+db,cb+da)(ca+db,\, cb+da), the same pair. Hence, by the argument of steps 1.1–3.1 applied to the second factor, the product class is also unchanged when (c,d)(c,d) is replaced by (c,d)(c',d').

step 3.1A1A2
5.1

Replacing first (a,b)(a,b) by (a,b)(a',b') and then (c,d)(c,d) by (c,d)(c',d'): [(a,b)][(c,d)]=[(a,b)][(c,d)]=[(a,b)][(c,d)][(a,b)] \cdot [(c,d)] = [(a',b')] \cdot [(c,d)] = [(a',b')] \cdot [(c',d')]; multiplication is well defined.

step 3.1step 4.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

The integers form a commutative ring

Statement

(Z,+,,0,1)(\mathbb{Z}, +, \cdot, 0, 1) with the operations of Arithmetic on the integers is a commutative ring with multiplicative identity, in which every element has the additive inverse [(a,b)]=[(b,a)]-[(a,b)] = [(b,a)].

Facts & Assumptions

Given: Z\mathbb{Z} with the operations of Arithmetic on the integers.

[L1]

Addition on N\mathbb{N} is commutative and associative, with zero as a two-sided identity (Addition is commutative, Addition is associative, Left identity for addition).

[L2]

Multiplication on N\mathbb{N} is commutative and associative, distributes over addition, and has the usual zero and identity laws (Multiplication is commutative, Multiplication is associative, Distributivity and the successor law for multiplication, Zero and one under multiplication).

[L3]

The integer operations are independent of representatives (Integer addition and negation are well defined, Integer multiplication is well defined).

Proof

technique · direct
1.1

By [L3], each axiom may be verified on arbitrary fixed representatives (a,b),(c,d),(e,f)(a,b), (c,d), (e,f).

L3suffices
1.2

Associativity of ++: ((a,b)+(c,d))+(e,f)((a,b)+(c,d))+(e,f) and (a,b)+((c,d)+(e,f))(a,b)+((c,d)+(e,f)) both equal (a+c+e,  b+d+f)(a+c+e,\; b+d+f).

L1
1.3

Commutativity of ++: (a+c,b+d)=(c+a,d+b)(a+c,\, b+d) = (c+a,\, d+b).

L1
1.4

Additive identity: (a,b)+(0,0)=(a+0,b+0)=(a,b)(a,b) + (0,0) = (a+0,\, b+0) = (a,b).

L1
1.5

Additive inverses: (a,b)+(b,a)=(a+b,b+a)(0,0)(a,b) + (b,a) = (a+b,\, b+a) \sim (0,0), since (a+b)+0=(b+a)+0(a+b) + 0 = (b+a) + 0.

L1
1.6

Commutativity of \cdot: swapping (a,b)(c,d)(a,b) \leftrightarrow (c,d) sends (ac+bd,ad+bc)(ac+bd,\, ad+bc) to (ca+db,cb+da)(ca+db,\, cb+da), the same pair.

L1L2
1.7

Multiplicative identity: (a,b)(1,0)=(a1+b0,  a0+b1)=(a,b)(a,b) \cdot (1,0) = (a \cdot 1 + b \cdot 0,\; a \cdot 0 + b \cdot 1) = (a,b).

L1L2
1.8

Associativity of \cdot: expanding, both ((a,b)(c,d))(e,f)((a,b)(c,d))(e,f) and (a,b)((c,d)(e,f))(a,b)((c,d)(e,f)) equal (ace+adf+bcf+bde,  acf+ade+bce+bdf)(ace+adf+bcf+bde,\; acf+ade+bce+bdf).

L1L2
1.9

Distributivity: (a,b)((c,d)+(e,f))=(a(c+e)+b(d+f),  a(d+f)+b(c+e))=(ac+bd,ad+bc)+(ae+bf,af+be)=(a,b)(c,d)+(a,b)(e,f)(a,b) \cdot ((c,d)+(e,f)) = (a(c+e)+b(d+f),\; a(d+f)+b(c+e)) = (ac+bd,\, ad+bc) + (ae+bf,\, af+be) = (a,b)(c,d) + (a,b)(e,f).

L1L2
2.1

Steps 1.2–1.9 verify all axioms: (Z,+,,0,1)(\mathbb{Z}, +, \cdot, 0, 1) is a commutative ring with identity and additive inverses.

step 1.1step 1.2step 1.3step 1.4step 1.5step 1.6step 1.7step 1.8step 1.9
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-24Open item page →

Order on the integers

Definition

For integers x=[(a,b)]x = [(a,b)] and y=[(c,d)]y = [(c,d)] (The integers as equivalence classes of pairs of naturals) define

xy    a+db+cin N.x \le y \iff a + d \le b + c \quad \text{in } \mathbb{N}.

Write x<yx < y when xyx \le y and xyx \ne y. An integer xx is positive when 0<x0 < x; on representatives, 0<[(a,b)]0 < [(a,b)] exactly when b<ab < a.

Remarks

  • The defining inequality is "abcda - b \le c - d" restated without subtraction.
  • Well-definedness, totality, and compatibility with the arithmetic are proved in The integers form a totally ordered ring .
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

The integers form a totally ordered ring

Statement

The relation of Order on the integers is well defined and is a total order on Z\mathbb{Z}; it is compatible with addition (xyx \le y implies x+zy+zx + z \le y + z) and positives are closed under multiplication (0<x0 < x and 0<y0 < y imply 0<xy0 < xy). Thus Z\mathbb{Z} is a totally ordered commutative ring.

Facts & Assumptions

Given: Integers x=[(a,b)]x = [(a,b)], y=[(c,d)]y = [(c,d)], z=[(e,f)]z = [(e,f)] with the operations of Arithmetic on the integers.

[L1]

Addition on N\mathbb{N} is commutative and associative (Addition is commutative, Addition is associative).

[L2]

The order on N\mathbb{N} is total, antisymmetric, and transitive (\le is a linear order on N\mathbb{N}).

[L3]

Natural order is translation-invariant: xy    x+zy+zx\le y\iff x+z\le y+z (Order is compatible with addition).

[L4]

By the definition of natural order, xyx\le y exactly when y=x+ky=x+k for some natural kk; if x<yx<y, such a gap is nonzero (Order on the natural numbers).

[L5]

Natural multiplication is commutative and associative, distributes over addition, and has the usual zero and identity laws; multiplication by a nonzero natural preserves strict order (Multiplication is commutative, Multiplication is associative, Distributivity and the successor law for multiplication, Zero and one under multiplication, Order is compatible with multiplication).

[L6]

The integer operations make Z\mathbb{Z} a commutative ring with multiplicative identity (The integers form a commutative ring).

Proof

technique · direct
1.1

Suppose (a,b)(a,b)(a,b) \sim (a',b') and (c,d)(c,d)(c,d) \sim (c',d'), i.e. a+b=b+aa + b' = b + a' and c+d=d+cc + d' = d + c'.

given
1.2

Suppose a+db+ca + d \le b + c.

given
1.3

Totality: in N\mathbb{N} either a+db+ca + d \le b + c or b+ca+db + c \le a + d, so xyx \le y or yxy \le x.

L2
1.4

Antisymmetry: xyx \le y and yxy \le x give a+db+ca + d \le b + c and b+ca+db + c \le a + d, hence a+d=b+ca + d = b + c, which is x=yx = y as classes.

L2
1.5

Transitivity: from a+db+ca + d \le b + c and c+fd+ec + f \le d + e, adding gives (a+d)+(c+f)(b+c)+(d+e)(a+d)+(c+f) \le (b+c)+(d+e); regrouping, (a+f)+(c+d)(b+e)+(c+d)(a+f)+(c+d) \le (b+e)+(c+d); cancelling, a+fb+ea + f \le b + e, i.e. xzx \le z.

L1L2L3
1.6

Compatibility with addition: x+zy+zx + z \le y + z reads (a+e)+(d+f)(b+f)+(c+e)(a+e)+(d+f) \le (b+f)+(c+e), which regroups to (a+d)+(e+f)(b+c)+(e+f)(a+d) + (e+f) \le (b+c) + (e+f), equivalent to a+db+ca + d \le b + c, i.e. xyx \le y.

L1L3
1.7

Suppose 0<x0 < x and 0<y0 < y, i.e. b<ab < a and d<cd < c.

given
2.1

Adding (a+d)(a'+d'): (a+d)+(a+d)(b+c)+(a+d)(a+d) + (a'+d') \le (b+c) + (a'+d').

step 1.2L3
2.2

Regrouping with the equations of step 1.1: (b+c)+(a+d)=(b+a)+(c+d)=(a+b)+(d+c)=(a+d)+(b+c)(b+c) + (a'+d') = (b+a') + (c+d') = (a+b') + (d+c') = (a+d) + (b'+c').

step 1.1L1
2.3

Write a=b+ka = b + k and c=d+mc = d + m with nonzero naturals k,mk,m.

step 1.7L4
3.1

So (a+d)+(a+d)(a+d)+(b+c)(a+d) + (a'+d') \le (a+d) + (b'+c'); cancelling (a+d)(a+d) gives a+db+ca'+d'\le b'+c'. Applying the same argument with primed and unprimed representatives exchanged proves the converse implication, so the relation is independent of representatives.

step 1.1step 2.1step 2.2L3
3.2

Expanding both components of xy=[(ac+bd,ad+bc)]xy = [(ac+bd,\, ad+bc)]: ac+bd=(b+k)(d+m)+bd=(bd+bm+kd+bd)+kmac + bd = (b+k)(d+m) + bd = (bd + bm + kd + bd) + km and ad+bc=(b+k)d+b(d+m)=bd+kd+bd+bmad + bc = (b+k)d + b(d+m) = bd + kd + bd + bm, so ac+bd=(ad+bc)+kmac + bd = (ad + bc) + km.

step 2.3L1L5
4.1

Since k,mk,m are nonzero, 0<k0<k and 0<m0<m by [L4]. Hence [L5] gives 0=0m<km0=0\cdot m<km, and step 3.2 yields ad+bc<ac+bdad+bc<ac+bd, which is 0<xy0<xy.

step 2.3step 3.2L2L4L5
5.1

The order is well defined, total, compatible with addition, and positives are closed under multiplication; together with [L6], this makes Z\mathbb{Z} a totally ordered commutative ring.

step 3.1step 1.3step 1.4step 1.5step 1.6step 4.1L6
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The integers have no zero divisors; multiplicative cancellation

Statement

If x,yZx, y \in \mathbb{Z} are nonzero then xy0xy \ne 0. Consequently, if xz=yzxz = yz and z0z \ne 0, then x=yx = y.

Facts & Assumptions

Given: Nonzero integers x,yx, y.

[L1]

Z\mathbb{Z} is a totally ordered ring; in particular trichotomy holds (each integer is negative, zero, or positive) and positives are closed under multiplication (The integers form a totally ordered ring).

[L2]

Ring arithmetic in Z\mathbb{Z}: (u)v=(uv)(-u)v = -(uv), (u)=u-(-u) = u, and distributivity (The integers form a commutative ring).

Proof

technique · cases
1.1

By trichotomy, each of xx and yy is positive or negative; split on the sign pattern.

L1cases-exhaustive
1.2

Case both positive: 0<xy0 < xy by closure of positives, so xy0xy \ne 0.

assume-case bothL1
1.3

Case exactly one negative, say y<0y < 0 (the other case is identical by commutativity): 0<y0 < -y, so 0<x(y)=(xy)0 < x(-y) = -(xy), hence xy<0xy < 0 and xy0xy \ne 0.

assume-case mixedL1L2
1.4

Case both negative: 0<x0 < -x and 0<y0 < -y, so 0<(x)(y)=xy0 < (-x)(-y) = xy, and xy0xy \ne 0.

assume-case negnegL1L2
2.1

In every case xy0xy \ne 0: the product of nonzero integers is nonzero.

step 1.2step 1.3step 1.4cases
3.1

Cancellation: if xz=yzxz = yz with z0z \ne 0, then (xy)z=xzyz=0(x-y)z = xz - yz = 0; were xy0x - y \ne 0, the product would be nonzero, so xy=0x - y = 0, i.e. x=yx = y.

step 2.1L2
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The naturals embed in the integers

Statement

The map ι(n)=[(n,0)]\iota(n) = [(n,0)] is injective and preserves addition, multiplication, and order. Its image is exactly the set of nonnegative integers, so every x0x \ge 0 in Z\mathbb{Z} is ι(k)\iota(k) for a unique natural kk.

Facts & Assumptions

Given: The map ι:NZ\iota : \mathbb{N} \to \mathbb{Z}, ι(n)=[(n,0)]\iota(n) = [(n,0)].

[A1]

Arithmetic identities in N\mathbb{N}: x+0=xx + 0 = x, 0+x=x0 + x = x, x0=0x \cdot 0 = 0, 0x=00 \cdot x = 0, x1=xx \cdot 1 = x.

[A2]

The order on N\mathbb{N}, and: xyx \le y iff y=x+ky = x + k for some kk.

Proof

technique · direct
1.1

Injectivity: [(m,0)]=[(n,0)][(m,0)] = [(n,0)] means m+0=0+nm + 0 = 0 + n, i.e. m=nm = n.

A1
1.2

Addition: ι(m)+ι(n)=[(m+n,0+0)]=ι(m+n)\iota(m) + \iota(n) = [(m+n,\, 0+0)] = \iota(m+n).

A1
1.3

Multiplication: ι(m)ι(n)=[(mn+00,  m0+0n)]=ι(mn)\iota(m)\,\iota(n) = [(mn + 0 \cdot 0,\; m \cdot 0 + 0 \cdot n)] = \iota(mn).

A1
1.4

Order: ι(m)ι(n)\iota(m) \le \iota(n) reads m+00+nm + 0 \le 0 + n, i.e. mnm \le n.

A1A2
1.5

Image: if 0[(a,b)]0 \le [(a,b)] then bab \le a, so a=b+ka = b + k and (a,b)(k,0)(a,b) \sim (k,0), giving [(a,b)]=ι(k)[(a,b)] = \iota(k); conversely 0ι(k)0 \le \iota(k) for every kk.

A2algebra
2.1

ι\iota embeds N\mathbb{N} into Z\mathbb{Z}, preserving arithmetic and order, with image the nonnegative integers.

step 1.1step 1.2step 1.3step 1.4step 1.5
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-24Open item page →

The rationals as equivalence classes of pairs of integers

Definition

On the set of pairs (a,b)(a,b) with a,bZa, b \in \mathbb{Z} and b0b \ne 0, define

(a,b)(c,d)    ad=cbin Z.(a,b) \sim (c,d) \iff ad = cb \quad \text{in } \mathbb{Z}.

This is an equivalence relation (The rational-defining relation is an equivalence relation ). The rationals are the quotient Q\mathbb{Q}, and [(a,b)][(a,b)] is written a/ba/b.

Remarks

  • The pair (a,b)(a,b) encodes the formal quotient a/ba/b; the relation ad=cbad = cb is "a/b=c/da/b = c/d" cleared of denominators, using only the ring arithmetic of Z\mathbb{Z} (The integers form a commutative ring).
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The rational-defining relation is an equivalence relation

Statement

The relation (a,b)(c,d)    ad=cb(a,b) \sim (c,d) \iff ad = cb on pairs of integers with nonzero second component (The rationals as equivalence classes of pairs of integers) is an equivalence relation.

Facts & Assumptions

Given: Pairs (a,b),(c,d),(e,f)(a,b), (c,d), (e,f) of integers with b,d,f0b, d, f \ne 0.

[L1]

Z\mathbb{Z} is a commutative ring (The integers form a commutative ring).

[L2]

Multiplicative cancellation in Z\mathbb{Z}: ud=vdud = vd with d0d \ne 0 implies u=vu = v (The integers have no zero divisors; multiplicative cancellation).

Proof

technique · direct
1.1

Reflexivity: ab=baab = ba, so (a,b)(a,b)(a,b) \sim (a,b).

L1
1.2

Symmetry: if ad=cbad = cb then cb=adcb = ad, which is the defining equation for (c,d)(a,b)(c,d) \sim (a,b).

L1
1.3

Suppose (a,b)(c,d)(a,b) \sim (c,d) and (c,d)(e,f)(c,d) \sim (e,f), i.e. ad=cbad = cb and cf=edcf = ed.

given
2.1

Multiplying the first equation by ff and the second by bb: adf=cbfadf = cbf and cfb=edbcfb = edb.

step 1.3L1
3.1

Chaining: (af)d=adf=cbf=cfb=edb=(eb)d(af)d = adf = cbf = cfb = edb = (eb)d.

step 2.1L1
4.1

Cancelling the nonzero dd: af=ebaf = eb, so (a,b)(e,f)(a,b) \sim (e,f); the relation is transitive.

step 3.1L2
5.1

The relation is reflexive, symmetric, and transitive, hence an equivalence relation.

step 1.1step 1.2step 4.1
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-24Open item page →

Arithmetic on the rationals

Definition

On Q\mathbb{Q} (The rationals as equivalence classes of pairs of integers) define, on representatives,

[(a,b)]+[(c,d)]:=[(ad+cb,  bd)],[(a,b)][(c,d)]:=[(ac,  bd)],[(a,b)] + [(c,d)] := [(ad + cb,\; bd)], \qquad [(a,b)] \cdot [(c,d)] := [(ac,\; bd)], [(a,b)]:=[(a,b)],0:=[(0,1)],1:=[(1,1)],-[(a,b)] := [(-a, b)], \qquad 0 := [(0,1)], \qquad 1 := [(1,1)],

and, for [(a,b)]0[(a,b)] \ne 0 (equivalently a0a \ne 0), the inverse [(a,b)]1:=[(b,a)][(a,b)]^{-1} := [(b,a)].

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

Rational arithmetic is well defined

Statement

Sum, product, and negation of Arithmetic on the rationals are independent of the chosen representatives.

Facts & Assumptions

Given: Pairs with (a,b)(a,b)(a,b) \sim (a',b') and (c,d)(c,d)(c,d) \sim (c',d') (The rationals as equivalence classes of pairs of integers), all second components nonzero.

[L1]

Z\mathbb{Z} is a commutative ring (The integers form a commutative ring).

Proof

technique · direct
1.1

By hypothesis ab=abab' = a'b and cd=cdcd' = c'd.

given
2.1

Product: (ac)(bd)=(ab)(cd)=(ab)(cd)=(ac)(bd)(ac)(b'd') = (ab')(cd') = (a'b)(c'd) = (a'c')(bd), so (ac,bd)(ac,bd)(ac,\, bd) \sim (a'c',\, b'd').

step 1.1L1
2.2

Sum: (ad+cb)(bd)=(ab)(dd)+(cd)(bb)=(ab)(dd)+(cd)(bb)=(ad+cb)(bd)(ad + cb)(b'd') = (ab')(dd') + (cd')(bb') = (a'b)(dd') + (c'd)(bb') = (a'd' + c'b')(bd), so (ad+cb,bd)(ad+cb,bd)(ad+cb,\, bd) \sim (a'd'+c'b',\, b'd').

step 1.1L1
2.3

Negation: from ab=abab' = a'b, (a)b=(a)b(-a)b' = (-a')b, so (a,b)(a,b)(-a, b) \sim (-a', b').

step 1.1L1
3.1

All three operations are independent of representatives.

step 2.1step 2.2step 2.3
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

The reciprocal on the rationals is well-defined

Statement

On Q{0}\mathbb{Q} \setminus \{0\} the reciprocal [(a,b)]1:=[(b,a)][(a,b)]^{-1} := [(b,a)] (Arithmetic on the rationals) is independent of the chosen representative: if (a,b)(a,b)(a,b) \sim (a',b') with a,a,b,b0a, a', b, b' \ne 0, then (b,a)(b,a)(b,a) \sim (b',a'). Hence the reciprocal is a well-defined function on Q{0}\mathbb{Q} \setminus \{0\}.

Facts & Assumptions

Given: Nonzero rationals represented by integer pairs (a,b)(a,b) and (a,b)(a',b') with a,a,b,b0a, a', b, b' \ne 0, where (x,y)(z,w)    xw=zy(x,y) \sim (z,w) \iff x w = z y in Z\mathbb{Z} (The rationals as equivalence classes of pairs of integers).

[L1]

Multiplication in Z\mathbb{Z} is commutative (The integers form a commutative ring).

Proof

technique · direct
1.1

By hypothesis (a,b)(a,b)(a,b) \sim (a',b'), that is ab=aba b' = a' b in Z\mathbb{Z}.

given
2.1

Commuting each product by [L1], ba=bab' a = b a', hence ba=bab a' = b' a.

step 1.1L1
3.1

The equation ba=bab a' = b' a is exactly the defining relation (b,a)(b,a)(b,a) \sim (b',a'), and since a,a0a, a' \ne 0 the pairs (b,a),(b,a)(b,a), (b',a') are legal rational representatives; therefore [(a,b)]1=[(b,a)]=[(b,a)]=[(a,b)]1[(a,b)]^{-1} = [(b,a)] = [(b',a')] = [(a',b')]^{-1}, so the reciprocal is well-defined on Q{0}\mathbb{Q} \setminus \{0\}.

step 2.1given
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The rationals form a field

Statement

(Q,+,,0,1)(\mathbb{Q}, +, \cdot, 0, 1) with the operations of Arithmetic on the rationals is a field: a commutative ring with 101 \ne 0 in which every nonzero element has a multiplicative inverse.

Facts & Assumptions

Given: Rationals with representatives (a,b),(c,d),(e,f)(a,b), (c,d), (e,f), second components nonzero.

[L1]

The operations are independent of representatives (Rational arithmetic is well defined).

[L2]

Z\mathbb{Z} is a commutative ring in which 101 \ne 0 (The integers form a commutative ring; 101 \ne 0 because 101 \ne 0 in N\mathbb{N}).

[L3]

Z\mathbb{Z} has no zero divisors and admits cancellation (The integers have no zero divisors; multiplicative cancellation).

Proof

technique · direct
1.1

By [L1], each axiom may be verified on fixed representatives.

L1suffices
1.2

Associativity of ++: both ((a,b)+(c,d))+(e,f)((a,b)+(c,d))+(e,f) and (a,b)+((c,d)+(e,f))(a,b)+((c,d)+(e,f)) have representative (adf+cbf+ebd,  bdf)(adf + cbf + ebd,\; bdf).

L2
1.3

Commutativity of ++: (ad+cb,bd)(ad+cb,\, bd) and (cb+ad,db)(cb+ad,\, db) are equal pairs.

L2
1.4

Additive identity: (a,b)+(0,1)=(a1+0b,  b1)=(a,b)(a,b) + (0,1) = (a \cdot 1 + 0 \cdot b,\; b \cdot 1) = (a,b).

L2
1.5

Additive inverses: (a,b)+(a,b)=(abab,  b2)=(0,b2)(0,1)(a,b) + (-a,b) = (ab - ab,\; b^2) = (0, b^2) \sim (0,1).

L2
1.6

Associativity and commutativity of \cdot: ((ac)e,(bd)f)=(a(ce),b(df))((ac)e,\, (bd)f) = (a(ce),\, b(df)) and (ac,bd)=(ca,db)(ac,\, bd) = (ca,\, db).

L2
1.7

Multiplicative identity: (a,b)(1,1)=(a,b)(a,b)(1,1) = (a,b); and 101 \ne 0 since 11011 \cdot 1 \ne 0 \cdot 1.

L2
1.8

Distributivity: (a,b)((c,d)+(e,f))(a,b)\bigl((c,d)+(e,f)\bigr) has representative (a(cf+ed),  b(df))(a(cf+ed),\; b(df)), while (a,b)(c,d)+(a,b)(e,f)(a,b)(c,d) + (a,b)(e,f) has representative (acbf+aebd,  b2df)=(b(acf+aed),  b(bdf))(acbf + aebd,\; b^2 df) = (b(acf + aed),\; b(bdf)); cancelling the common nonzero factor bb these are equivalent.

L2L3
1.9

Inverses: [(a,b)]=0[(a,b)] = 0 iff a1=0ba \cdot 1 = 0 \cdot b iff a=0a = 0; for a0a \ne 0, (a,b)(b,a)=(ab,ba)(1,1)(a,b)(b,a) = (ab,\, ba) \sim (1,1).

L2
2.1

All field axioms hold: Q\mathbb{Q} is a field.

step 1.1step 1.2step 1.3step 1.4step 1.5step 1.6step 1.7step 1.8step 1.9
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-24Open item page →

Order on the rationals

Definition

Every rational has a representative with positive denominator (if b<0b < 0 then (a,b)(a,b)(a,b) \sim (-a,-b) with b>0-b > 0, Every rational has a positive-denominator representative ). For representatives with b>0b > 0 and d>0d > 0 define

[(a,b)][(c,d)]    adcbin Z.[(a,b)] \le [(c,d)] \iff ad \le cb \quad \text{in } \mathbb{Z}.

A rational xx is positive when 0<x0 < x; on such representatives, 0<[(a,b)]0 < [(a,b)] exactly when 0<a0 < a.

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Every rational has a positive-denominator representative

Statement

Every rational has a representative (a,b)(a,b) with b>0b > 0: for a class [(a,b)][(a,b)] (where b0b \ne 0), if b>0b > 0 take (a,b)(a,b) itself, and if b<0b < 0 then (a,b)(a,b)(a,b) \sim (-a,-b) with b>0-b > 0. Consequently the order on Q\mathbb{Q} (Order on the rationals), which is stated on positive-denominator representatives, is defined on all of Q\mathbb{Q}.

Facts & Assumptions

Given: A rational represented by (a,b)(a,b) with a,bZa, b \in \mathbb{Z}, b0b \ne 0, and the relation (x,y)(z,w)    xw=zy(x,y) \sim (z,w) \iff x w = z y (The rationals as equivalence classes of pairs of integers).

[L1]

Trichotomy in Z\mathbb{Z}: each nonzero integer is either >0> 0 or <0< 0, and b<0b < 0 iff b>0-b > 0 (The integers form a totally ordered ring).

[L2]

In the commutative ring Z\mathbb{Z}, a(b)=(ab)=(a)ba(-b) = -(ab) = (-a)b (both products are the additive inverse of abab, by distributivity) (The integers form a commutative ring).

Proof

technique · direct
1.1

Since b0b \ne 0, by trichotomy [L1] either b>0b > 0 or b<0b < 0.

givenL1
2.1

If b>0b > 0, the representative (a,b)(a,b) already has positive denominator.

step 1.1
2.2

If b<0b < 0, then b>0-b > 0 by [L1], and a(b)=(a)ba(-b) = (-a)b by [L2] is exactly the defining relation (a,b)(a,b)(a,b) \sim (-a,-b); so (a,b)(-a,-b) represents the same class and has positive denominator b-b.

step 1.1L1L2
3.1

In either case the class has a representative with positive denominator; hence the order Order on the rationals, stated on such representatives, is defined for every rational.

step 2.1step 2.2
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The rationals form a totally ordered field

Statement

The relation of Order on the rationals is well defined and makes the field Q\mathbb{Q} (The rationals form a field) a totally ordered field: the order is total, xyx \le y implies x+zy+zx + z \le y + z, and 0<x0 < x, 0<y0 < y imply 0<xy0 < xy.

Facts & Assumptions

Given: Rationals x=[(a,b)]x = [(a,b)], y=[(c,d)]y = [(c,d)], z=[(e,f)]z = [(e,f)] with b,d,f>0b, d, f > 0.

[L1]

Z\mathbb{Z} is a totally ordered commutative ring; positives are closed under products (The integers form a totally ordered ring).

Proof

technique · direct
1.1

Order-scaling in Z\mathbb{Z}: for p>0p > 0, if u<vu < v then 0<(vu)p0 < (v-u)p, so up<vpup < vp; conversely if upvpup \le vp and v<uv < u then vp<upvp < up, impossible; hence uvu \le v iff upvpup \le vp.

L1algebra
1.2

Suppose (a,b)(a,b)(a,b) \sim (a',b') and (c,d)(c,d)(c,d) \sim (c',d') with b,d>0b', d' > 0, i.e. ab=abab' = a'b and cd=cdcd' = c'd; suppose also adcbad \le cb.

given
1.3

Totality: adcbad \le cb or cbadcb \le ad in Z\mathbb{Z}, so xyx \le y or yxy \le x.

L1
1.4

Antisymmetry: adcbad \le cb and cbadcb \le ad give ad=cbad = cb, i.e. x=yx = y as classes.

L1
1.5

Positive products: if 0<x0 < x and 0<y0 < y then 0<a0 < a and 0<c0 < c, so xy=[(ac,bd)]xy = [(ac,\, bd)] has ac>0ac > 0 and bd>0bd > 0, hence 0<xy0 < xy.

L1
1.6

For transitivity, let z=[(e,f)]z = [(e,f)] with f>0f > 0 and suppose additionally yzy \le z, i.e. cfedcf \le ed.

given
2.1

Scaling the hypothesis adcbad \le cb by bd>0b'd' > 0: (ad)(bd)(cb)(bd)(ad)(b'd') \le (cb)(b'd').

step 1.1step 1.2L1
2.2

Rearranging both sides with ab=abab' = a'b and cd=cdcd' = c'd: (ad)(bd)=(ab)(dd)=(ab)(dd)=(ad)(bd)(ad)(b'd') = (ab')(dd') = (a'b)(dd') = (a'd')(bd) and (cb)(bd)=(cd)(bb)=(cd)(bb)=(cb)(bd)(cb)(b'd') = (cd')(bb') = (c'd)(bb') = (c'b')(bd).

step 1.2L1
2.3

Transitivity: from adcbad \le cb and cfedcf \le ed, scaling by f>0f > 0 and b>0b > 0 gives (af)d=(ad)f(cb)f=(cf)b(ed)b=(eb)d(af)d = (ad)f \le (cb)f = (cf)b \le (ed)b = (eb)d; cancelling d>0d > 0 via order-scaling, afebaf \le eb, i.e. xzx \le z.

step 1.1step 1.2step 1.6L1
2.4

Compatibility with addition: x+zy+zx + z \le y + z reads (af+eb)(df)(cf+ed)(bf)(af+eb)(df) \le (cf+ed)(bf), which expands to (ad)f2+(eb)(df)(cb)f2+(ed)(bf)(ad)f^2 + (eb)(df) \le (cb)f^2 + (ed)(bf); the second terms are equal, so this is (ad)f2(cb)f2(ad)f^2 \le (cb)f^2, equivalent by order-scaling with f2>0f^2 > 0 to adcbad \le cb, i.e. xyx \le y.

step 1.1L1
3.1

Combining: (ad)(bd)(cb)(bd)(a'd')(bd) \le (c'b')(bd) with bd>0bd > 0, so adcba'd' \le c'b' by order-scaling: the order is independent of representatives.

step 2.1step 2.2step 1.1L1
4.1

The order is well defined, total, compatible with addition, and positives are closed under multiplication: Q\mathbb{Q} is a totally ordered field.

step 3.1step 1.3step 1.4step 2.3step 2.4step 1.5
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The integers embed in the rationals

Statement

The map j(k)=[(k,1)]j(k) = [(k,1)] is injective and preserves addition, multiplication, and order. Composing with The naturals embed in the integers embeds N\mathbb{N} in Q\mathbb{Q}; we write kk for j(k)j(k) throughout.

Facts & Assumptions

Given: The map j:ZQj : \mathbb{Z} \to \mathbb{Q}, j(k)=[(k,1)]j(k) = [(k,1)].

[L1]

Ring arithmetic in Z\mathbb{Z} (The integers form a commutative ring).

[L2]

The order on Q\mathbb{Q} (Order on the rationals), whose defining inequality is read in the order on Z\mathbb{Z} (Order on the integers).

[L3]

Equality in Q\mathbb{Q}: [(a,b)]=[(c,d)][(a,b)] = [(c,d)] iff ad=cbad = cb (The rationals as equivalence classes of pairs of integers).

Proof

technique · direct
1.1

Injectivity: (k,1)(m,1)(k,1) \sim (m,1) means k1=m1k \cdot 1 = m \cdot 1, i.e. k=mk = m.

L3L1
1.2

Addition: j(k)+j(m)=[(k1+m1,  1)]=j(k+m)j(k) + j(m) = [(k \cdot 1 + m \cdot 1,\; 1)] = j(k+m).

L1
1.3

Multiplication: j(k)j(m)=[(km,1)]=j(km)j(k)\,j(m) = [(km,\, 1)] = j(km).

L1
1.4

Order: denominators are 1>01 > 0, so j(k)j(m)j(k) \le j(m) reads k1m1k \cdot 1 \le m \cdot 1, i.e. kmk \le m.

L1L2
2.1

jj embeds Z\mathbb{Z} into Q\mathbb{Q}, preserving arithmetic and order.

step 1.1step 1.2step 1.3step 1.4
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The rationals are Archimedean

Statement

For every rational xx there is a natural number nn with x<nx < n. Consequently, for every rational ε>0\varepsilon > 0 there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon.

Facts & Assumptions

Given: A rational x=[(a,b)]x = [(a,b)] with b>0b > 0.

[L1]

The order and arithmetic of Q\mathbb{Q} (The rationals form a totally ordered field).

[L2]

Integer facts: positive integers are exactly ι(m)\iota(m) with m1m \ge 1 natural; nonnegative integers are the image of N\mathbb{N}; the embeddings preserve arithmetic and order (The naturals embed in the integers, The integers embed in the rationals, The integers form a totally ordered ring).

Proof

technique · direct
1.1

Since b>0b > 0, bb lies in the image of N\mathbb{N} and b1b \ge 1.

L2
1.2

If a0a \le 0 set k=0k = 0; otherwise aa is a positive integer, so a=ι(k)a = \iota(k) for some natural k1k \ge 1. In both cases aka \le k (as integers).

L2
2.1

Then a<k+1a < k + 1 and, since b1b \ge 1 and k+1>0k+1 > 0, also k+1(k+1)bk + 1 \le (k+1)b.

step 1.1step 1.2L2
3.1

Hence a<(k+1)ba < (k+1)b, and dividing by b>0b > 0 (order-scaling in the definition of the rational order), x=[(a,b)]<[((k+1)b,b)]=k+1=:nx = [(a,b)] < [( (k+1)b,\, b)] = k+1 =: n.

step 2.1L1
4.1

For rational ε>0\varepsilon > 0: apply the above to x=1/εx = 1/\varepsilon to get nn with 1/ε<n1/\varepsilon < n, hence 1/n<ε1/n < \varepsilon.

step 3.1L1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Dedekind cut

Definition

Work over the totally ordered field Q\mathbb{Q} of rationals (The rationals as equivalence classes of pairs of integers, The rationals form a totally ordered field). A subset AQA \subseteq \mathbb{Q} is a Dedekind cut iff it satisfies all three of:

  • (C1) AA \ne \emptyset and AQA \ne \mathbb{Q} (proper and nonempty);
  • (C2) downward closed: if pAp \in A and q<pq < p, then qAq \in A;
  • (C3) no greatest element: if pAp \in A, then there exists rAr \in A with p<rp < r.

Remarks

This is the lower-set convention (Rudin's): a cut is the set of rationals lying strictly below a real point, so it "opens downward" and never closes off at a maximum. Under the opposite (upper-set) convention the inequalities are reversed; we fix the lower-set form throughout.

An equivalent phrasing of (C2) by contraposition: if qAq \notin A and q<pq < p, then pAp \notin A; the complement QA\mathbb{Q} \setminus A is upward closed. Consequently every aAa \in A and bAb \notin A satisfy a<ba < b: were bab \le a, downward closure (C2) would place bAb \in A. Thus a cut splits Q\mathbb{Q} into a lower piece AA and an upper piece QA\mathbb{Q} \setminus A with every element of the former below every element of the latter, the lower piece having no largest member.

The set of all Dedekind cuts is the carrier of the real numbers (The real numbers R\mathbb{R} as Dedekind cuts); each cut is a real number, identified with the downward gap of rationals it names.

DefinitionDefinition: Literature-sourcedProof: Not applicableverified 2026-08-02 (claude-opus-5)Open item page →

The real numbers R\mathbb{R} as Dedekind cuts

Definition

The real numbers are defined to be the set of all Dedekind cuts of Q\mathbb{Q} (Dedekind cut): R:={AQ:A is a Dedekind cut}.\mathbb{R} := \{\, A \subseteq \mathbb{Q} : A \text{ is a Dedekind cut} \,\}. Elements of R\mathbb{R} are written A,B,C,A, B, C, \dots; each is a subset of Q\mathbb{Q} satisfying (C1)–(C3).

The rationals embed into R\mathbb{R} by the rational embedding: for qQq \in \mathbb{Q} set q:={rQ:r<q},q^{*} := \{\, r \in \mathbb{Q} : r < q \,\}, the cut of all rationals strictly below qq. Each qq^{*} is a Dedekind cut (Each rational cut qq^{*} is a Dedekind cut ), and qqq \mapsto q^{*} sends Q\mathbb{Q} into R\mathbb{R}. The images of 00 and 11 are written 00^{*} and 11^{*}; being cuts they lie in R\mathbb{R} and serve as its additive and multiplicative identities.

Remarks

A cut AA is exactly the set of rationals lying below a putative real point; R\mathbb{R} is thus built by naming each point through the downward gap of rationals it determines. Where Q\mathbb{Q} has a genuine rational point qq, the cut qq^{*} recovers it, but the construction also admits cuts AA with no largest excluded rational and no rational boundary at all, such as {q:q<0 or q2<2}\{\, q : q < 0 \text{ or } q^{2} < 2 \,\}. These are precisely the missing limits of Q\mathbb{Q}: the cut convention manufactures a real number wherever Q\mathbb{Q} leaves a hole, which is why R\mathbb{R} is complete while Q\mathbb{Q} is not.

The order on R\mathbb{R} is set inclusion, AB:ABA \le B :\Leftrightarrow A \subseteq B (Order on the Dedekind reals). That qqq \mapsto q^{*} is an order-preserving ring embedding, and that its image is dense, is recorded in The rational cuts embed densely in R\mathbb{R}, preserving sums, products, 00, 11 and the order; the arithmetic and order structure making R\mathbb{R} a complete ordered field is developed in The Dedekind reals form a totally ordered field and Dedekind completeness: the least-upper-bound property.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Each rational cut qq^{*} is a Dedekind cut

Statement

For every qQq \in \mathbb{Q} the set q={rQ:r<q}q^{*} = \{\, r \in \mathbb{Q} : r < q \,\} (The real numbers R\mathbb{R} as Dedekind cuts) is a Dedekind cut (Dedekind cut). In particular 00^{*} and 11^{*} are Dedekind cuts, hence elements of R\mathbb{R}, so they are legitimate as the additive and multiplicative identities of R\mathbb{R}.

Facts & Assumptions

Given: A rational qq and the set q={rQ:r<q}q^{*} = \{\, r \in \mathbb{Q} : r < q \,\}, with the Dedekind-cut axioms (C1) proper and nonempty, (C2) downward closed, (C3) no greatest element (Dedekind cut).

[L1]

Q\mathbb{Q} is a totally ordered field: << is transitive and total, q1<q<q+1q - 1 < q < q + 1, and whenever p<qp < q the midpoint p+q2\tfrac{p+q}{2} satisfies p<p+q2<qp < \tfrac{p+q}{2} < q (The rationals form a totally ordered field).

Proof

technique · direct
1.1

(C1) qq^{*} is nonempty and proper: q1<qq - 1 < q gives q1qq - 1 \in q^{*}, while qqq \not< q gives qqq \notin q^{*}, so qq^{*} \ne \emptyset and qQq^{*} \ne \mathbb{Q}.

givenL1
1.2

(C2) qq^{*} is downward closed: if pqp \in q^{*}, so p<qp < q, and r<pr < p, then r<qr < q by transitivity, hence rqr \in q^{*}.

givenL1
1.3

(C3) qq^{*} has no greatest element: if pqp \in q^{*} then p<qp < q, so the midpoint m=p+q2m = \tfrac{p+q}{2} satisfies p<m<qp < m < q, giving mqm \in q^{*} with m>pm > p.

givenL1
2.1

Satisfying (C1), (C2), (C3), qq^{*} is a Dedekind cut; applied at q=0q = 0 and q=1q = 1 this shows 00^{*} and 11^{*} are Dedekind cuts and hence elements of R\mathbb{R}.

step 1.1step 1.2step 1.3
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Order on the Dedekind reals

Definition

For Dedekind cuts A,BRA, B \in \mathbb{R} (Dedekind cut, The real numbers R\mathbb{R} as Dedekind cuts), the order is set inclusion:

AB    AB,A<B    AB.A \le B \iff A \subseteq B, \qquad A < B \iff A \subsetneq B.

That is, A<BA < B means ABA \subseteq B and ABA \ne B.

A cut AA is called positive iff 0<A0^{*} < A, and nonnegative iff 0A0^{*} \le A, where 0={rQ:r<0}0^{*} = \{\, r \in \mathbb{Q} : r < 0 \,\} is the cut of 00. Negative and nonpositive cuts are defined symmetrically: A<0A < 0^{*} and A0A \le 0^{*}.

Remarks

Positivity has a convenient rational restatement: 0A0^{*} \le A iff every rational r<0r < 0 lies in AA, and 0<A0^{*} < A iff moreover 0A0 \in A. Indeed if 0A0 \in A then downward closure (C2) forces every r<0r < 0 into AA, so 0A0^{*} \subseteq A and the inclusion is proper; conversely 0A0^{*} \subsetneq A supplies some qAq \in A with q0q \ge 0, whence 0A0 \in A by (C2). Thus a cut is positive exactly when it contains 00.

Inclusion is manifestly reflexive, antisymmetric, and transitive; what is not immediate is that it is total (any two cuts are comparable), which is Inclusion totally orders the Dedekind reals. Compatibility of this order with the field operations (translation invariance of \le and closure of nonnegatives under products), making R\mathbb{R} a totally ordered field, is The Dedekind reals form a totally ordered field.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

Inclusion totally orders the Dedekind reals

Statement

Set inclusion totally orders the Dedekind reals (Order on the Dedekind reals): the relation AB:ABA \le B :\Leftrightarrow A \subseteq B on cuts (Dedekind cut) is reflexive, antisymmetric (with antisymmetry delivering set equality A=BA = B), and transitive, and it is moreover total: for any two cuts A,BA, B, either ABA \subseteq B or BAB \subseteq A.

Facts & Assumptions

Given: Dedekind cuts A,BRA, B \in \mathbb{R}, ordered by inclusion (Order on the Dedekind reals).

[A1]

Set inclusion \subseteq is a partial order on any family of sets: reflexive (AAA \subseteq A), antisymmetric (mutual inclusion ABA \subseteq B, BAB \subseteq A gives A=BA = B), and transitive.

[A2]

The order on Q\mathbb{Q} is total (The rationals form a totally ordered field): for rationals x,yx, y exactly one of x<yx < y, x=yx = y, y<xy < x holds.

[L1]

Downward closure (C2): if pAp \in A and q<pq < p then qAq \in A, and likewise for BB (Dedekind cut).

Proof

technique · direct
1.1

The relation \le is set inclusion, and \subseteq is reflexive, antisymmetric (mutual inclusion ABA \subseteq B and BAB \subseteq A forces the set equality A=BA = B), and transitive; hence \le is a partial order on R\mathbb{R}.

A1
1.2

It remains to establish totality. Fix cuts A,BA, B; if ABA \subseteq B there is nothing to prove, so assume A⊈BA \not\subseteq B. It suffices to show BAB \subseteq A.

suffices: B ⊆ A when A ⊄ B
2.1

Since A⊈BA \not\subseteq B, choose a rational xx with xAx \in A and xBx \notin B.

step 1.2choose
3.1

Every yBy \in B satisfies y<xy < x: otherwise xyx \le y by trichotomy, and then downward closure of BB places xBx \in B (directly if x<yx < y, or as x=yBx = y \in B), contradicting xBx \notin B.

step 2.1L1A2
4.1

Fix any yBy \in B. From y<xy < x together with xAx \in A, downward closure of AA gives yAy \in A; as yBy \in B was arbitrary, BAB \subseteq A.

step 2.1step 3.1L1
5.1

Thus for all cuts A,BA, B, ABA \subseteq B or BAB \subseteq A, so \le is total; combined with the partial-order properties, set inclusion is a total order on R\mathbb{R}.

step 1.1step 1.2step 4.1
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Addition, negation, and subtraction of Dedekind cuts

Definition

Let A,BRA, B \in \mathbb{R} be Dedekind cuts of Q\mathbb{Q} (Dedekind cut, The real numbers R\mathbb{R} as Dedekind cuts).

Sum. The sum is the Minkowski sumset in Q\mathbb{Q}: A+B:={a+b:aA, bB}.A + B := \{\, a + b : a \in A,\ b \in B \,\}.

Additive identity. 0:={qQ:q<0}0^{*} := \{\, q \in \mathbb{Q} : q < 0 \,\}, the cut of the rational 00 under the embedding qq={rQ:r<q}q \mapsto q^{*} = \{\, r \in \mathbb{Q} : r < q \,\} (The real numbers R\mathbb{R} as Dedekind cuts).

Additive inverse. For a cut AA, A:={pQ:rQ, r>0, with prA}.-A := \{\, p \in \mathbb{Q} : \exists\, r \in \mathbb{Q},\ r > 0,\ \text{with } -p - r \notin A \,\}. Equivalently, pAp \in -A iff there is a rational sAs \notin A with s<ps < -p (set s=prs = -p - r; conversely r=ps>0r = -p - s > 0). Intuitively p-p is bounded away from AA from below: some rational strictly beneath p-p already fails to lie in AA.

Subtraction. AB:=A+(B)A - B := A + (-B).

Remarks

The sum A+BA + B is again a cut, and (R,+)(\mathbb{R}, +) is an abelian group with identity 00^{*}: closure, commutativity, associativity, and the identity law are Cut addition: A+BA+B is a cut, commutative and associative, with identity 00^{*}, and existence of inverses is For a cut AA, A-A is a cut and A+(A)=0A + (-A) = 0^{*}.

The r>0r > 0 slack in the definition of A-A is essential and is not cosmetic. Neither {a:aA}\{-a : a \in A\} nor {a:aA}\{-a : a \notin A\} is a cut in general: the first need not be downward closed, and the second can acquire a greatest element. Excising the boundary rational (the "pr-p - r with r>0r > 0" clause) makes A-A a genuine cut with no greatest element and forces the exact identity A+(A)=0A + (-A) = 0^{*}, not merely A+(A)0A + (-A) \subsetneq 0^{*} (For a cut AA, A-A is a cut and A+(A)=0A + (-A) = 0^{*}).

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Cut addition: A+BA+B is a cut, commutative and associative, with identity 00^{*}

Statement

For Dedekind cuts A,BA, B, the sumset A+B={a+b:aA, bB}A + B = \{\, a + b : a \in A,\ b \in B \,\} (Addition, negation, and subtraction of Dedekind cuts) is again a Dedekind cut. Addition of cuts is commutative and associative, and 0={qQ:q<0}0^{*} = \{\, q \in \mathbb{Q} : q < 0 \,\} is a two-sided identity: A+0=AA + 0^{*} = A for every cut AA.

Facts & Assumptions

Given: Dedekind cuts A,B,CA, B, C; A+B:={a+b:aA, bB}A + B := \{\, a + b : a \in A,\ b \in B \,\} and 0:={qQ:q<0}0^{*} := \{\, q \in \mathbb{Q} : q < 0 \,\} (Addition, negation, and subtraction of Dedekind cuts).

[A1]

Cut axioms (C1)–(C3), and the restatement that for aAa \in A and bAb \notin A one has a<ba < b; the contrapositive of (C2): if xAx \notin A and y>xy > x then yAy \notin A (Dedekind cut).

[L1]

Q\mathbb{Q} is a commutative, associative, totally ordered field; in particular addition is commutative and associative and the order is translation-invariant (The rationals form a totally ordered field).

Proof

technique · direct
1.1

(C1) A+BA + B is proper and nonempty: choosing aAa \in A, bBb \in B gives a+bA+Ba + b \in A + B, so A+BA + B \neq \varnothing; choosing aAa' \notin A, bBb' \notin B, every aAa \in A, bBb \in B satisfies a<aa < a' and b<bb < b', hence a+b<a+ba + b < a' + b', so a+bA+Ba' + b' \notin A + B and A+BQA + B \neq \mathbb{Q}.

A1L1
1.2

(C2) A+BA + B is downward closed: if s=a+bA+Bs = a + b \in A + B with aAa \in A, bBb \in B, and q<sq < s, then qa<bq - a < b, so qaBq - a \in B by (C2) for BB; hence q=a+(qa)A+Bq = a + (q - a) \in A + B.

A1L1
1.3

(C3) A+BA + B has no greatest element: given s=a+bA+Bs = a + b \in A + B, (C3) for AA yields aAa' \in A with a>aa' > a, whence a+bA+Ba' + b \in A + B and a+b>a+b=sa' + b > a + b = s.

A1L1
1.4

Commutativity and associativity descend from Q\mathbb{Q}: A+B={a+b}={b+a}=B+AA + B = \{a + b\} = \{b + a\} = B + A, and (A+B)+C={(a+b)+c}={a+(b+c)}=A+(B+C)(A + B) + C = \{(a + b) + c\} = \{a + (b + c)\} = A + (B + C).

L1
1.5

A+0AA + 0^{*} \subseteq A: for aAa \in A and q0q \in 0^{*} (so q<0q < 0), a+q<aa + q < a, hence a+qAa + q \in A by (C2).

A1L1
1.6

AA+0A \subseteq A + 0^{*}: given aAa \in A, (C3) supplies rAr \in A with r>ar > a; then ar<0a - r < 0, so ar0a - r \in 0^{*}, and a=r+(ar)A+0a = r + (a - r) \in A + 0^{*}.

A1L1
2.1

A+BA + B satisfies (C1)–(C3), so it is a Dedekind cut.

step 1.1step 1.2step 1.3A1
2.2

The two inclusions give the identity law A+0=AA + 0^{*} = A.

step 1.5step 1.6
3.1

Hence A+BA + B is a cut, and cut addition is commutative and associative with two-sided identity 00^{*}.

step 2.1step 1.4step 2.2
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

For a cut AA, A-A is a cut and A+(A)=0A + (-A) = 0^{*}

Statement

For every Dedekind cut AA, the set A={pQ:rQ, r>0, prA}-A = \{\, p \in \mathbb{Q} : \exists\, r \in \mathbb{Q},\ r > 0,\ -p - r \notin A \,\} (Addition, negation, and subtraction of Dedekind cuts) is again a Dedekind cut, and A+(A)=0A + (-A) = 0^{*}, where 0={qQ:q<0}0^{*} = \{\, q \in \mathbb{Q} : q < 0 \,\}. Thus every cut has an additive inverse and (R,+)(\mathbb{R}, +) is a group.

Facts & Assumptions

Given: A Dedekind cut AA; A:={pQ:r>0, prA}-A := \{\, p \in \mathbb{Q} : \exists\, r > 0,\ -p - r \notin A \,\},  A+(A):={a+p:aA, pA}\ A + (-A) := \{\, a + p : a \in A,\ p \in -A \,\}, and 0:={qQ:q<0}0^{*} := \{\, q \in \mathbb{Q} : q < 0 \,\} (Addition, negation, and subtraction of Dedekind cuts).

[A1]

Cut axioms (C1)–(C3), and the restatement that for aAa \in A and bAb \notin A one has a<ba < b; the contrapositive of (C2): if xAx \notin A and y>xy > x then yAy \notin A (Dedekind cut).

[A2]

A nonempty set KZK \subseteq \mathbb{Z} with k<Mk < M for every kKk \in K, where MZM \in \mathbb{Z}, has a greatest element: {Mk:kK}\{\, M - k : k \in K \,\} is then a nonempty set of positive integers, so it has a least element MnM - n by "every nonempty subset SNS \subseteq \mathbb{N} has a least element" (The well-ordering principle), and that nn is the greatest element of KK.

[L1]

Q\mathbb{Q} is Archimedean: for every rational xx there is a natural number nn with x<nx < n (The rationals are Archimedean).

[L2]

Q\mathbb{Q} is a totally ordered field; addition, negation, and scaling by positive rationals respect the order (The rationals form a totally ordered field).

[L3]

If AA and A-A are cuts then A+(A)A + (-A) is a cut (Cut addition: A+BA+B is a cut, commutative and associative, with identity 00^{*}).

Proof

technique · direct
1.1

(C1, nonempty) AQA \neq \mathbb{Q}, so pick sAs \notin A; then p0:=s1p_{0} := -s - 1 satisfies p01=sA-p_{0} - 1 = s \notin A with witness r=1>0r = 1 > 0, so p0Ap_{0} \in -A and A-A \neq \varnothing.

A1choose
1.2

(C1, proper) AA \neq \varnothing, so pick aAa \in A; then aA-a \notin -A, for if aA-a \in -A there were r>0r > 0 with ar=(a)rAa - r = -(-a) - r \notin A, yet ar<aAa - r < a \in A forces arAa - r \in A by (C2), a contradiction. Hence AQ-A \neq \mathbb{Q}.

A1L2
1.3

(C2, downward closed) If pAp \in -A with witness r>0r > 0 (so prA-p - r \notin A) and q<pq < p, then qr>pr-q - r > -p - r, so qrA-q - r \notin A by the contrapositive of (C2); thus qAq \in -A with the same rr.

A1L2
1.4

(C3, no greatest) If pAp \in -A with witness r>0r > 0, set t:=p+r/2>pt := p + r/2 > p; then tr/2=prA-t - r/2 = -p - r \notin A, so tAt \in -A with witness r/2>0r/2 > 0, and t>pt > p.

A1L2
1.5

(A+(A)0A + (-A) \subseteq 0^{*}) For aAa \in A and pAp \in -A with witness r>0r > 0: since prA-p - r \notin A while aAa \in A, the restatement gives a<pra < -p - r, so a+p<r<0a + p < -r < 0; hence a+p0a + p \in 0^{*}.

A1L2
1.6

(setup) Fix v0v \in 0^{*} and put w:=v/2w := -v/2, so w>0w > 0 since v<0v < 0; by (C1) choose a0Aa_{0} \in A (as AA \neq \varnothing) and b0Ab_{0} \notin A (as AQA \neq \mathbb{Q}).

A1L2choose
2.1

(A-A is a cut) A-A satisfies (C1)–(C3), so A-A is a Dedekind cut.

step 1.1step 1.2step 1.3step 1.4A1
2.2

(bounded above) Apply [L1] to the rational b0/wb_{0}/w: there is a natural MM with b0/w<Mb_{0}/w < M, so b0<Mwb_{0} < Mw since w>0w > 0; because b0Ab_{0} \notin A and Mw>b0Mw > b_{0}, the contrapositive of (C2) gives MwAMw \notin A, whence any kZk \in \mathbb{Z} with kwAkw \in A satisfies k<Mk < M (else kMk \ge M gives kwMwkw \ge Mw, so kwAkw \notin A by the contrapositive of (C2)), so K:={kZ:kwA}K := \{\, k \in \mathbb{Z} : kw \in A \,\} is bounded above by MM.

step 1.6L1L2A1
2.3

(nonempty) Apply [L1] to the rational a0/w-a_{0}/w: there is a natural NN with a0/w<N-a_{0}/w < N, so Nw<a0-Nw < a_{0} since w>0w > 0; because a0Aa_{0} \in A and Nw<a0-Nw < a_{0}, (C2) gives NwA-Nw \in A, so NK-N \in K and KK \neq \varnothing.

step 1.6L1L2A1
3.1

(greatest element) KK is a nonempty set of integers bounded above, so by [A2] it has a greatest element nn; then nwAnw \in A because nKn \in K, while n+1>nn + 1 > n gives n+1Kn + 1 \notin K, i.e. (n+1)wA(n+1)w \notin A.

step 2.2step 2.3A2
4.1

(0A+(A)0^{*} \subseteq A + (-A)) With nn from step 3.1, set p:=(n+2)wp := -(n+2)w; the witness r=w>0r = w > 0 gives pw=(n+1)wA-p - w = (n+1)w \notin A, so pAp \in -A, while nwAnw \in A, and nw+p=nw(n+2)w=2w=vnw + p = nw - (n+2)w = -2w = v. Hence v=nw+pA+(A)v = nw + p \in A + (-A); as v0v \in 0^{*} was arbitrary, 0A+(A)0^{*} \subseteq A + (-A).

step 3.1A1L2
5.1

The inclusions of steps 1.5 and 4.1 give A+(A)=0A + (-A) = 0^{*}; with A-A a cut (step 2.1) and A+(A)A + (-A) therefore a cut [L3], AA has additive inverse A-A.

step 1.5step 4.1step 2.1L3
DefinitionDefinition: AI-adaptedProof: Not applicableverified 2026-08-02 (claude-opus-5)Open item page →

Multiplication and reciprocals of Dedekind cuts

Definition

Multiplication of Dedekind cuts (Dedekind cut, The real numbers R\mathbb{R} as Dedekind cuts) is defined first for nonnegative cuts, then extended to all cuts by their signs (Order on the Dedekind reals) via the absolute value.

Positive case. For cuts A,B>0A, B > 0^{*} (strictly positive),

AB:={qQ:q0}    {ab:aA, bB, a>0, b>0}.A \cdot B := \{\, q \in \mathbb{Q} : q \le 0 \,\} \;\cup\; \{\, a b : a \in A,\ b \in B,\ a > 0,\ b > 0 \,\}.

Absolute value. A:=A|A| := A if A0A \ge 0^{*}, and A:=A|A| := -A otherwise (Addition, negation, and subtraction of Dedekind cuts for A-A); thus A0|A| \ge 0^{*} always, and 0=0|0^{*}| = 0^{*}.

Sign extension. For arbitrary cuts A,BA, B,

  • AB:=0A \cdot B := 0^{*} if A=0A = 0^{*} or B=0B = 0^{*};
  • AB:=ABA \cdot B := |A| \cdot |B| if A,BA, B are both >0> 0^{*} or both <0< 0^{*};
  • AB:=(AB)A \cdot B := -\bigl(|A| \cdot |B|\bigr) if A,BA, B have opposite signs.

Identity. The multiplicative identity is 1={rQ:r<1}1^{*} = \{\, r \in \mathbb{Q} : r < 1 \,\}.

Reciprocal. For A>0A > 0^{*},

A1:={pQ:p0}    {p>0:sQ, s>0, sA, p<1/s}.A^{-1} := \{\, p \in \mathbb{Q} : p \le 0 \,\} \;\cup\; \{\, p > 0 : \exists\, s \in \mathbb{Q},\ s > 0,\ s \notin A,\ p < 1/s \,\}.

Equivalently, a positive rational pp lies in A1A^{-1} iff 1/p1/p is an upper rational bound of AA that is not the least one (Rudin's construction). For A<0A < 0^{*}, set A1:=((A)1)A^{-1} := -\bigl((-A)^{-1}\bigr). Division is A/B:=AB1A / B := A \cdot B^{-1} for B0B \ne 0^{*}.

Remarks

  • The product formula is stated only for strictly positive cuts A,B>0A, B > 0^{*}: then there exist positive aAa \in A, bBb \in B, so the positive products abab are nonempty and, because A,BA, B have no greatest element (axiom (C3)), ABA \cdot B has none either; together with downward closure this makes ABA \cdot B a genuine cut, the clause {q0}\{q \le 0\} being absorbed below those positive products. The formula is deliberately not applied at the boundary A=0A = 0^{*} or B=0B = 0^{*}, where {q0}\{q \le 0\} would leave 00 as a greatest element and so fail to be a cut; products with a zero factor are supplied instead by the first sign rule, AB=0A \cdot B = 0^{*}, so the operation is well posed on all cuts.
  • On the rational embedding qqq \mapsto q^{*} the operation agrees with Q\mathbb{Q}: (pq)=pq(pq)^{*} = p^{*} \cdot q^{*} (The rational cuts embed densely in R\mathbb{R}, preserving sums, products, 00, 11 and the order); with q(1/q)=1q^{*} \cdot (1/q)^{*} = 1^{*} that gives (q)1=(1/q)(q^{*})^{-1} = (1/q)^{*} for q>0q > 0, the reciprocal being the one supplied by For a positive cut AA, the reciprocal A1A^{-1} satisfies AA1=1A \cdot A^{-1} = 1^{*}.
  • That these operations send cuts to cuts and satisfy the field axioms ( commutativity, associativity, distributivity over addition, identity 11^{*}, and AA1=1A \cdot A^{-1} = 1^{*} for every A0A \ne 0^{*}) is The Dedekind reals form a field.
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

For a positive cut AA, the reciprocal A1A^{-1} satisfies AA1=1A \cdot A^{-1} = 1^{*}

Statement

For A>0A > 0^{*}, the reciprocal A1A^{-1} (Multiplication and reciprocals of Dedekind cuts) is a Dedekind cut with A1>0A^{-1} > 0^{*}, and AA1=1A \cdot A^{-1} = 1^{*}.

Facts & Assumptions

Given: A cut AA with A>0A > 0^{*}, and the multiplicative identity 1={rQ:r<1}1^{*} = \{ r \in \mathbb{Q} : r < 1 \}.

[L1]

Nonnegative product: for A,B>0A, B > 0^{*}, AB={q0}{ab:aA,bB,a>0,b>0}A \cdot B = \{q \le 0\} \cup \{ab : a \in A,\, b \in B,\, a > 0,\, b > 0\} (Multiplication and reciprocals of Dedekind cuts).

[L2]

Reciprocal: for A>0A > 0^{*}, A1={p0}{p>0:sQ, s>0, sA, p<1/s}A^{-1} = \{p \le 0\} \cup \{\, p > 0 : \exists\, s \in \mathbb{Q},\ s > 0,\ s \notin A,\ p < 1/s \,\} (Multiplication and reciprocals of Dedekind cuts).

[L3]

A>0A > 0^{*} means AA contains a positive rational; and every cut is a proper, downward-closed set of rationals with no greatest element (Order on the Dedekind reals, Dedekind cut).

[L4]

Q\mathbb{Q} is a field: rational addition and multiplication are commutative and associative, multiplication distributes over addition, and every nonzero rational is invertible (The rationals form a field); the order is total, xyx \le y implies x+zy+zx + z \le y + z, and 0<x0 < x, 0<y0 < y imply 0<xy0 < xy (The rationals form a totally ordered field).

[L6]

Every nonempty subset SNS \subseteq \mathbb{N} has a least element: there is S\ell \in S with s\ell \le s for all sSs \in S (The well-ordering principle).

[L5]

Rational power growth: for a rational y>1y > 1 one has yn1+n(y1)y^{n} \ge 1 + n(y-1) for every natural n1n \ge 1, by induction from Q\mathbb{Q} arithmetic — at n=1n = 1 both sides are yy, and if yn1+n(y1)y^{n} \ge 1 + n(y-1) then, multiplying by y>0y > 0 and writing y=1+(y1)y = 1 + (y-1), yn+1(1+(y1))(1+n(y1))=1+(n+1)(y1)+n(y1)21+(n+1)(y1)y^{n+1} \ge (1 + (y-1))(1 + n(y-1)) = 1 + (n+1)(y-1) + n(y-1)^{2} \ge 1 + (n+1)(y-1) because n(y1)20n(y-1)^{2} \ge 0; and by the Archimedean property every rational is exceeded by some such power; since a cut is proper it omits a rational upper bound, so for any a0>0a_{0} > 0 some a0ynAa_{0} y^{n} \notin A (The rationals are Archimedean, Dedekind cut).

Proof

technique · direct
1.1

A1A^{-1} is a cut with A1>0A^{-1} > 0^{*}: since A>0A > 0^{*} contains 00 and hence, by downward closure, all rationals 0\le 0, every sAs \notin A is positive; fix a0Aa_{0} \in A with a0>0a_{0} > 0, so any positive pA1p \in A^{-1} has p<1/s<1/a0p < 1/s < 1/a_{0} (its witness sAs \notin A satisfies s>a0s > a_{0}), making A1A^{-1} proper; it is nonempty (it contains 00) and downward closed: a q0q \le 0 lies in the {p0}\{p \le 0\} clause, and if 0<q<p0 < q < p with pA1p \in A^{-1} carrying witness ss (p<1/sp < 1/s) then q<p<1/sq < p < 1/s, so qA1q \in A^{-1} with the same witness ss; it contains a positive pp (take any sAs \notin A and 0<p<1/s0 < p < 1/s), and has no greatest element: a p0p \le 0 is exceeded by the positive element just exhibited, while any positive pA1p \in A^{-1} carries a witness s>0s > 0, sAs \notin A with p<1/sp < 1/s, and the rational p=(p+1/s)/2p' = (p + 1/s)/2 satisfies p<p<1/sp < p' < 1/s, so pp' lies in A1A^{-1} with the same witness ss yet p>pp' > p.

L2L3L4
1.2

Inclusion AA11A \cdot A^{-1} \subseteq 1^{*}: any q0q \le 0 in AA1A \cdot A^{-1} lies in 11^{*}, and if aAa \in A, pA1p \in A^{-1} with a,p>0a, p > 0, choose sAs \notin A, s>0s > 0, p<1/sp < 1/s, so a<sa < s (as aAa \in A, sAs \notin A) and ap<s(1/s)=1ap < s \cdot (1/s) = 1, giving ap1ap \in 1^{*}.

L1L2L3L4
1.3

For the reverse inclusion fix a target xx with 0<x<10 < x < 1: pick a rational tt with x<t<1x < t < 1 (betweenness in Q\mathbb{Q}) and set y:=1/ty := 1/t, so y>1y > 1; choose a0Aa_{0} \in A with a0>0a_{0} > 0 (as A>0A > 0^{*}); by rational power growth some power a0ynAa_{0} y^{n} \notin A, so {n1:a0ynA}\{\, n \ge 1 : a_{0} y^{n} \notin A \,\} is a nonempty set of naturals.

L3L4L5
2.1

Let n1n \ge 1 be the least natural with a0ynAa_{0} y^{n} \notin A (nonempty by step 1.3; n1n \ge 1 since a0y0=a0Aa_{0} y^{0} = a_{0} \in A); by minimality a:=a0yn1Aa := a_{0} y^{n-1} \in A with a>0a > 0, while s:=a0yn=ayAs := a_{0} y^{n} = a \cdot y \notin A with s>0s > 0.

L4L6step 1.3choose
3.1

Set p:=x/a>0p := x/a > 0; since x<t=1/yx < t = 1/y gives 1/x>y1/x > y, we get 1/p=a/x>ay=s1/p = a/x > a \cdot y = s, so p<1/sp < 1/s with s>0s > 0, sAs \notin A, whence pA1p \in A^{-1} by the reciprocal's definition; then x=apx = a \cdot p with aAa \in A, pA1p \in A^{-1}, a,p>0a, p > 0, so xAA1x \in A \cdot A^{-1}, and with the {q0}\{q \le 0\} clause this yields 1AA11^{*} \subseteq A \cdot A^{-1}.

L1L2L4step 1.1step 1.3step 2.1algebra
4.1

Combining the two inclusions gives AA1=1A \cdot A^{-1} = 1^{*}, and by step 1.1 the reciprocal A1A^{-1} is a Dedekind cut with A1>0A^{-1} > 0^{*}.

step 1.1step 1.2step 3.1
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The Dedekind reals form a field

Statement

The set R\mathbb{R} of Dedekind cuts of Q\mathbb{Q} (The real numbers R\mathbb{R} as Dedekind cuts), with cut addition and cut multiplication (Addition, negation, and subtraction of Dedekind cuts, Multiplication and reciprocals of Dedekind cuts), is a field.

Facts & Assumptions

Given: Cuts A,B,CRA, B, C \in \mathbb{R}, the cut 00^{*} (additive identity) and 11^{*} (multiplicative identity).

[L1]

Nonnegative product: for A,B>0A, B > 0^{*}, AB={q0}{ab:aA,bB,a>0,b>0}A \cdot B = \{q \le 0\} \cup \{ab : a \in A,\, b \in B,\, a > 0,\, b > 0\} (Multiplication and reciprocals of Dedekind cuts).

[L2]

Sign rules and reciprocal: AB=0A \cdot B = 0^{*} if AA or BB is 00^{*}; AB=ABA \cdot B = |A||B| for equal signs and (AB)-(|A||B|) for opposite signs; and A1=((A)1)A^{-1} = -((-A)^{-1}) when A<0A < 0^{*} (Multiplication and reciprocals of Dedekind cuts).

[L3]

Absolute value: A=A|A| = A if A0A \ge 0^{*} and A=A|A| = -A otherwise, so A0|A| \ge 0^{*} (Multiplication and reciprocals of Dedekind cuts).

[L4]

Addition: A+B={a+b:aA,bB}A + B = \{a + b : a \in A,\, b \in B\}, with inverse A-A (Addition, negation, and subtraction of Dedekind cuts).

[L5]

(R,+)(\mathbb{R}, +) is an abelian group: ++ is well defined, commutative, associative, with identity 00^{*} (Cut addition: A+BA+B is a cut, commutative and associative, with identity 00^{*}) and inverses A+(A)=0A + (-A) = 0^{*} (For a cut AA, A-A is a cut and A+(A)=0A + (-A) = 0^{*}).

[L6]

Inclusion totally orders R\mathbb{R}, so exactly one of A>0A > 0^{*}, A=0A = 0^{*}, A<0A < 0^{*} holds (Inclusion totally orders the Dedekind reals).

[L7]

Q\mathbb{Q} is a field: rational multiplication is commutative, associative, distributes over addition, and every nonzero rational is invertible (The rationals form a field); its order is total, xyx \le y implies x+zy+zx + z \le y + z, and 0<x0 < x, 0<y0 < y imply 0<xy0 < xy (The rationals form a totally ordered field).

[L8]

The embedding qqq \mapsto q^{*} is an injective ring map with (pq)=pq(pq)^{*} = p^{*} \cdot q^{*} and 101^{*} \ne 0^{*} (The rational cuts embed densely in R\mathbb{R}, preserving sums, products, 00, 11 and the order).

[L9]

Multiplicative inverse of a positive cut: for A>0A > 0^{*}, the reciprocal A1A^{-1} is a cut with A1>0A^{-1} > 0^{*} and AA1=1A \cdot A^{-1} = 1^{*} (For a positive cut AA, the reciprocal A1A^{-1} satisfies AA1=1A \cdot A^{-1} = 1^{*}).

[L10]

Negation is an additive homomorphism on (R,+)(\mathbb{R}, +): (X+Y)=(X)+(Y)-(X + Y) = (-X) + (-Y), since ((X)+(Y))+(X+Y)=0\bigl((-X) + (-Y)\bigr) + (X + Y) = 0^{*} by commutativity, associativity, and the inverse law, so (X)+(Y)(-X) + (-Y) is the unique additive inverse of X+YX + Y (Cut addition: A+BA+B is a cut, commutative and associative, with identity 00^{*}, For a cut AA, A-A is a cut and A+(A)=0A + (-A) = 0^{*}).

[L11]

A cut AA is positive iff 0<A0^{*} < A, and 0<A0^{*} < A holds exactly when 0A0 \in A; in that case (C3) supplies aAa \in A with a>0a > 0 (Order on the Dedekind reals, Dedekind cut).

Proof

technique · direct
1.1

For A,B>0A, B > 0^{*}, ABA \cdot B is a cut: it is nonempty and proper, downward closed because any 0<y<ab0 < y < ab equals (y/b)b(y/b)\,b with 0<y/b<a0 < y/b < a in AA (so the positive part of ABA \cdot B is exactly {ab:aA,bB,a,b>0}\{ab : a \in A, b \in B, a, b > 0\}), and it has no greatest element because AA has none: given abab with aAa \in A, bBb \in B, a,b>0a, b > 0, choose aAa' \in A with a>aa' > a, and then abABa'b \in A \cdot B with ab>aba'b > ab since b>0b > 0; and 0B=00^{*} \cdot B = 0^{*} by the sign rule, so multiplication of nonnegatives lands in R\mathbb{R}.

L1L2L6L7L11
1.2

On nonnegatives multiplication is commutative: ABA \cdot B and BAB \cdot A are the same set, since {ab}={ba}\{ab\} = \{ba\} by commutativity of rational multiplication.

L1L7
1.3

Identity on nonnegatives: A1=AA \cdot 1^{*} = A for A0A \ge 0^{*}. For xAx \in A with x>0x > 0 pick aAa \in A, a>xa > x (no greatest element), so x=a(x/a)x = a \cdot (x/a) with 0<x/a<10 < x/a < 1, giving AA1A \subseteq A \cdot 1^{*}; conversely ar<aAa r < a \in A for 0<r<10 < r < 1 forces arAar \in A, so A1AA \cdot 1^{*} \subseteq A; the 00^{*} case is the sign rule.

L1L7
1.4

101^{*} \ne 0^{*}, as the embedding is injective and 101 \ne 0 in Q\mathbb{Q}.

L8
1.5

For the reverse inclusion of distributivity, dispose of degenerate cases: if A=0A = 0^{*} then AB=AC=A(B+C)=0A \cdot B = A \cdot C = A \cdot (B + C) = 0^{*}, so AB+AC=0=A(B+C)A \cdot B + A \cdot C = 0^{*} = A \cdot (B + C); if B=0B = 0^{*} then AB=0A \cdot B = 0^{*} and B+C=0+C=CB + C = 0^{*} + C = C (additive identity), so AB+AC=0+AC=AC=A(B+C)A \cdot B + A \cdot C = 0^{*} + A \cdot C = A \cdot C = A \cdot (B + C), and symmetrically if C=0C = 0^{*}.

L2L4L5
1.6

Sign rule: for all cuts X,YX, Y, (X)Y=(XY)(-X) \cdot Y = -(X \cdot Y) and X(Y)=(XY)X \cdot (-Y) = -(X \cdot Y); indeed X=X|-X| = |X| so both sides keep magnitude XY|X| |Y|, while negating one factor toggles the same-sign versus opposite-sign classification of the pair and hence flips the product's sign in the definition AB=0A \cdot B = 0^{*} / AB|A| |B| / (AB)-(|A| |B|) (the 00^{*} case being immediate), so in particular XY=(XY)X \cdot Y = -(|X| \cdot Y) whenever X<0X < 0^{*}.

L2L3L6
2.1

On nonnegatives multiplication is associative: by step 1.1 the positive elements of ABA \cdot B are exactly the products abab, so those of (AB)C(A \cdot B) \cdot C are the (ab)c=abc(ab)c = abc, and likewise A(BC)A \cdot (B \cdot C) has positive part the a(bc)=abca(bc) = abc; both sides are thus {q0}{abc:aA,bB,cC,a,b,c>0}\{q \le 0\} \cup \{abc : a \in A, b \in B, c \in C,\, a,b,c > 0\}, by associativity of rational products.

step 1.1L1L7
2.2

Distributivity on nonnegatives, inclusion \subseteq for A,B,C0A, B, C \ge 0^{*}: a positive element of A(B+C)A \cdot (B + C) is awa \cdot w with aAa \in A, wB+Cw \in B + C, a,w>0a, w > 0, and w=b+cw = b + c for some bBb \in B, cCc \in C; then aw=ab+aca \cdot w = ab + ac where abABab \in A \cdot B and acACac \in A \cdot C (each product lies in the positive part of its factor product when positive, otherwise in that product's {q0}\{q \le 0\} clause), so awAB+ACa \cdot w \in A \cdot B + A \cdot C; with the {q0}\{q \le 0\} clause this gives A(B+C)AB+ACA \cdot (B + C) \subseteq A \cdot B + A \cdot C.

L1L4L7step 1.1
2.3

For the reverse inclusion assume A,B,C>0A, B, C > 0^{*}, the degenerate cases being step 1.5; then ABA \cdot B and ACA \cdot C each contain a positive rational and, being downward-closed cuts (step 1.1), contain positive rationals arbitrarily close to 00.

L1L11step 1.1step 1.5
2.4

Every A0A \ne 0^{*} has a multiplicative inverse: for A>0A > 0^{*} the reciprocal A1A^{-1} satisfies AA1=1A \cdot A^{-1} = 1^{*}; for A<0A < 0^{*} we have A>0-A > 0^{*} and A1=((A)1)A^{-1} = -((-A)^{-1}), so applying the sign rule to both factors gives AA1=(A)(A)1=1A \cdot A^{-1} = (-A) \cdot (-A)^{-1} = 1^{*} by the reciprocal of the positive cut A-A.

L2L3L9step 1.6
3.1

Take uAB+ACu \in A \cdot B + A \cdot C with u>0u > 0, say u=s+tu = s + t with sABs \in A \cdot B, tACt \in A \cdot C: if t0t \le 0, pick a positive tACt' \in A \cdot C with t<ut' < u (available by step 2.3) and set s:=uts' := u - t', so 0<ss0 < s' \le s (since t0t \le 0 gives su>ss \ge u > s') and sABs' \in A \cdot B by downward closure, then replace (s,t)(s, t) by (s,t)(s', t'); symmetrically if s0s \le 0; so we may assume s,t>0s, t > 0.

L4step 1.1step 2.3
3.2

The nonnegative laws now extend by signs: ABA \cdot B and BAB \cdot A share magnitude AB=BA|A| |B| = |B| |A| and the same sign, hence are equal (step 1.2); (AB)C(A \cdot B) \cdot C and A(BC)A \cdot (B \cdot C) share magnitude ABC|A| |B| |C| and the sign given by the product of the three factor signs, hence are equal (step 2.1); and A1=AA \cdot 1^{*} = A, since 1>01^{*} > 0^{*} leaves the sign of AA unchanged and A1=A|A| \cdot 1^{*} = |A| (step 1.3).

L2L3step 1.2step 1.3step 2.1
4.1

With s,t>0s, t > 0 from step 3.1, step 1.1 gives s=a1b1s = a_{1} b_{1} and t=a2c1t = a_{2} c_{1} with a1,a2Aa_{1}, a_{2} \in A, b1Bb_{1} \in B, c1Cc_{1} \in C all positive; set a:=max(a1,a2)a := \max(a_{1}, a_{2}), so aAa \in A and a>0a > 0.

L11step 1.1step 3.1
5.1

Put b:=s/ab := s/a and c:=t/ac := t/a: then 0<b=a1b1/ab10 < b = a_{1} b_{1}/a \le b_{1}, so bBb \in B, and 0<c=a2c1/ac10 < c = a_{2} c_{1}/a \le c_{1}, so cCc \in C, both by downward closure; hence u=s+t=ab+ac=a(b+c)u = s + t = ab + ac = a(b + c) with b+cB+Cb + c \in B + C, b+c>0b + c > 0, aAa \in A, a>0a > 0, so uA(B+C)u \in A \cdot (B + C).

L1L4L7step 4.1
6.1

Hence for A,B,C>0A, B, C > 0^{*} and uAB+ACu \in A \cdot B + A \cdot C: if u0u \le 0 then uA(B+C)u \in A \cdot (B + C) by its {q0}\{q \le 0\} clause, and if u>0u > 0 then uA(B+C)u \in A \cdot (B + C) by step 5.1, so AB+ACA(B+C)A \cdot B + A \cdot C \subseteq A \cdot (B + C); with step 2.2 this gives A(B+C)=AB+ACA \cdot (B + C) = A \cdot B + A \cdot C, an equality that also holds in the degenerate cases of step 1.5, so distributivity holds for all A,B,C0A, B, C \ge 0^{*}.

L1step 1.5step 2.2step 5.1
7.1

Distributivity for A0A \ge 0^{*} with B,C0B, C \le 0^{*}: writing B=BB = -|B|, C=CC = -|C| so that B+C=(B)+(C)=(B+C)B + C = (-|B|) + (-|C|) = -(|B| + |C|) by [L10], the sign rule and nonnegative distributivity give A(B+C)=(A(B+C))=(AB+AC)=((AB))+((AC))=AB+ACA \cdot (B + C) = -(A \cdot (|B| + |C|)) = -(A \cdot |B| + A \cdot |C|) = (-(A \cdot |B|)) + (-(A \cdot |C|)) = A \cdot B + A \cdot C, the last equality using that negation is an additive homomorphism.

L3L5L10step 6.1step 1.6
7.2

Distributivity for A0A \ge 0^{*} with B0CB \ge 0^{*} \ge C and D:=B+C0D := B + C \ge 0^{*}: then B=D+CB = D + |C| with D,C0D, |C| \ge 0^{*}, so AB=AD+ACA \cdot B = A \cdot D + A \cdot |C| by nonnegative distributivity, whence AD=ABAC=AB+ACA \cdot D = A \cdot B - A \cdot |C| = A \cdot B + A \cdot C because AC=(AC)A \cdot C = -(A \cdot |C|) by the sign rule; that is A(B+C)=AB+ACA \cdot (B + C) = A \cdot B + A \cdot C.

L3L4L5step 6.1step 1.6
7.3

Distributivity for A0A \ge 0^{*} with B0CB \ge 0^{*} \ge C and D:=B+C<0D := B + C < 0^{*}: then C=B+D|C| = B + |D| with B,D0B, |D| \ge 0^{*}, so AC=AB+ADA \cdot |C| = A \cdot B + A \cdot |D| by nonnegative distributivity, giving AC=(AC)=((AB))+((AD))A \cdot C = -(A \cdot |C|) = (-(A \cdot B)) + (-(A \cdot |D|)) and AD=(AD)A \cdot D = -(A \cdot |D|) by the sign rule, whence AB+AC=(AD)=AD=A(B+C)A \cdot B + A \cdot C = -(A \cdot |D|) = A \cdot D = A \cdot (B + C).

L3L4L5step 6.1step 1.6
8.1

Distributivity for A0A \ge 0^{*} and arbitrary B,CB, C: if B,C0B, C \ge 0^{*} this is step 6.1; if B,C0B, C \le 0^{*} it is step 7.1; otherwise one factor is 0\ge 0^{*} and the other 0\le 0^{*}, say B0CB \ge 0^{*} \ge C (else exchange B,CB, C using commutativity of ++), and then it is step 7.2 or step 7.3 according as B+C0B + C \ge 0^{*} or B+C<0B + C < 0^{*}; by the sign trichotomy these cases are exhaustive, so A(B+C)=AB+ACA \cdot (B + C) = A \cdot B + A \cdot C.

L5L6step 6.1step 7.1step 7.2step 7.3
9.1

Distributivity for A<0A < 0^{*}: the sign rule gives A(B+C)=(A(B+C))A \cdot (B + C) = -(|A| \cdot (B + C)) and AB+AC=((AB))+((AC))=(AB+AC)A \cdot B + A \cdot C = (-(|A| \cdot B)) + (-(|A| \cdot C)) = -(|A| \cdot B + |A| \cdot C), while A0|A| \ge 0^{*} makes step 8.1 apply to give A(B+C)=AB+AC|A| \cdot (B + C) = |A| \cdot B + |A| \cdot C, so the two negated cuts coincide and A(B+C)=AB+ACA \cdot (B + C) = A \cdot B + A \cdot C.

L3L5L10step 1.6step 8.1
10.1

By the sign trichotomy every cut AA is either 0\ge 0^{*} (step 8.1) or <0< 0^{*} (step 9.1), so A(B+C)=AB+ACA \cdot (B + C) = A \cdot B + A \cdot C holds for all cuts A,B,CA, B, C.

L6step 8.1step 9.1
11.1

Thus (R,+)(\mathbb{R}, +) is an abelian group (L5), multiplication is commutative and associative with identity 101^{*} \ne 0^{*} (step 3.2, step 1.4), distributes over addition (step 10.1), and every nonzero cut is invertible (step 2.4): R\mathbb{R} is a field.

L5step 1.4step 3.2step 10.1step 2.4
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The rational cuts embed densely in R\mathbb{R}, preserving sums, products, 00, 11 and the order

Statement

The rational embedding qqq \mapsto q^{*}, where q={rQ:r<q}q^{*} = \{\, r \in \mathbb{Q} : r < q \,\} (The real numbers R\mathbb{R} as Dedekind cuts), is injective and order-preserving-and-reflecting, p<q    pqp < q \iff p^{*} \subsetneq q^{*}, and a ring embedding: (p+q)=p+q(p+q)^{*} = p^{*} + q^{*}, (pq)=pq(pq)^{*} = p^{*} \cdot q^{*}, 000 \mapsto 0^{*}, 111 \mapsto 1^{*}. Moreover its image is dense: for cuts A<BA < B there is a rational qq with A<q<BA < q^{*} < B.

Facts & Assumptions

Given: Rationals p,qp, q, the embedding qq={rQ:r<q}q \mapsto q^{*} = \{\, r \in \mathbb{Q} : r < q \,\}, and cuts A,BA, B (The real numbers R\mathbb{R} as Dedekind cuts).

[L1]

Cut structure: downward closure (pAp \in A, q<pqAq < p \Rightarrow q \in A), the separation property (aAa \in A, bAa<bb \notin A \Rightarrow a < b), and the absence of a greatest element (Dedekind cut), holding of every element of R\mathbb{R} (The real numbers R\mathbb{R} as Dedekind cuts).

[L2]

Order is inclusion: A<BA < B means ABA \subsetneq B (Order on the Dedekind reals).

[L3]

Trichotomy, transitivity, and irreflexivity of the rational order (The rationals form a totally ordered field).

[L4]

Cut addition is the rational sumset A+B={a+b:aA, bB}A + B = \{\, a + b : a \in A,\ b \in B \,\}, the additive inverse is A={pQ:r>0, prA}-A = \{\, p \in \mathbb{Q} : \exists\, r > 0,\ -p - r \notin A \,\}, and 0={qQ:q<0}0^{*} = \{\, q \in \mathbb{Q} : q < 0 \,\} is the additive identity of the embedding (Addition, negation, and subtraction of Dedekind cuts).

[L5]

Cut multiplication: for A,B>0A, B > 0^{*}, AB={q0}{ab:aA, bB, a>0, b>0}A \cdot B = \{\, q \le 0 \,\} \cup \{\, ab : a \in A,\ b \in B,\ a > 0,\ b > 0 \,\}; the sign rules AB=0A \cdot B = 0^{*} when AA or BB is 00^{*}, AB=ABA \cdot B = |A|\,|B| for equal signs and AB=(AB)A \cdot B = -(|A|\,|B|) for opposite signs; and A=A|A| = A for A0A \ge 0^{*} else A=A|A| = -A, with 1={r<1}1^{*} = \{\, r < 1 \,\} the multiplicative identity (Multiplication and reciprocals of Dedekind cuts).

[L6]

Q\mathbb{Q} is a field: rational addition and multiplication are commutative and associative, multiplication distributes over addition, and every nonzero rational is invertible (The rationals form a field); its order is total, xyx \le y implies x+zy+zx + z \le y + z, and 0<x0 < x, 0<y0 < y imply 0<xy0 < xy (The rationals form a totally ordered field). Consequently multiplying a<ba < b by a positive preserves the order, and every pair r<sr < s has the strict midpoint r<(r+s)/2<sr < (r+s)/2 < s, since 2=1+1>02 = 1 + 1 > 0 is invertible and 2r<r+s<2s2r < r + s < 2s.

Proof

technique · direct
1.1

Order preservation: if p<qp < q then pqp^{*} \subsetneq q^{*}. For rpr \in p^{*} we have r<p<qr < p < q, so rqr \in q^{*}, giving pqp^{*} \subseteq q^{*}; and pqp \in q^{*} while ppp \notin p^{*}, so the inclusion is proper.

L3
1.2

Order reflection: if pqp^{*} \subsetneq q^{*} then p<qp < q. Pick rqpr \in q^{*} \setminus p^{*}; then r<qr < q and ¬(r<p)\neg(r < p), so pr<qp \le r < q, whence p<qp < q.

L3
1.3

Unit identities: 000 \mapsto 0^{*} and 111 \mapsto 1^{*} hold because 0={r<0}0^{*} = \{\, r < 0 \,\} and 1={r<1}1^{*} = \{\, r < 1 \,\} are exactly the cuts named by the embedding at 00 and 11 and fixed as the additive and multiplicative identities.

L4L5
1.4

Additive identity, inclusion p+q(p+q)p^{*} + q^{*} \subseteq (p+q)^{*}: a typical element is a+ba + b with a<pa < p and b<qb < q, and order compatibility of rational addition gives a+b<p+qa + b < p + q, so a+b(p+q)a + b \in (p+q)^{*}.

L4L6
1.5

Additive identity, inclusion (p+q)p+q(p+q)^{*} \subseteq p^{*} + q^{*}: given r<p+qr < p + q set d=(p+qr)/2>0d = (p + q - r)/2 > 0, a=pda = p - d, b=qdb = q - d; then a<pa < p, b<qb < q, and a+b=(p+q)2d=ra + b = (p + q) - 2d = r, so r=a+bp+qr = a + b \in p^{*} + q^{*}.

L4L6
1.6

Nonnegative product, inclusion pq(pq)p^{*} \cdot q^{*} \subseteq (pq)^{*} for p,q>0p, q > 0: an element is either 0\le 0, hence in (pq)(pq)^{*} since pq>0pq > 0, or abab with 0<a<p0 < a < p and 0<b<q0 < b < q, and then ab<pb<pqab < pb < pq, so ab(pq)ab \in (pq)^{*}.

L5L6
1.7

Nonnegative product, inclusion (pq)pq(pq)^{*} \subseteq p^{*} \cdot q^{*} for p,q>0p, q > 0: take r<pqr < pq; if r0r \le 0 it lies in the {q0}\{\, q \le 0 \,\} clause, and if r>0r > 0 then r/q<pr/q < p, so the strict midpoint a=(r/q+p)/2a = (r/q + p)/2 satisfies r/q<a<pr/q < a < p, and b=r/ab = r/a gives 0<a<p0 < a < p and 0<b<q0 < b < q (as a>r/q>0a > r/q > 0 yields b=r/a<qb = r/a < q), with ab=rpqab = r \in p^{*} \cdot q^{*}.

L5L6choose
1.8

Density setup: let A<BA < B, i.e. ABA \subsetneq B; choose xBAx \in B \setminus A, and since BB has no greatest element choose yBy \in B with y>xy > x.

L1L2choose
1.9

Negation identity (p)=(p)-(p^{*}) = (-p)^{*}: by the negation definition (p)={r:t>0, rtp}={r:t>0, rtp}={r:t>0, rpt}={r:r<p}=(p)-(p^{*}) = \{\, r : \exists\, t > 0,\ -r - t \notin p^{*} \,\} = \{\, r : \exists\, t > 0,\ -r - t \ge p \,\} = \{\, r : \exists\, t > 0,\ r \le -p - t \,\} = \{\, r : r < -p \,\} = (-p)^{*}, where rtp-r - t \notin p^{*} gives rtp-r - t \ge p by trichotomy and t=pr>0t = -p - r > 0 witnesses the last equality.

L4L3L6
2.1

Additive identity: combining the two inclusions, (p+q)=p+q(p+q)^{*} = p^{*} + q^{*}.

step 1.4step 1.5
2.2

Nonnegative multiplicative identity: for p,q>0p, q > 0 the two inclusions give (pq)=pq(pq)^{*} = p^{*} \cdot q^{*}, while if p=0p = 0 or q=0q = 0 then pq=0pq = 0 and the sign rule 0B=00^{*} \cdot B = 0^{*} gives (pq)=0=pq(pq)^{*} = 0^{*} = p^{*} \cdot q^{*}; hence (pq)=pq(pq)^{*} = p^{*} \cdot q^{*} for all p,q0p, q \ge 0.

step 1.6step 1.7L5
2.3

Injectivity: if p=qp^{*} = q^{*} then neither pqp^{*} \subsetneq q^{*} nor qpq^{*} \subsetneq p^{*}, so by reflection ¬(p<q)\neg(p < q) and ¬(q<p)\neg(q < p); trichotomy forces p=qp = q.

step 1.2L3
2.4

Combining preservation and reflection, p<q    pqp < q \iff p^{*} \subsetneq q^{*}, that is p<q    p<qp < q \iff p^{*} < q^{*}: the embedding preserves and reflects order.

step 1.1step 1.2L2
2.5

A<yA < y^{*}: for aAa \in A, separation gives a<xa < x (as xAx \notin A) and x<yx < y, so a<ya < y and aya \in y^{*}, whence AyA \subseteq y^{*}; and xyx \in y^{*} (since x<yx < y) while xAx \notin A, so the inclusion is proper, AyA \subsetneq y^{*}.

step 1.8L1L2L3
2.6

y<By^{*} < B: for ryr \in y^{*}, r<yr < y and yBy \in B, so downward closure gives rBr \in B, whence yBy^{*} \subseteq B; and yBy \in B while yyy \notin y^{*}, so yBy^{*} \subsetneq B.

step 1.8L1L2
2.7

Absolute value identity p=p|p^{*}| = |p|^{*}: since 0p    0^{*} \subseteq p^{*} \iff every r<0r < 0 satisfies r<p    p0r < p \iff p \ge 0, we have p0    p0p \ge 0 \iff p^{*} \ge 0^{*}; if p0p \ge 0 then p=p=p|p^{*}| = p^{*} = |p|^{*}, while if p<0p < 0 then p<0p^{*} < 0^{*}, so p=(p)=(p)=p|p^{*}| = -(p^{*}) = (-p)^{*} = |p|^{*} using (p)=(p)-(p^{*}) = (-p)^{*} and p=p|p| = -p.

step 1.9L2L3L5
3.1

Multiplicative identity for all signs: the sign rules give pq=±(pq)p^{*} \cdot q^{*} = \pm(|p^{*}| \cdot |q^{*}|), and pq=pq=(pq)|p^{*}| \cdot |q^{*}| = |p|^{*} \cdot |q|^{*} = (|p|\,|q|)^{*} by the absolute-value identity and the nonnegative case; when p,qp, q share a sign pq0pq \ge 0 and pq=pq|p|\,|q| = pq, so pq=(pq)p^{*} \cdot q^{*} = (pq)^{*}, and when they have opposite signs pq<0pq < 0, pq=pq|p|\,|q| = -pq, and ((pq))=(pq)-\bigl((-pq)^{*}\bigr) = (pq)^{*} by the negation identity, so again pq=(pq)p^{*} \cdot q^{*} = (pq)^{*} (the p=0p = 0 or q=0q = 0 case being step 2.2); hence (pq)=pq(pq)^{*} = p^{*} \cdot q^{*} for all p,qp, q.

step 2.2step 2.7step 1.9L5
4.1

Taking q=yq = y yields A<q<BA < q^{*} < B, so the image is dense; with injectivity, order preservation/reflection, and the ring identities (p+q)=p+q(p+q)^{*} = p^{*} + q^{*}, (pq)=pq(pq)^{*} = p^{*} \cdot q^{*}, 000 \mapsto 0^{*}, 111 \mapsto 1^{*}, the map qqq \mapsto q^{*} is a dense, order-preserving ring embedding of Q\mathbb{Q} into R\mathbb{R}. Closure of the image under reciprocals, which a subfield would also require, is not established here.

step 2.1step 3.1step 1.3step 2.3step 2.4step 2.5step 2.6
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

The Dedekind reals form a totally ordered field

Statement

The inclusion order AB:    ABA \le B :\iff A \subseteq B (Order on the Dedekind reals) makes R\mathbb{R}, the field of Dedekind cuts (The Dedekind reals form a field), a totally ordered field: the order is total, translation-invariant (ABA+CB+CA \le B \Rightarrow A + C \le B + C), and closed under multiplication of nonnegatives (0A0^{*} \le A and 0B0AB0^{*} \le B \Rightarrow 0^{*} \le A \cdot B).

Facts & Assumptions

Given: Cuts A,B,CA, B, C ordered by inclusion (Order on the Dedekind reals).

[L1]

R\mathbb{R} (Dedekind cuts) is a field under ++ and \cdot (The Dedekind reals form a field).

[L2]

Inclusion totally orders R\mathbb{R}: reflexive, antisymmetric, transitive, and total (Inclusion totally orders the Dedekind reals).

[L3]

Addition is the sumset A+B={a+b:aA, bB}A + B = \{\, a + b : a \in A,\ b \in B \,\}, with identity 00^{*} (Addition, negation, and subtraction of Dedekind cuts).

[L4]

For strictly positive cuts A,B>0A, B > 0^{*}, AB={qQ:q0}{ab:aA, bB, a>0, b>0}A \cdot B = \{\, q \in \mathbb{Q} : q \le 0 \,\} \cup \{\, a b : a \in A,\ b \in B,\ a > 0,\ b > 0 \,\}; and AB=0A \cdot B = 0^{*} whenever A=0A = 0^{*} or B=0B = 0^{*} (the sign rule). Also 0={rQ:r<0}0^{*} = \{\, r \in \mathbb{Q} : r < 0 \,\} (Multiplication and reciprocals of Dedekind cuts, Order on the Dedekind reals).

Proof

technique · direct
1.1

By Inclusion totally orders the Dedekind reals the relation \subseteq is a reflexive, antisymmetric, transitive, and total order on R\mathbb{R}.

L2
1.2

Translation invariance: suppose ABA \subseteq B. Every element of A+CA + C has the form a+ca + c with aAa \in A, cCc \in C; since aABa \in A \subseteq B, also a+cB+Ca + c \in B + C. Hence A+CB+CA + C \subseteq B + C, i.e. ABA+CB+CA \le B \Rightarrow A + C \le B + C.

L3
1.3

Positivity of products of nonnegatives: suppose 0A0^{*} \le A and 0B0^{*} \le B. If A=0A = 0^{*} or B=0B = 0^{*}, then AB=0A \cdot B = 0^{*} by the sign rule [L4], so 0AB0^{*} \subseteq A \cdot B. Otherwise A,B>0A, B > 0^{*}, and the positive-case formula [L4] gives AB{qQ:q0}{rQ:r<0}=0A \cdot B \supseteq \{\, q \in \mathbb{Q} : q \le 0 \,\} \supseteq \{\, r \in \mathbb{Q} : r < 0 \,\} = 0^{*}, so 0AB0^{*} \subseteq A \cdot B. In either case 0AB0^{*} \le A \cdot B.

L4
2.1

Thus R\mathbb{R} is a field whose inclusion order is total, translation-invariant, and closed under multiplication of nonnegative cuts: a totally ordered field.

step 1.1step 1.2step 1.3L1
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The Dedekind reals are Archimedean

Statement

R\mathbb{R} (Dedekind cuts) is Archimedean: for every cut AA there is a natural number nn with A<nA < n^{*}. Equivalently, the rational cuts (n)nN(n^{*})_{n \in \mathbb{N}} are cofinal in R\mathbb{R}: no single cut is an upper bound for all of them.

Facts & Assumptions

Given: A cut AA.

[L1]

A cut is a proper subset of Q\mathbb{Q} (AQA \ne \mathbb{Q}), and aAa \in A, bAa<bb \notin A \Rightarrow a < b (Dedekind cut); the elements of R\mathbb{R} are exactly these cuts (The real numbers R\mathbb{R} as Dedekind cuts).

[L2]

Rational Archimedean property: for every qQq \in \mathbb{Q} there is a natural number nn with n>qn > q (The rationals are Archimedean).

[L3]

The embedding preserves order: p<qpqp < q \Rightarrow p^{*} \subsetneq q^{*}, i.e. p<qp^{*} < q^{*} (The rational cuts embed densely in R\mathbb{R}, preserving sums, products, 00, 11 and the order).

[L4]

Inclusion order, and transitivity of << in the totally ordered field (Order on the Dedekind reals, The Dedekind reals form a totally ordered field).

Proof

technique · direct
1.1

Since AQA \ne \mathbb{Q}, choose a rational qAq \notin A.

L1choose
1.2

By the rational Archimedean property, choose a natural number nn with n>qn > q.

L2choose
2.1

AqA \subseteq q^{*}: for aAa \in A, the separation property gives a<qa < q (as qAq \notin A), so aqa \in q^{*}.

step 1.1L1
2.2

q<nq^{*} < n^{*}: from q<nq < n and order preservation, qnq^{*} \subsetneq n^{*}.

step 1.2L3
3.1

Hence AqnA \subseteq q^{*} \subsetneq n^{*}, so A<nA < n^{*}: the rational cuts are cofinal and R\mathbb{R} is Archimedean.

step 2.1step 2.2L4
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Dedekind completeness: the least-upper-bound property

Statement

Least-upper-bound property. Every nonempty set SS of Dedekind cuts that is bounded above (there is a cut BB with ABA \le B for all ASA \in S) has a least upper bound supS\sup S, and it is given explicitly by the union C:=ASA.C := \bigcup_{A \in S} A. Together with The Dedekind reals form a totally ordered field this shows R\mathbb{R} is a complete totally ordered field: the Dedekind construction is order-complete. This order-completeness is the Dedekind counterpart of the Cauchy-sequence completeness of R\mathbb{R}.

Facts & Assumptions

Given: A nonempty set SS of Dedekind cuts bounded above by a cut BB (ABA \le B for all ASA \in S), and C:=ASAC := \bigcup_{A \in S} A (The real numbers R\mathbb{R} as Dedekind cuts).

[L1]

Cut axioms: (C1) proper and nonempty, (C2) downward closed, (C3) no greatest element (Dedekind cut).

[L2]

Order is inclusion: AD    ADA \le D \iff A \subseteq D (Order on the Dedekind reals).

[L3]

Inclusion is a partial (indeed total) order, so upper and least-upper bounds are taken with respect to \subseteq (Inclusion totally orders the Dedekind reals).

[L4]

R\mathbb{R} is a totally ordered field; the least-upper-bound property below is the order-completeness that complements it (The Dedekind reals form a totally ordered field).

Proof

technique · direct
1.1

(C1) CC is nonempty and proper: SS has a member A0A_0 with A0A_0 \ne \emptyset and A0CA_0 \subseteq C, so CC \ne \emptyset; and every ASA \in S satisfies ABA \subseteq B, so C=ASABC = \bigcup_{A \in S} A \subseteq B with BQB \ne \mathbb{Q}, hence CQC \ne \mathbb{Q}.

givenL1L2
1.2

(C2) CC is downward closed: if pCp \in C then pAp \in A for some ASA \in S; for q<pq < p, downward closure of AA gives qACq \in A \subseteq C.

givenL1
1.3

(C3) CC has no greatest element: if pCp \in C then pAp \in A for some ASA \in S; as AA has no greatest element there is rAr \in A with r>pr > p, and rCr \in C.

givenL1
1.4

CC is an upper bound for SS: every ASA \in S satisfies AASA=CA \subseteq \bigcup_{A' \in S} A' = C, i.e. ACA \le C.

givenL2
1.5

CC is below every upper bound: if a cut DD satisfies ADA \le D for all ASA \in S, then ADA \subseteq D for all AA, so C=ASADC = \bigcup_{A \in S} A \subseteq D, i.e. CDC \le D.

givenL2L3
2.1

CC is a Dedekind cut.

step 1.1step 1.2step 1.3L1
3.1

Therefore supS\sup S exists and equals C=ASAC = \bigcup_{A \in S} A: R\mathbb{R} has the least-upper-bound property. With The Dedekind reals form a totally ordered field, R\mathbb{R} is a complete totally ordered field, the order-completeness of the Dedekind construction, the exact counterpart of Cauchy-sequence completeness.

step 2.1step 1.4step 1.5L4

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The cut S={q:q<0 or q2<2}S = \{q : q<0 \text{ or } q^2<2\} is an irrational real number

Example

The set S:={qQ:q<0 or q2<2}S := \{ q \in \mathbb{Q} : q < 0 \text{ or } q^2 < 2 \} is a Dedekind cut (Dedekind cut), hence a real number (The real numbers R\mathbb{R} as Dedekind cuts), yet no rational lies "at its boundary": it is the cut that names 2\sqrt{2}, the real number Q\mathbb{Q} lacks. It is the canonical witness that cuts capture limits missing from Q\mathbb{Q}, and the standard test case for the completeness of R\mathbb{R}.

Facts & Assumptions

Given: The set S:={qQ:q<0 or q2<2}S := \{ q \in \mathbb{Q} : q < 0 \text{ or } q^2 < 2 \}, the cut axioms (C1)–(C3) (Dedekind cut), and R\mathbb{R} as the set of all cuts with rational embedding qq={rQ:r<q}q \mapsto q^\ast = \{ r \in \mathbb{Q} : r < q \} (The real numbers R\mathbb{R} as Dedekind cuts).

[L1]

Q\mathbb{Q} is a totally ordered field; in particular squaring is order-preserving on nonnegatives (0a<ba2<b20 \le a < b \Rightarrow a^2 < b^2) and the usual rational arithmetic holds (The rationals form a totally ordered field).

[L2]

No rational number squares to 22 (FALSE: some rational number squares to 2).

Verification

technique · direct
1.1

(C1) 0S0 \in S since 02=0<20^2 = 0 < 2, so SS \ne \emptyset; and 2S2 \notin S since 2>02 > 0 and 22=4>22^2 = 4 > 2, so SQS \ne \mathbb{Q}.

givenL1
1.2

(C2) Let pSp \in S and q<pq < p. If q<0q < 0 then qSq \in S by definition. Otherwise 0q<p0 \le q < p, so p>0p > 0; then pSp \in S forces p2<2p^2 < 2, and 0q<p0 \le q < p gives q2<p2<2q^2 < p^2 < 2, whence qSq \in S.

givenL1
1.3

(C3, case q0q \le 0) Given qSq \in S with q0q \le 0, take r=1r = 1: then 1S1 \in S (as 12=1<21^2 = 1 < 2) and r=1>0qr = 1 > 0 \ge q, so r>qr > q.

givenL1
1.4

(C3, case q>0q > 0) Given qSq \in S with q>0q > 0, we have q2<2q^2 < 2; set r=2q+2q+2r = \dfrac{2q+2}{q+2}. Then rq=2q2q+2>0r - q = \dfrac{2 - q^2}{q+2} > 0, so r>q>0r > q > 0, while r22=2(q22)(q+2)2<0r^2 - 2 = \dfrac{2\,(q^2 - 2)}{(q+2)^2} < 0, so r2<2r^2 < 2; hence rSr \in S with r>qr > q.

givenL1algebra
2.1

(C3) Combining the two cases, every qSq \in S admits rSr \in S with r>qr > q: SS has no greatest element.

step 1.3step 1.4
3.1

By steps 1.1, 1.2 and 2.1, SS satisfies (C1)–(C3); it is a Dedekind cut (Dedekind cut), i.e. a real number (The real numbers R\mathbb{R} as Dedekind cuts).

step 1.1step 1.2step 2.1
4.1

Finally SpS \ne p^\ast for every pQp \in \mathbb{Q}: were S=p={r:r<p}S = p^\ast = \{ r : r < p \}, then pSp \notin S would give p>0p > 0 and p22p^2 \ge 2, while p2=2p^2 = 2 is impossible by [L2], so p2>2p^2 > 2; as p>0p > 0 we have p+2>0p + 2 > 0, and then s:=2p+2p+2s := \dfrac{2p+2}{p+2} satisfies 0<s<p0 < s < p and s2>2s^2 > 2, so sSs \notin S, yet s<ps < p puts sp=Ss \in p^\ast = S, a contradiction. Thus SS is a cut represented by no rational: it is the cut that names 2\sqrt{2}, the real number absent from Q\mathbb{Q}.

step 3.1L2algebra
False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

FALSE: some rational number squares to 2

Statement

False claim: there exists xQx \in \mathbb{Q} with x2=2x^2 = 2.

Facts & Assumptions

Given: The rationals as quotients of integer pairs (The rationals as equivalence classes of pairs of integers).

[A1]

Every rational can be written a/ba/b in lowest terms, with a,ba, b not both even (cancel common factors of 22; the process terminates by well-ordering of N\mathbb{N}).

[A2]

Parity in Z\mathbb{Z}: if k2k^2 is even then kk is even (an odd k=2j+1k = 2j+1 has odd square 4j2+4j+14j^2 + 4j + 1).

Refutation

technique · contradiction
1.1

Assume, for contradiction, that some xQx \in \mathbb{Q} has x2=2x^2 = 2; write x=a/bx = a/b in lowest terms, a,ba, b not both even.

assume-contraA1
2.1

Clearing denominators: a2=2b2a^2 = 2b^2.

step 1.1algebra
3.1

a2a^2 is even, hence aa is even: a=2ca = 2c.

step 2.1A2
4.1

Substituting: 4c2=2b24c^2 = 2b^2, so b2=2c2b^2 = 2c^2 is even, hence bb is even.

step 3.1A2algebra
5.1

Both aa and bb are even, contradicting the lowest-terms choice of step 1.1; the assumption fails: no rational squares to 22.

step 4.1step 1.1discharge-contradiction
False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

FALSE: every Dedekind cut has a greatest element

Statement

False claim: every Dedekind cut (Dedekind cut) has a greatest element: some mAm \in A with qmq \le m for all qAq \in A.

Facts & Assumptions

Given: The cut axioms (C1)–(C3) (Dedekind cut), R\mathbb{R} as the set of all cuts (The real numbers R\mathbb{R} as Dedekind cuts), and the rational cut 0:={qQ:q<0}0^\ast := \{ q \in \mathbb{Q} : q < 0 \}.

[L1]

Q\mathbb{Q} is a totally ordered field; in particular for q<0q < 0 the rational q/2q/2 satisfies q<q/2<0q < q/2 < 0 (The rationals form a totally ordered field).

Refutation

technique · direct
1.1

(C1, C2) 0={qQ:q<0}0^\ast = \{ q \in \mathbb{Q} : q < 0 \} is nonempty (10-1 \in 0^\ast) and proper (000 \notin 0^\ast), and it is downward closed: q<p<0q<0q < p < 0 \Rightarrow q < 0, so q0q \in 0^\ast.

givenL1
1.2

(C3) For any q0q \in 0^\ast, i.e. q<0q < 0, the rational q/2q/2 satisfies q<q/2<0q < q/2 < 0, so q/20q/2 \in 0^\ast and q/2>qq/2 > q; hence no element of 00^\ast is greatest.

givenL1
2.1

By steps 1.1 and 1.2, 00^\ast satisfies (C1)–(C3): it is a Dedekind cut (Dedekind cut), i.e. a real number (The real numbers R\mathbb{R} as Dedekind cuts), with no greatest element.

step 1.1step 1.2
3.1

Thus 00^\ast is a Dedekind cut having no greatest element, directly contradicting the claim; more strongly, "no greatest element" is precisely axiom (C3), which every cut must satisfy, so the claim fails for all cuts and is false.

step 2.1given

Sources