The Open Logic Text — accessible offline edition

Infinite Sets — Explore equations

Infinite Sets

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

Equation and object guide

All 121 stable expressions, 12 formal objects, 39 source references, and 2 disclosed corrections are indexed here.

121 expression records

Expression 1

g∘f:A→g[f[A]]

Conventional reading: g composed with f, from A to the image under g of the image of A under f

Meaning here: This declares the composite g after f as a function from A onto its displayed image g of f of A.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 92, column 26

Expression 3

g(x)=x

Conventional reading: g open parenthesis x close parenthesis equals x

Meaning here: The piecewise function g fixes x when x is outside the closure set F.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 81, column 23

Expression 10

φ(x,c1,…,ck)

Conventional reading: phi open parenthesis x comma c sub one comma and so on comma c sub k close parenthesis

Meaning here: This is the formula phi with distinguished variable x and parameters c sub one through c sub k.

1 occurrence
  1. Occurrence 1: dedekind-induction.tex, line 53, column 11

Expression 11

A≼B

Conventional reading: A has cardinality no greater than B

Meaning here: An injection exists from A into B, so A has cardinality no greater than B.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 12, column 1

Expression 12

g[B]→B

Conventional reading: from the image of B under g to B

Meaning here: This is the domain-to-codomain part of the inverse map from g of B to B.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 99, column 1

Expression 13

f

Conventional reading: f

Meaning here: The function f in the surrounding closure, restriction, injection, or composition argument.

23 occurrences
  1. Occurrence 1: dedekind-algebra.tex, line 42, column 19
  2. Occurrence 2: dedekind-algebra.tex, line 42, column 39
  3. Occurrence 3: dedekind-algebra.tex, line 48, column 59
  4. Occurrence 4: dedekind-algebra.tex, line 50, column 48
  5. Occurrence 5: dedekind-algebra.tex, line 54, column 19
  6. Occurrence 6: dedekind-algebra.tex, line 57, column 59
  7. Occurrence 7: dedekind-algebra.tex, line 58, column 44
  8. Occurrence 8: dedekind-algebra.tex, line 64, column 33
  9. Occurrence 9: dedekind-algebra.tex, line 72, column 101
  10. Occurrence 10: dedekind-algebra.tex, line 73, column 1
  11. Occurrence 11: dedekind-algebra.tex, line 86, column 33
  12. Occurrence 12: dedekind-algebra.tex, line 92, column 21
  13. Occurrence 13: dedekind-algebra.tex, line 115, column 101
  14. Occurrence 14: dedekind-algebra.tex, line 115, column 220
  15. Occurrence 15: card-sb.tex, line 31, column 31
  16. Occurrence 16: card-sb.tex, line 32, column 41
  17. Occurrence 17: card-sb.tex, line 36, column 19
  18. Occurrence 18: card-sb.tex, line 39, column 59
  19. Occurrence 19: card-sb.tex, line 40, column 44
  20. Occurrence 20: card-sb.tex, line 72, column 35
  21. Occurrence 21: card-sb.tex, line 77, column 7
  22. Occurrence 22: card-sb.tex, line 82, column 62
  23. Occurrence 23: card-sb.tex, line 94, column 1

Expression 18

x=g(x)=g(y)=y

Conventional reading: x equals g open parenthesis x close parenthesis equals g open parenthesis y close parenthesis equals y

Meaning here: When x and y are outside F, the definition makes g fix both, so equality of their g-values yields x equals y.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 77, column 56

Expression 19

g(x)={f(x)if x∈Fxotherwise

Conventional reading: g of x equals f of x if x is in F, and equals x otherwise

Meaning here: The function g agrees with f on F and is the identity outside F.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 59, column 1

Expression 25

∀v1…∀vk((φ(o,v1,…,vk)∧(∀x∈N)(φ(x,v1,…,vk)→φ(s(x),v1,…,vk)))→(∀x∈N)φ(x,v1,…,vk))

Conventional reading: for every v sub one through v sub k: if phi of o, with those parameters, holds, and for every x in N, phi of x, with those parameters, implies phi of s of x, with those parameters, then for every x in N, phi of x, with those parameters, holds

Meaning here: This is the fully quantified induction schema with free parameters displayed: the base case and successor step imply the property for every x in N.

1 occurrence
  1. Occurrence 1: dedekind-induction.tex, line 57, column 2

Expression 26

g[f[A]]⊆g[B]⊆A

Conventional reading: the image under g of the image of A under f is a subset of the image of B under g, which is a subset of A

Meaning here: The image g of f of A is contained in g of B, and g of B is contained in A.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 91, column 27

Expression 35

clof(o)=⋂{X:o∈X and X is f-closed}

Conventional reading: the closure of o under f equals the intersection of all sets X such that o is in X and X is f closed

Meaning here: This defines the closure of o under f as the intersection of every f-closed set that contains o.

1 occurrence
  1. Occurrence 1: dedekind-algebra.tex, line 44, column 2

Expression 37

ran(f)∪{o}

Conventional reading: the range of f union the singleton containing o

Meaning here: The union of the range of f with the singleton containing o, an f-closed set containing o.

1 occurrence
  1. Occurrence 1: dedekind-algebra.tex, line 64, column 81

Expression 38

A

Conventional reading: A

Meaning here: The set A in the surrounding Dedekind-infinite, Dedekind-algebra, or cardinality construction.

8 occurrences
  1. Occurrence 1: hilberts-hotel.tex, line 61, column 7
  2. Occurrence 2: hilberts-hotel.tex, line 62, column 6
  3. Occurrence 3: hilberts-hotel.tex, line 62, column 32
  4. Occurrence 4: dedekind-algebra.tex, line 82, column 36
  5. Occurrence 5: dedekind-algebra.tex, line 92, column 1
  6. Occurrence 6: dedekind-algebra.tex, line 105, column 55
  7. Occurrence 7: dedekind-algebra.tex, line 115, column 63
  8. Occurrence 8: dedekind-algebra.tex, line 115, column 94

Expression 40

g[f[A]]≈A

Conventional reading: the image under g of the image of A under f is equinumerous with A

Meaning here: The composite image g of f of A has the same cardinality as A.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 96, column 1

Expression 47

B⊆Clof(B)

Conventional reading: B is a subset of the closure of B under f

Meaning here: The generating set B is contained in its closure under f.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 38, column 33

Expression 51

f(x)=g(x)=g(y)=f(y)

Conventional reading: f of x equals g of x, which equals g of y, which equals f of y

Meaning here: On F, g agrees with f; equality of g of x and g of y therefore gives equality of f of x and f of y.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 76, column 23

Expression 52

Clof(B)⊆X

Conventional reading: the closure of B under f is a subset of X

Meaning here: The closure of B under f is contained in every f-closed set X containing B.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 41, column 22

Expression 57

F=Clof(C∖B)

Conventional reading: F equals the closure under f of the set difference C minus B

Meaning here: F is the closure under f of those elements of C that are not in B.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 56, column 47

Expression 61

φ(x,v1,…,vk)

Conventional reading: phi open parenthesis x comma v sub one comma and so on comma v sub k close parenthesis

Meaning here: The formula phi with variable x and the displayed free variables v sub one through v sub k.

1 occurrence
  1. Occurrence 1: dedekind-induction.tex, line 55, column 9

Expression 68

h[D]={h(x):x∈D}

Conventional reading: the image of D under h equals the set of all h of x such that x is in D

Meaning here: This defines the image of D under h as the set of values h of x for x in D.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 86, column 37

Expression 76

Clof(B)=⋂{X:B⊆X and X is f-closed}

Conventional reading: the closure of B under f equals the intersection of all sets X such that B is a subset of X and X is f closed

Meaning here: This defines the closure of B under f as the intersection of all f-closed supersets of B.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 27, column 1

Expression 77

g(y)=f(y)=x

Conventional reading: g open parenthesis y close parenthesis equals f open parenthesis y close parenthesis equals x

Meaning here: For the chosen y in F, g of y equals f of y, and this common value is x.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 82, column 149

Expression 81

y=g(y)=g(x)=f(x)

Conventional reading: y equals g of y, which equals g of x, which equals f of x

Meaning here: If g of x equaled g of y across the two cases, the definitions would force y, g of y, g of x, and f of x to be equal.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 71, column 48

Expression 87

g(x)=g(y)

Conventional reading: g open parenthesis x close parenthesis equals g open parenthesis y close parenthesis

Meaning here: The two inputs x and y have equal g-values.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 75, column 13

Expression 88

g−1∘h:A→B

Conventional reading: g inverse composed with h, from A to B

Meaning here: The composite first applies h and then g inverse, producing a bijection from A to B.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 99, column 29

Expression 93

f(x)∈clof(o)

Conventional reading: f open parenthesis x close parenthesis is an element of the closure of o under f

Meaning here: The f-image of x belongs to the closure generated by o.

1 occurrence
  1. Occurrence 1: dedekind-algebra.tex, line 73, column 16

Expression 94

∀x∀y(s(x)=s(y)→x=y)

Conventional reading: for every x and every y, if s of x equals s of y, then x equals y

Meaning here: The successor function s is injective: equal successor values imply equal inputs.

1 occurrence
  1. Occurrence 1: dedekind-algebra.tex, line 25, column 10

Expression 95

A≈B and B≈C

Conventional reading: A is equinumerous with B, and B is equinumerous with C

Meaning here: The intended conclusion is that A, B, and C all have the same cardinality. The immutable source nests a binary equinumerosity macro incorrectly; the reader exposes the intended two equalities.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 52, column 56

Expression 98

y=f(x)∈F

Conventional reading: y equals f open parenthesis x close parenthesis is an element of F

Meaning here: The common element y equals f of x and belongs to F.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 73, column 9

Expression 109

g∘f−1:A→B

Conventional reading: g composed with f inverse, from A to B

Meaning here: The composite first applies f inverse and then g, giving a bijection from A to B in the helper proof.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 67, column 18

Expression 111

a+o=aa×o=oao=s(o)a+s(b)=s(a+b)a×s(b)=(a×b)+aas(b)=ab×a

Conventional reading: six recursive arithmetic clauses: a plus o equals a; a times o equals o; a to the power o equals s of o; a plus s of b equals s of the sum a plus b; a times s of b equals a times b plus a; and a to the power s of b equals a to the power b times a

Meaning here: These six recursion equations define addition, multiplication, and exponentiation from the successor structure of a Dedekind algebra.

1 occurrence
  1. Occurrence 1: dedekind-induction.tex, line 76, column 1

Expression 114

B≼A

Conventional reading: B has cardinality no greater than A

Meaning here: An injection exists from B into A, so B has cardinality no greater than A.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 12, column 21

Expression 115

g(x)≠g(y)

Conventional reading: g open parenthesis x close parenthesis is not equal to g open parenthesis y close parenthesis

Meaning here: The values g of x and g of y are unequal.

1 occurrence
  1. Occurrence 1: card-sb.tex, line 70, column 55

Expression 119

(∀n∈N)(φ(n)→φ(s(n)))

Conventional reading: for every n in N, if phi of n holds then phi of s of n holds

Meaning here: For every n in N, the induction property passes from n to its successor s of n.

1 occurrence
  1. Occurrence 1: dedekind-induction.tex, line 41, column 19

Expression 121

(∀n∈N)(n∈X→s(n)∈X)

Conventional reading: for every n in N, if n is in X then s of n is in X

Meaning here: For every n in N, membership of n in X implies membership of its successor in X.

1 occurrence
  1. Occurrence 1: dedekind-induction.tex, line 25, column 29

One diagram

Hilbert's Hotel room-shift diagram

Nine numbered guests are shown moving from room n to room n plus one, leaving room one empty; ellipses indicate the infinite continuation.

Words-only linearization: Diagram. Guests one through nine occupy correspondingly numbered rooms. Each guest moves from room n to room n plus one. Room one is left free for a new guest, and ellipses show that the shift continues through all numbered rooms.

Open in reading context.

12 formal objects

  1. Hilbert's Hotel room-shift diagram — hilberts-hotel.tex, line 32.
  2. Definition of a Dedekind-infinite set — hilberts-hotel.tex, line 60.
  3. Definition of closure under a function — dedekind-algebra.tex, line 41.
  4. Lemma on closure properties — dedekind-algebra.tex, line 53.
  5. Definition of a Dedekind algebra — dedekind-algebra.tex, line 81.
  6. Theorem producing a Dedekind algebra — dedekind-algebra.tex, line 98.
  7. Arithmetical induction theorem for Dedekind algebras — dedekind-induction.tex, line 16.
  8. Formula induction schema for Dedekind algebras — dedekind-induction.tex, line 37.
  9. Fully quantified induction schema with parameters — dedekind-induction.tex, line 57.
  10. Recursive clauses for arithmetic operations — dedekind-induction.tex, line 76.
  11. Lemma on closure of a set under a function — card-sb.tex, line 35.
  12. Sandwich proposition for equinumerous sets — card-sb.tex, line 51.

39 resolved source references

  1. David Hilbert 2013, 730 — hilberts-hotel.tex, line 52.
  2. 1888 — hilberts-hotel.tex, line 58.
  3. condition three, repeated application of the successor function — dedekind-algebra.tex, line 30.
  4. three, repeated application of the successor function — dedekind-algebra.tex, line 32.
  5. the closure-contains-o clause — dedekind-algebra.tex, line 67.
  6. the least-closure clause — dedekind-algebra.tex, line 67.
  7. the closure-contains-o clause — dedekind-algebra.tex, line 69.
  8. the closure-is-f-closed clause — dedekind-algebra.tex, line 72.
  9. the least-closure clause — dedekind-algebra.tex, line 75.
  10. placing o outside the range — dedekind-algebra.tex, line 94.
  11. requiring f to be injective — dedekind-algebra.tex, line 94.
  12. the lemma on closure properties — dedekind-algebra.tex, line 105.
  13. the clause placing o outside the range — dedekind-algebra.tex, line 109.
  14. the injection clause — dedekind-algebra.tex, line 112.
  15. the closure-generates-A clause — dedekind-algebra.tex, line 115.
  16. the lemma on closure properties — dedekind-algebra.tex, line 115.
  17. the lemma on closure properties — dedekind-algebra.tex, line 115.
  18. the lemma on closure properties — dedekind-algebra.tex, line 115.
  19. the arithmetical induction theorem — dedekind-induction.tex, line 33.
  20. the arithmetical induction theorem — dedekind-induction.tex, line 48.
  21. the Set Theory part — dedekind-induction.tex, line 63.
  22. the Ordinal Arithmetic chapter — dedekind-induction.tex, line 72.
  23. Michael Potter 2004, pp. 95–8 — dedekind-induction.tex, line 73.
  24. the reflections section of Arithmetization — dedekinds-proof.tex, line 16.
  25. the Arithmetization chapter — dedekinds-proof.tex, line 21.
  26. the reflections section of Arithmetization — dedekinds-proof.tex, line 30.
  27. 1888, Theorems 132–3 — dedekinds-proof.tex, line 38.
  28. (Richard Dedekind, 1888, preface) — dedekinds-proof.tex, line 57.
  29. the Arithmetization chapter — dedekinds-proof.tex, line 61.
  30. the theorem that a Dedekind-infinite set yields a Dedekind algebra — dedekinds-proof.tex, line 69.
  31. (Richard Dedekind, 1888, §66) — dedekinds-proof.tex, line 82.
  32. Michael Potter (2004), p. 23 — dedekinds-proof.tex, line 103.
  33. the Schröder-Bernstein theorem in Size of Sets — card-sb.tex, line 11.
  34. Michael Potter (2004), pp. 157–8 — card-sb.tex, line 19.
  35. the definition of closure generated from one element — card-sb.tex, line 25.
  36. the lemma on closure properties — card-sb.tex, line 46.
  37. the lemma on closure of a set under a function — card-sb.tex, line 72.
  38. the lemma on closure of a set under a function — card-sb.tex, line 82.
  39. the sandwich proposition for equinumerous sets — card-sb.tex, line 97.

2 disclosed reader corrections

  1. TR007-SOURCE-FORMULA-002: The source nests a binary equinumerosity macro, syntactically comparing the proposition A is equinumerous with B to C. The reader preserves that printed source separately and states the sandwich proposition's intended conclusion: A is equinumerous with B and B is equinumerous with C.
  2. TR007-SOURCE-PROSE-001: The reader removes the stray word 'be' from the immutable source phrase 'must be characterize.'