Title: Theory / Unimportant / Math / Logic / Set Theory / Kunen / V2+8
Tags: 2ed fromMath mathToDef hasSeenConjDef toBinaryRelation closed mathToSee Ed2 typToBinary counterExample effectToImplementation examplesSwitchExample1 toBinaryFunction

Smaller0: \(S\vdash\phi\)
Greater0: \(S\cup\{\neg\phi\}\)
Page: 3
Chapter: 0
Section: 2
Variables: \(\phi\) be a formula.
Smaller to greater: iff
Greater1: inconsistent
Connect Greater0: is

Name: Finitism
Definition: The notion of an infinite set is a fiction.
Page: 5
Chapter: I
Section: 1

Name: Platonism
Definition: The Abstract mathematical statements have an absolute meaning in some ideal universe and their truth is independent of us or what we think about them.
Page: 6
Chapter: I
Section: 1

Name: Formalism
Definition: The theory asserting that what is "really true" is elementary finitistic reasoning.
Page: 6
Chapter: I
Section: 1
Typ: metatheory

Smaller0: \(F\) is finitistic
Greater0: formalized and proved
Page: 9, 19
Chapter: I
Section: 1.1, 3
Variables: \(F\) a fact
Index: 2
Kind: Thesis
Hide middle: yes
Prefix Greater: \(F\) can be
Greater1: ZFC and BST^-
Connect Greater0: within

Name: And
Page: 11
Chapter: 1
Section: 2
Notation: \(\land\)

Name: existential quantifier
Page: 11
Chapter: 1
Section: 2
Notation: \(\exists\)

Name: not
Page: 11
Chapter: 1
Section: 2
Notation: \(\neg\)

Name: Equality
Page: 11
Chapter: 1
Section: 2
Notation: \(=\)

Name: variables
Page: 11
Chapter: 1
Section: 2
Denoted by: \(v_0,v_1,\dots\)

Name: A formula
Definition: An expression constructed by the rules \(v_i\in v_j\), \(v_i=v_j\), \((\phi)\land(\psi)\), \(\neg(\phi)\) and \(\exists v_i(\phi)\) for any natural \(i,j\) and formulas \(\phi,\psi\).
Page: 11
Chapter: 1
Section: 2

Name: universall quantifier
Page: 11
Chapter: 1
Section: 2
Notation: \(\forall\)

Name: Or
Page: 11
Chapter: 1
Section: 2
Notation: \(\lor\)

Name: Implies
Page: 11
Chapter: 1
Section: 2
Notation: \(\implies\)

Name: If and only if
Page: 11
Chapter: 1
Section: 2
Notation: \(\iff\)

Definition: \(((\phi)\implies(\psi))\land((\psi)\implies(\phi))\).
Page: 11
Chapter: 1
Section: 2
Notation: \((\phi)\iff(\psi)\)

Name: Its universal closure
Definition: A sentence obtained by universally quantifying all free variables of \(\phi\).
Page: 11
Chapter: 1
Section: 2
Variables: \(\phi\) be a formula.

Definition: \(\neg(\phi)\lor(\psi)\).
Page: 11
Chapter: 1
Section: 2
Notation: \((\phi)\implies(\psi)\)

Definition: \(\neg(\neg(\phi))\land(\neg(\psi))\).
Page: 11
Chapter: 1
Section: 2
Notation: \((\phi)\lor(\psi)\)

Definition: There is a formal proof of a contradiction from \(\Gamma\).
Page: 11
Chapter: I
Section: 2
Variables: \(\Gamma\) a set of sentence
Notation: \(\text{Incon}(\Gamma)\)
Index: 1
Kind: Def

Definition: \(\neg\text{Incon}(\Gamma)\).
Page: 11
Chapter: I
Section: 2
Variables: \(\Gamma\) a set of sentence
Context: Set theory
Notation: \(\text{Con}(\Gamma)\)
Index: 1
Kind: Def

Question: The basic symbols of the formal language are
Answer: \(\land,\neg,\exists,(,),\in,=\) and \(v_j\) for each natural number \(j\).
Page: 11
Chapter: 1
Section: 2

Name: Formal logic
Definition: A language with precisely defined rules of formation
Page: 11
Chapter: I
Section: 2

Name: logical symbols
Definition: Connectives \(\land,\lor,\neg,\implies{},\iff{}\)
Page: 11
Chapter: I
Section: 2
Definition2: quantifiers \(\forall,\exists\)
Conjdef: Either
Definition3: variables

Name: nonlogical symbols
Definition: an arity (a non-negative integer)
Page: 11
Chapter: I
Section: 2
Definition2: a type (predicate or function)
Conjdef: A symbol with

Name: A term in Polish notation
Definition: an atomic term
Page: 11
Chapter: I
Section: 2
Definition2: an \(n\)-ary symbol, followed by \(n\) terms without any separator nor parenthesis
Conjdef: Either
Name2: A term in prefix notation

Name: A set of nonlogical symbols
Page: 11
Chapter: I
Section: 2
Denoted by: \(\mathcal L\)

Name: Lexicon
Definition: A set of nonlogical symbols, with types and arities
Page: 11
Chapter: I
Section: 2
Name2: Signature

Name: Predicate logic
Definition: Logic based on Boolean combination of boolean predicate
Page: 11
Chapter: I
Section: 2
Intuition: A logic for developing formal axiomatic theories

Question: Why is syntax important in logic ?
Answer: For formal definition only, not for learning
Page: 12
Chapter: I
Section: 2

Name: Membership
Page: 12
Chapter: 1
Section: 2
Notation: \(\in\)

Name: An extension by definitions of \(\Gamma\)
Definition: A set of symbols \(\mathcal L'\supseteq \mathcal L\) and a set of sentences \(\Gamma\cup\{\delta_s:s\in\mathcal L'\setminus \mathcal L\}\) with \(\delta_s\) a definition of \(s\) over \(\mathcal L\).
Page: 12
Chapter: I
Section: 2
Variables: \(\mathcal L\) a set of symbols,
\(\Gamma\) a set of sentence
Kind: Def

Smaller0: \(\Gamma\vdash\phi\)
Greater0: \(\Gamma'\vdash\phi\)
Page: 13
Chapter: I
Section: 2
Variables: \(\mathcal L\supseteq \mathcal L'\) sets of symbols,
\(\Gamma\) a set of sentence
\(\Gamma'\) in \(\mathcal L'\) an extension by definitions of \(\Gamma\)
\(\phi\in\mathcal L\)
Index: 3
Kind: Theo
Smaller to greater: iff

Definition: A \(\mathcal L\)-formula which is \(\Gamma\)-equivalent to \(\phi\)
Page: 13
Chapter: I
Section: 2
Variables: \(\mathcal L\supseteq \mathcal L'\) sets of symbols,
\(\Gamma\) a set of sentence
\(\Gamma'\) in \(\mathcal L'\) an extension y definitions of \(\Gamma\)
\(\phi\in\mathcal L'\)
Notation: \(\hat\phi\)
Index: 3
Kind: Theo

Name: A conservative extension of \(S\)
Definition: A superset \(S'\) of \(S\) such that for all sentence \(\phi\) of \(\mathcal L\), with \(S'\vdash\phi\), then \(S\vdash \phi\).
Page: 13
Chapter: 1
Section: 2
Variables: \(\mathcal L\) be a set of symbols
\(S\) be a set of sentences over \(\mathcal L\)
\(S'\) in \(\mathcal L'\) be an extension by definitions of \(S\) in \(\mathcal L\).
Index: 3
Kind: Theorem

Definition: \(\forall x(x\in A\implies x\in B)\)
Page: 12, 17
Chapter: 1
Section: 2, 3
Variables: \(A,B\) be sets.
Notation: \(A\subset B\)

Name: An extension by definition of \(S\)
Definition: \(\mathcal L'=\mathcal L\cup\{P\}\).
Page: 13
Chapter: 1
Section: 2
Variables: \(\mathcal L\) be a set of symbols
\(S\) be a set of sentences over \(\mathcal L\).
Definition2: \(S'\) being \(S\) with a formula defining \(P\)
Conjdef: The pair

Question: For each formula \(\psi'(x_1,\dots,x_n)\) of \(\mathcal L'\) there is
Answer: a formula \(\psi(x_1,\dots,x_n)\) of \(\mathcal L\) such that \(S'\vdash\forall x_1,\dots,x_n (\psi(x_1,\dots,x_n)\iff \psi'(x_1,\dots,x_n))\).
Page: 13
Chapter: 1
Section: 2
Variables: \(\mathcal L\) be a set of symbols and \(S\) be a set of sentences over \(\mathcal L\).
\(S'\) in \(\mathcal L'\) be an extension by definitions of \(S\) in \(\mathcal L\).
Index: 3
Kind: Theorem

Name: A definition of \(p\) over \(\mathcal L,\Gamma\)
Definition: A sentence of the form \(\forall x_1,\dots,x_n[p(x_1,\dots,x_n)\iff\theta(x_1,\dots,x_n)]\)} where \(\theta\) is a formula of \(\mathcal L\).
Page: 13
Chapter: I
Section: 2
Variables: \(\mathcal L\) a set of symbols,
\(\Gamma\) a set of sentence and
\(p\) an \(n\)-ary predicate symbol not belonging to \(\mathcal L\).
Kind: Def

Name: The intersection of \(A\) and of \(B\)
Definition: \(\bigcap\{A,B\}\)
Page: 14, 21
Chapter: 1
Section: 2, 4
Variables: \(A,B\) be sets.
Notation: \(A\cap B\)
Definition2: \(\{x\in A:x\in B\}\)
Extra: 1st one V1
2nd one V2

Name: Extension by definition
Page: 14
Section: 2
Chapter: I
Index: 4
Kind: Theo
Under: composition.

Definition: the formal encoding of \(i\).
Page: 15
Chapter: 1
Section: 2
Variables: \(i\) a mathematical object
Notation: [$]\text{\textopencorner} i \text{\textcorner}[/$]
Example: [$]\text{\textopencorner} 2 \text{\textcorner}=\{\emptyset,\{\emptyset\}\}[/$]
Example2: [$]\text{\textopencorner} \{a_1,\dots,a_n\} \text{\textcorner}[/$] the constant introduced by [$]\theta_b(y)=\forall x[x\in y\iff \bigvee_{i=1}^nx=\text{\textopencorner} a_i \text{\textcorner}][/$]

Definition: The formula which holds only for [$]x=\text{\textopencorner} b\text{\textcorner}[/$].
Page: 15
Chapter: I
Section: 2
Variables: \(b\) a mathematical object
Notation: \(\theta_b(x)\)

Name: A hereditary set
Definition: A set \(x\) such that for all \(i\in\mathbb N\), the union of elements of ... union (\(i\) times) of elements of \(x\) are sets.
Page: 15
Chapter: 1
Section: 2

Definition: \(\aleph(x)\).
Page: 15
Chapter: I
Section: 2
Variables: \(\aleph\) a function defined on ordinals
\(x\) an ordinal
Notation: \(\aleph_x\)

Question: \(\aleph(x)\) equals
Answer: \(\emptyset\).
Page: 15
Chapter: I
Section: 2
Variables: \(\aleph\) a function defined on a set \(X\)
\(x\not\in X\)

Name: Foundation axiom
Definition: \(\forall x\,\left\{\exists(y\in x)\implies \exists y\left[y\in x\land \neg \exists z\left(z\in x\land z\in y\right)\right]\right\} \) each non empty set contains an element disjoint from it
Page: 16, 32
Chapter: I
Section: 3
Index: 2, 28
Kind: Axiom, Lem
Definition2: \(\in\) is well-founded on \(V\)

Name: Extensionality axiom
Definition: \(\forall x,\forall y(\forall z(z\in x\iff z\in y)\implies x=y)\).
Page: 16, 19
Chapter: I
Section: 3, 4
Index: 1
Kind: Axiom
Intuition: a set is determined by its members

Name: Comprehension scheme
Definition: given a set \(z\) and a definable property, the set of elements of \(z\) satisfying this property exists.
Page: 17, 19
Chapter: I
Section: 3, 4
Notation: \(\{x:x\in z\land \phi\}\)
Index: 3
Kind: Axiom
Definition2: For each formula \(\phi\) with free variables \(x,z,w_1,\dots,w_n\):
\[\forall z\forall w_1,\dots,w_n\exists y\forall x(x\in y\iff x\in z\land \phi) \]
Typ: infinite scheme
Notation2: \(\{x\in z:\phi\}.\)

Name: Pairing axiom
Definition: \(\forall x\forall y\exists z(x\in z\land y\in z)\)
Page: 17, 22
Chapter: Introduction
Section: 3, 4
Index: 4
Kind: Axiom
Intuition: (using extensionality) the set containing both of those elements belongs to the universe of discourse.

Name: Union axiom
Definition: \(\forall\mathcal F\exists A\forall Y\forall x(x\in Y\land Y\in\mathcal F\implies x\in A)\)
for all sets \(\mathcal F\) of the universe, the union of its set is a subset of an element of the universe of discourse.
Page: 17
Chapter: I
Section: 3
Index: 5
Kind: Axiom
Intuition: (using extensionality) the union of elements of \(\mathcal F\) belongs to the universe of discourse.

Name: Infinity axiom
Definition: \(\exists x\left(0\in x\land \forall y\in x(S(y)\in x)\right)\)
Page: 17, 38
Chapter: I
Section: 3, 7
Index: 7, 21
Kind: Axiom
Definition2: \(\omega\) is a set
Definition3: Some limit ordinal exists

Name: Power set axiom
Definition: \(\forall x\exists y\forall z(z\subseteq x\implies z\in y).\)
Page: 17
Chapter: I
Section: 3
Index: 8
Kind: Axiom
Abbreviation: PSA

Name: Choice axiom
Definition: \(\forall F\left(\emptyset F\land \forall x,y\in F (x\ne y\implies x\cap y=\emptyset)\right)\implies \exists C\forall x\in F(\text{SING}(C\cap x))\)
Page: 17
Chapter: I
Section: 3
Index: 9
Kind: Axiom
Abbreviation: AC
Extra: def

Definition: X without Power Set
Page: 17
Chapter: Introduction
Section: 3
Variables: X an axiomatic system
Notation: X-P

Definition: X without Foundation
Page: 17
Chapter: Introduction
Section: 3
Variables: X an axiomatic system
Notation: X^-

Page: 17
Section: 3
Chapter: Introduction
Axiom: choice
Name: Zermelo-Frankel with choice
Vocabulary: \(\{\in\}\)
Extends: ZF
Abbreviation: ZFC
French: Zermelo-Frankel avec choix

Page: 17
Section: 3
Chapter: Introduction
Axiom: AC
Name: Zermelo with choice
Vocabulary: \(\{\in\}\)
Extends: Z
Extra: Set existence in V1
Abbreviation: ZC

Page: 17
Section: 3
Chapter: Introduction
Axiom: Replacement Scheme
Name: Zermelo-Frankel
Vocabulary: \(\{\in\}\)
Extends: Z
Extra: Set existence in V1
Abbreviation: ZF

Definition: \(\forall a(a\in z\iff (a\in x\land a\in y))\).
Page: 17, 20
Chapter: I
Section: 3, 4
Notation: \(x\cap y=z\)

Definition: \(\forall z(z\not\in x)\).
Page: 17
Chapter: I
Section: 3
Notation: \(x=\emptyset\)

Definition: \(\exists y\in x\forall z\in x(z=y)\).
Page: 17
Chapter: I
Section: 3
Notation: \(\text{SING}(x)\)

Page: 17
Section: 3
Chapter: Introduction
Axiom: Power Set
Name: Zermelo
Vocabulary: \(\{\in\}\)
Extends: BST
Axiom2: Infinity
Extra: Set existence in V1
Abbreviation: Z
Context: Set theory

Definition: \(\forall z. z\in y\implies z=x\lor z\in x\)
Page: 17
Chapter: I
Section: 3
Variables: \(x,y\) sets
Notation: \(y=S(x)\)
Kind: Theo

Definition: \(X\) with the Axiom of Infinity deleted
Page: 17
Chapter: I
Section: 3
Variables: \(X\) a theory
Notation: \(X-Inf\)

Name: Replacement scheme
Definition: For each formula \(\phi\) with free variables \(x,z,A,w_1,\dots,w_n\):
\(\forall A\forall w_1,\dots,w_n\left[\forall x\in A \exists ! y\phi\implies\exists Y\forall x\in A\exists y\in Y\phi\right].\)
Page: 17, 25
Chapter: 1
Section: 3
Index: 6
Kind: Axiom
Intuition: The image of a definable function is a set
Typ: Infinite scheme

Page: 18
Section: 3
Chapter: I
Axiom: PSA or Replacement
Name: Basic Set Theory^-
Vocabulary: \(\{\in\}\)
Axiom2: Union
Axiom3: Pairing
Extra: doublon
Abbreviation: BST^-
Axiom4: Comprehension
Axiom5: Extensionality

Page: 18
Section: 3
Chapter: I
Axiom: Foundation
Name: Basic Set Theory
Vocabulary: \(\{\in\}\)
Extends: BST^-
Abbreviation: BST

Name: The set of hereditarily finite sets
Page: 18
Chapter: I
Section: 3
Notation: \(HF\)
Notation2: \(H(\aleph_0)\)
Notation3: \(R(\omega)\)

Definition: The axiom that every set can be well-ordered.
Page: 19
Chapter: I
Section: 3
Context: Kunen's set theory
Notation: AC^+

Definition: \(\{x:x\in v\land\phi(x)\}\)
Page: 20
Chapter: I
Section: 4
Variables: \(\phi(x)\) a formula with one free variable
Notation: \(\{x\in v:\phi (x)\}\)
Kind: Not

Name: A class
Definition: A collection of set defined by a formula
Page: 20
Chapter: 1
Section: 4
Context: set theory
Kind: not

Name: A proper class
Definition: A collection of set which is not a set, defined by a formula
Page: 20
Chapter: 1
Section: 4
Kind: Not

Question: The number of set \(A\) such that \(\forall x[x\in A\iff\phi(x)]\) is
Answer: at most one.
Page: 20
Chapter: I
Section: 4
Variables: \(\phi(x)\) a formula with one free variable

Definition: \(\{x:x=x\}\),
Page: 21
Chapter: 1
Section: 4
Notation: \(V\)
Kind: Def
Typ: A proper class

Definition: \(\{x\in v:x\not\in w\}\)
Page: 21
Chapter: I
Section: 4
Variables: \(v,w\) sets
Notation: \(v\setminus w\)
Index: 5
Kind: Def

Definition: \(\{x: x=v\lor x=w\}\)
Page: 22
Chapter: I
Section: 4
Variables: \(v,w\) sets
Context: Set theory formalism
Notation: \(\{v,w\}\)
Index: 11
Kind: Def

Definition: \(\{x:x\not\in x\}\)
Page: 22
Chapter: I
Section: 4
Context: Set theory
Notation: \(R\)
Property: Proper class

Smaller0: ZFC
Greater0: =
Page: 22
Chapter: I
Section: 4
Prefix Greater: \(V\)
Suffix Greater: \(R\)

Definition: \(\{x: x=v\}\)
Page: 22
Chapter: I
Section: 4
Variables: \(v\) sets
Notation: \(\{v\}\)
Index: 11
Kind: Def

Smaller0: \(\langle x,y\rangle=\langle x',y'\rangle\)
Greater0: \(x=x'\) and \(y=y'\)
Page: 22
Chapter: I
Section: 4
Variables: \(x,y,x',y'\) sets
Index: 12
Kind: Lem
Smaller to greater: iff

Name: The ordered pair of \(x\) and \(y\)
Definition: \(\{\{x\},\{x,y\}\}\)
Page: 22
Chapter: 1
Section: 4
Variables: \(x,y\) sets.
Notation: \(\langle x,y\rangle\)
Index: 11
Kind: Def
Definition2: the function sending \(0\) to \(x\) and \(1\) to \(y\)
Conjdef: Either
Notation2: \((x,y)\)

Name: The union of elements of \(\mathcal F\)
Definition: \(\{x:\exists Y\in \mathcal F,x\in Y\}\).
Page: 23
Chapter: 1
Section: 4
Variables: \(\mathcal F\) be a set.
Notation: \(\bigcup\mathcal F\)

Definition: The set of numbers \(0,\dots,n-1\)
Page: 23
Chapter: I
Section: 4
Variables: \(n\) a natural number
Context: Set theory/ordinal
Notation: \(n\)
Index: 13
Kind: Def
Assuming: Union, pairing

Name: The intersection of every elements of \(\mathcal F\)
Definition: \(\{x:\forall Y\in \mathcal F,x\in Y\}\).
Page: 23
Chapter: 1
Section: 4
Variables: \(\mathcal F\) be a set
Notation: \(\bigcap\mathcal F\)
Assuming: \(\mathcal F\) non empty

Name: The union of \(A\) and of \(B\)
Definition: \(\bigcup\{A,B\}\).
Page: 23
Chapter: 1
Section: 4
Variables: \(A,B\) be sets.
Notation: \(A\cup B\)

Name: The successor of \(\alpha\)
Definition: \(\alpha\cup\{\alpha\}\).
Page: 24, 40
Chapter: 1
Section: 4, 8
Variables: \(\alpha\) a set
Notation: \(S(\alpha)\)
Index: 17, 1
Kind: Def, Table
Definition2: \(\alpha+1\) (assuming \(\alpha\) ordinal)

Name: An inductive set
Definition: A set \(x\) such that \(\emptyset \in x\) and \(\forall y\in x (S(y)\in x)\).
Page: 24
Chapter: I
Section: 5
Variables: \(n\) a natural number
Index: 1
Kind: Def

Definition: \(\{y:\forall I[I\text{ is inductive}\implies y\in I]\}\).
Page: 25
Chapter: I
Section: 5
Notation: \(\mathbb N\)
Index: 2
Kind: Def
Assuming: Axiom of infinity

Definition: \(\{\{x\}\mid x\in A\}\)
Page: 25
Chapter: I
Section: 4
Variables: \(A\) a set
Notation: \(A^*\)
Assuming: Power set or replacement scheme

Smaller0: \(X\subseteq\mathbb N\)
Greater0: \(X=\mathbb N\)
Page: 25, 37
Chapter: I
Section: 5, 7
Variables: \(X\) a set
Index: 19
Kind: Theo
Hide middle: yes
Smaller1: \(X\) is inductive
Name: Principle of Ordinary Induction

Name: A total ordering
Definition: A pair \(\langle A,R\rangle\) such that \(R\) totally orders \(A\).
Page: 26
Chapter: 1
Section: 6

Name: A binary relation
Definition: A set \(R\) of ordered pairs.
Page: 26
Chapter: I
Section: 6
Index: 1
Kind: Def

Definition: \(\langle x,y\rangle\not\in R\).
Page: 26
Chapter: I
Section: 6
Variables: \(R\) a binary relation
Notation: \(x\not Ry\)
Index: 1
Kind: Def

Name: A transitive binary relation on \(A\)
Definition: \(\forall x,y,z\in A[ xRy\land yRz\implies xRz]\).
Page: 26
Chapter: I
Section: 6
Index: 2
Kind: Def

Name: An irreflexive binary relation on \(A\)
Definition: \(\forall x\in A[ x\not Rx]\).
Page: 26
Chapter: I
Section: 6
Variables: \(A\) a set
Index: 2
Kind: Def

Name: A reflexive binary relation on \(A\)
Definition: \(\forall x\in A [x Rx]\).
Page: 26
Chapter: I
Section: 6
Index: 2
Kind: Def

Name: A binary function which satisfies trichotomy on \(A\)
Definition: \(\forall xy\in A[xRy\lor yRx\lor x=y]\).
Page: 26
Chapter: I
Section: 6
Index: 2
Kind: Def

Name: A symmetric binary function on \(A\)
Definition: \(\forall xy\in A[xRy\iff yRx]\).
Page: 26
Chapter: I
Section: 6
Index: 2
Kind: Def

Name: partial order
Definition: transitive
Page: 26
Chapter: I
Section: 6
Index: 2
Kind: Def
Definition2: irreflexive
Conjdef: binary relation on \(A\)

Name: A total order on \(A\)
Definition: A partial order on \(A\) which satisfies the trichotomy on \(A\).
Page: 26
Chapter: I
Section: 6
Index: 2
Kind: Def

Page: 26
Definition: The relation on elements \(x,y\) such that \(x Ry\land yRx\)
Chapter: I
Section: 6
Variables: \(R\) a pre-order
Notation: \(\cong\)
Equivalence: An equivalence relation

Name: An equivalence relation on \(A\)
Definition: A reflexive, symmetric and transitive binary relation on \(A\).
Page: 26
Chapter: I
Section: 6
Index: 2
Kind: Def

Name: A pre-order on \(A\)
Definition: Reflexive
Page: 26
Chapter: I
Section: 6
Index: 2
Kind: Def
Definition2: transitive
Conjdef: A binary relation on \(A\)

Definition: \(\langle x,y\rangle\in R\).
Page: 26
Chapter: 1
Section: 6
Variables: \(R\) a binary relation
Notation: \(xRy\)

Name: A partial non-strict order on \(A\)
Definition: a pre-order on \(A\)
Page: 26
Chapter: I
Section: 6
Index: 2
Kind: Def
Definition2: \(\neg\exists xy\in A[xRy\land yRx\land x\ne y]\)
Conjdef: A binary relation \(R\) such that both:

Name: Cartesian product of \(A\) and of \(B\)
Definition: \(\{\langle x,y\rangle:x\in A,y\in B\}\).
Page: 27
Chapter: 1
Section: 6
Variables: \(A,B\) be sets.
Notation: \(A\times B\)
Assuming: BST^-
(Power set or Replacement)

Name: The domain of the relation \(R\)
Definition: \(\{x:\exists y(\langle x,y\rangle\in R)\}\).
Page: 27
Chapter: 1
Section: 6
Kind: Def
Abbreviation: dom(\(R\))
Assuming: Union and comprehension

Name: The restriction of \(f\) to \(C\)
Definition: \(f\cap(C\times B)\)
Page: 27
Chapter: 1
Variables: \(f:A\to B\)
\(C\subseteq A\).
Context: Set theory
Notation: \(f\upharpoonright C\)
Index: 7
Kind: Def
Assuming: Comprehension

Name: The range of a relation
Definition: \(\{y:\exists x(\langle x,y\rangle\in R)\}\).
Page: 27
Chapter: 1
Section: 6
Variables: \(R\) a binary relation.
Notation: ran(\(R\))
Kind: Def
Assuming: Union and comprehension

Name: The identity function on \(A\)
Definition: \(\{(x,x):x\in A\}\).
Page: 27
Chapter: I
Section: 6
Variables: \(A\) a set
Index: 4
Kind: Def
Abbreviation: \(id_A\)
Assuming: BST^- and (Power set or replacement)

Definition: The only \(y\) such that \(xRy\)
Page: 27
Chapter: I
Section: 6
Variables: \(R\) a binary relation
Notation: \(R(x)\)
Index: 3
Kind: Def
Assuming: \(R\) is a function

Definition: \(\bigcup\{^nA:n\in\mathbb N\}\).
Page: 28
Chapter: I
Section: 6
Variables: \(A\) a set
Notation: \(^{<\omega}A\)
Index: 11
Kind: Def
Assuming: BST^- and Axiom of infinity

Definition: The set of functions with domain \(B\) and range a subset of \(A\).
Page: 28
Chapter: 1
Section: 6
Variables: \(A,B\) sets.
Notation: \(^BA\)
Index: 10
Kind: Def
Assuming: BST^- and Power set axiom
Notation2: \(A^B\)

Name: A function
Definition: A binary relation \(f\) such that \(\forall x\in\text{dom}(f)\exists!y\in\text{ran}(f)(\langle x,y\rangle\in f)\).
Page: 28
Chapter: 1
Section: 6
Notation: \(f:\text{dom}(f)\to\text{ran}(f)\)
Index: 8
Kind: Def

Name: \(1-1\) function from \(A\) to \(B\)
Definition: \(f^{-1}\) is a function,
Page: 28
Chapter: 1
Section: 6
Variables: \(A,B\) be sets
\(f:A\to B\)
Notation: \(f:A\hookrightarrow B\)
Definition2: \(\forall x,y\in A[x\ne y\implies f(x)\ne f(y)]\).
Name2: Injection from \(A\) to \(B\)

Name: A function from \(A\) onto \(B\)
Definition: \(ran(f)\) is \(B\).
Page: 28
Chapter: 1
Section: 6
Variables: \(f:A\to B\).
Notation: \(f:A\twoheadrightarrow B\)
Name2: A surjection function from \(A\) to \(B\)

Page: 29
Definition: \(\{\langle y,x\rangle:\exists x(\langle x,y\rangle\in R)\}\).
Chapter: 1
Section: 6
Variables: \(R\) a relation.
Notation: \(R^{-1}\)
Name: The inverse of \(R\)
Kind: Def
Index: 13

Name: A bijection from \(A\) to \(B\)
Definition: A function which is onto and 1-1.
Page: 28
Chapter: 1
Section: 6
Notation: \(A\rightleftarrows B\)
Index: 8
Kind: Def

Name: Their lexicographic product
Definition: \(\{(s,t),(s',t')\in (S\times T)\times (S\times T): s<s'\lor (s=s'\land t\prec t')\).
Page: 29
Chapter: I
Section: 6
Variables: \((S,<), (T,\prec)\) ordered sets
Index: 15
Kind: Def

Name: The class of strict total orders
Page: 29
Section: 6
Chapter: I
Index: 16
Kind: Lem
Under: lexicographic product.

Name: An isomorphism between \(S\) and \(T\)
Definition: A function \(F:S\leftrightarrows T\) such that \(x<y\iff F(x)\prec F(y)\).
Page: 29
Chapter: I
Section: 6
Variables: \((S,<), (T,\prec)\) ordered sets
Index: 17
Kind: Def

Page: 29
Section: 6
Notation: \(R\circ S\)
Variables: \(R,S\) binary relations
Chapter: 1
Definition: \(\{(x,z)\mid \exists y. xRy\land ySz\}\)
Commutative: no
Associative: yes

Name: The image of \(C\) by \(f\)
Definition: \(\{f(x):x\in C\} \).
Page: 29
Chapter: 1
Section: 6
Variables: \(A,B,C\) sets
\(f:A\to B\)
\(C\subseteq A\)
Notation: \(f''C\)
Index: 12
Kind: Def

Page: 29
Definition: There exists an isomorphism from \(A\) to \(B\).
Chapter: 1
Section: 6
Variables: \(A,B\) be sets
\(R,S\) be relations.
Notation: \(\langle A,R\rangle\simeq\langle B,S\rangle\)
Name: \(\langle A,R\rangle\) and \(\langle B,S\rangle\) are isomorphic
Kind: Def
Index: 17

Definition: \(A\precsim B\) and \(A\not\approx B\).
Page: 30
Chapter: 1
Section: 10
Variables: \(A,B\) sets.
Notation: \(A\prec B\)
Index: 18
Kind: Def

Page: 30
Definition: There is a 1-1 function from A into B
Chapter: 1
Section: 6
Variables: \(A,B\) sets.
Notation: \(A\precsim B\)
Kind: Def, Lem
Index: 18, 19
Transitive: Transitive and reflexive

Page: 30, 33
Definition: There is a 1-1 function from A onto B.
Chapter: 1
Section: 6
Variables: \(A,B\) sets.
Notation: \(A\approx B\)
Kind: Def, Lem, Lem
Index: 18, 21, 31
Transitive: Equivalence relation

Name: Equivalence class of \(x\)
Definition: \(\{y: xRy\}\).
Page: 30
Chapter: I
Section: 6
Variables: \(A\) a set
\(X\) an equivalence relation on a set \(A\)
\(x\in A\)
Notation: \([x]\)
Index: 20
Kind: Def
Assuming: BST^- and Comprehension axiom

Definition: \(\{[y]:y\in A\}\).
Page: 30
Chapter: I
Section: 6
Variables: \(X\) an equivalence relation on a set \(A\)
Notation: \(A/R\)
Index: 20
Kind: Def
Assuming: BST^- and Power set or Replacement

Name: An \(R\)-minimal element in \(A\)
Definition: An element \(y\) such that, for all \(z\in A\), \(z\not Ry\).
Page: 30
Chapter: I
Section: 6
Variables: \(X\) a binary relation on a set \(A\)
Index: 21
Kind: Def

Smaller0: \(X\subseteq Y\)
Greater0: \(X\precsim Y\)
Page: 30
Chapter: 1
Section: 6
Variables: \(X,Y\) sets
Kind: Lem

Name: An \(R\)-maximal element in \(A\)
Definition: An element \(y\) such that, for all \(z\in A\), \(y\not Rz\).
Page: 30
Chapter: I
Section: 6
Variables: \(X\) a binary relation on a set \(A\)
Index: 21
Kind: Def

Name: A well-founded order on \(A\)
Definition: A binary relation \(R\) on \(A\) such that for all non-empty \(X\subseteq A\), there is a \(R\)-minimal element in \(X\).
Page: 31
Chapter: I
Section: 6
Variables: A set \(A\)
Index: 21
Kind: Def

Smaller0: \(R\) is well-founded
Greater0: \(R\) is irreflexive
Page: 31
Chapter: I
Section: 6
Variables: \(R\) a binary relation on \(A\)
Index: 22
Kind: Lem
Greater1: \(\neg\exists x,y\in A[xRy\land yRx]\)
Greater2: \(\neg\exists x,y,z\in A[x Ry\land yRz\land zRx]\)

Name: Well orders
Page: 31, 41
Section: 6, 8
Chapter: I
Index: 25, 5
Kind: Lem
Under: lexical prod
Under2: subset

Name: A well-order
Definition: A well founded total ordering.
Page: 31
Chapter: 1
Section: 6
Index: 21
Kind: Def

Name: A successor ordinal
Definition: of the form \(S(\beta)\)
Page: 32, 37
Chapter: 1
Section: 7
Index: 16
Kind: Def
Definition2: cf(\(\alpha\))=1
Conjdef: An ordinal \(\alpha\) such that, equivalently
Extra: Not in the book

Name: \(\phi\) relativised to \(A\)
Definition: the formula \(\phi\) where \(Q x.\psi\) are replaced by \(Q x\in A.\psi\)
Page: 32
Chapter: 1
Section: 6
Variables: \(A\) a class
\(\phi\) a formula
Index: 27
Kind: Not

Page: 33, 35
Definition: \(\{x:x\text{ is an ordinal}\}\).
Chapter: 1
Section: 6,7
Notation: \(\mathbb{ON}\)
Kind: Def, Lem
Index: 1, 8, 11, 12
Transitive: A proper class, transitive, well ordered

Name: Transitive set
Definition: A set \(x\) such that every element of \(x\) is a subset of \(x\).
Page: 34
Chapter: 1
Section: 7
Kind: Def

Name: A (Von Neuman) ordinal
Definition: transitive
Page: 34
Chapter: 1
Section: 7
Variables: \(X\) a set
Index: 2
Kind: Def
Definition2: well ordered by \(\in\)
Conjdef: A set

Smaller0: \(x\) is an ordinal
Greater0: does not belong to
Page: 35
Chapter: 1
Section: 7
Variables: \(x\) a set
Index: 5
Kind: Not
Prefix Greater: \(x\)

Smaller0: \(X\) is transitive
Greater0: \(X\in\mathrm{ON}\)
Page: 36
Chapter: 1
Section: 7
Variables: \(X\) a set
Index: 13
Kind: Lem
Smaller to greater: iff
Smaller1: \(X\subseteq\mathrm{ON}\)

Name: The type of \(\langle A,R\rangle\)
Definition: The unique ordinal \(C\) such that \(\langle A,R\rangle \simeq C\).
Page: 39, 41
Chapter: 1
Section: 8
Variables: \(\langle A,R\rangle\) a well-ordering.
Notation: \(\text{Type}(\langle A,R\rangle)\) (sometime omitting \(A\) or \(R\))
Index: 3
Kind: Theo, Def
Assuming: ZF

Definition: \(\bigcup X\)
Page: 36
Chapter: 1
Section: 7
Variables: \(X\) a set of ordinals.
Notation: \(\text{sup}(Y)\)
Index: 14
Kind: Lem

Definition: \(\bigcap X\).
Page: 36
Chapter: 1
Section: 7
Variables: \(X\) a set of ordinals.
Notation: \(\text{min}(Y)\)
Index: 14
Kind: Lem

Definition: \(\alpha\subseteq\beta\)
Page: 36, 40
Chapter: 1
Section: 7, 8
Variables: \(\alpha,\beta\) ordinals
Notation: \(\alpha\le\beta\)
Index: 10
Kind: Lem
Definition2: there exists a unique \(\gamma\) such that \(\alpha+\gamma=\beta\)
Assuming: ZF

Definition: \(\alpha\in\beta\)
Page: 36, 40
Chapter: 1
Section: 7, 8
Variables: \(\alpha,\beta\) ordinals
Notation: \(\alpha<\beta\)
Index: 10
Kind: Lem
Assuming: ZF

Name: A limit ordinal
Definition: An ordinal distinct from 0 and not a successor ordinal.
Page: 37
Chapter: 1
Section: 7
Variables: \(\alpha\) an ordinal
Index: 16
Kind: Def

Name: A natural number
Definition: An ordinal \(\alpha\) such that for all \(\beta\le \alpha\), \(\beta=0\) or \(\beta\) is a successor.
Page: 37
Chapter: 1
Section: 7
Variables: \(\alpha\) an ordinal
Index: 16
Kind: Def

Smaller0: \(\gamma
Greater0: \(\gamma\le\alpha\)
Page: 37
Chapter: 1
Section: 7
Variables: \(\alpha,\gamma\) ordinals
Index: 15
Kind: Lem
Smaller to greater: iff
Extra: Missing part is probably \(\gamma\subseteq \alpha\)

Name: Ordinal which are natural numbers
Page: 37
Section: 7
Chapter: 1
Index: 17
Kind: Lem
Under: successor function

Smaller0: \(S(y)\)
Greater0: \(y\)
Page: 37
Chapter: 1
Section: 7
Index: 20
Kind: Lem
Smaller to greater: \(\not\preceq\)
Greater to smaller: \(\not\succeq\)
Hide sides: yes

Name: A finite set
Definition: A set \(x\) such that \(x\preceq n\) for some natural \(n\)
Page: 38
Chapter: 1
Section: 7
Index: 22
Kind: Def

Name: An infinite set
Definition: A set which is not finite
Page: 38
Chapter: 1
Section: 7
Index: 22
Kind: Def

Name: The length of \(F\)
Definition: \(\text{dom}(F)\).
Page: 38
Chapter: I
Section: 6
Variables: \(F\) a sequence
Notation: \(\text{lh}(F)\)
Index: 24
Kind: Def

Smaller0: \(x\) is finite
Greater0: \(x\) is a natural number
Page: 38
Chapter: 1
Section: 7
Variables: \(x\) a set
Index: 23
Kind: Lem
Smaller to greater: iff
Assuming: \(x\) is an ordinal

Name: A sequence
Definition: A function whose domain is an ordinal
Page: 38
Chapter: 1
Section: 7
Context: set theory
Index: 24
Kind: Lem
Denoted by: \(F\)

Definition: \(F\cup\{(\text{lh} F,b)\}\)
Page: 38
Chapter: 1
Section: 7
Variables: \(F\) a sequence,
\(b\) a set
Notation: \(F\frown b\)
Index: 24
Kind: Def
Cardinal: A sequence of length \(\text{lh}F+1\)

Smaller0: \(f\) is an isomorphism
Greater0: \(\alpha=\beta\)
Page: 39
Chapter: 1
Section: 8
Variables: \(\alpha,\beta\) ordinals
\(f:\alpha\to\beta\)
Kind: Lem
Smaller to greater: iff
Assuming: \(f\) surjective
Greatest: \(f\) is identity

Smaller0: \(\alpha+(\beta+\gamma)\)
Greater0: \((\alpha+\beta)+\gamma\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta,\gamma\) sets
Kind: Table
Smaller to greater: =
Hide middle: yes
Assuming: ZF
Name: Associative law

Smaller0: \(\alpha+S(\beta)\)
Greater0: \(S(\alpha+\beta)\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta\) sets
Kind: Table
Smaller to greater: =
Hide middle: yes
Assuming: ZF

Smaller0: \(\text{sup}\{\alpha^\xi:\xi<\beta\} \)
Greater0: \((\alpha^\beta)\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta\) sets
Kind: Table
Smaller to greater: \(=\)
Assuming: ZF, \(\beta\) is a limit ordinal

Smaller0: \(\text{sup}\{\alpha+\xi:\xi<\beta\} \)
Greater0: \((\alpha+\beta)\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta\) sets
Kind: Table
Smaller to greater: \(=\)
Assuming: ZF, \(\beta\) is a limit ordinal

Question: \((0+\alpha)=\)
Answer: \(\alpha\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha\) sets
Kind: Table
Assuming: ZF

Smaller0: \(\alpha\cdot(\beta+\gamma)\)
Greater0: \((\alpha\cdot\beta)+(\alpha\cdot\gamma)\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta,\gamma\) sets
Kind: Table
Smaller to greater: =
Assuming: ZF
Name: Left distributive law

Smaller0: \(\alpha\cdot S(\beta)\)
Greater0: \(\alpha\cdot\beta+\alpha\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta\) sets
Kind: Table
Smaller to greater: =
Hide middle: yes

Smaller0: \((\alpha\cdot\beta)\)
Greater0: \(\text{sup}\{\alpha\cdot\xi:\xi<\beta\} \)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta\) sets
Kind: Table
Smaller to greater: =
Hide middle: yes
Assuming: ZF, \(\beta\) is a limit ordinal

Question: \((\alpha\cdot0)\)
Answer: equals \(0\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha\) a set
Kind: Table
Assuming: ZF

Question: \(\alpha\cdot1\)
Answer: \(\alpha\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha\) a set
Kind: Table

Question: \((\alpha+0)=\)
Answer: \(\alpha\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha\) sets
Kind: Table
Assuming: ZF

Smaller0: \(\alpha\cdot(\beta\cdot\gamma)\)
Greater0: \((\alpha\cdot\beta)\cdot\gamma\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta,\gamma\) sets
Kind: Table
Smaller to greater: =
Assuming: ZF
Name: Associative law

Name: Hereditarily finite sets
Definition: The sets that can be displayed explicitely as finite expression using \(\{,\}\)
Page: 18
Chapter: I
Section: 3

Question: \(1+\omega\) equals
Answer: \(\omega\)
Page: 40
Chapter: 1
Section: 8
Kind: Table

Question: \(\omega+1\)
Answer: \(>\omega=1+\omega\)
Page: 40
Chapter: 1
Section: 8
Kind: Table

Question: \(2\cdot\omega\)
Answer: \(=\omega\)
Page: 40
Chapter: 1
Section: 8
Kind: Table

Question: \(\omega\cdot2\)
Answer: \(>\omega\)
Page: 40
Chapter: 1
Section: 8
Kind: Table

Smaller0: \((1+1)\cdot\omega\)
Greater0: \(1\cdot\omega+1\cdot\omega\)
Page: 40
Chapter: 1
Section: 8
Kind: Table
Smaller to greater: <
Greater to smaller: >
Hide sides: yes

Question: \(\alpha\cdot0\)
Answer: \(0\)
Page: 40
Chapter: 1
Section: 8
Kind: Table

Question: \(0\cdot\alpha\)
Answer: \(0\)
Page: 40
Chapter: 1
Section: 8
Kind: Table

Question: \(1\cdot\alpha\)
Answer: \(\alpha\)
Page: 40
Chapter: 1
Section: 8
Kind: Table

Question: \(\alpha\cdot1\)
Answer: \(\alpha\)
Page: 40
Chapter: 1
Section: 8
Kind: Table

Question: \(\alpha^1\)
Answer: equals \(\alpha\)
Page: 40
Chapter: 1
Section: 8
Kind: Table

Question: \(\alpha^0\)
Answer: equals \(1\)
Page: 40
Chapter: 1
Section: 8
Kind: Table

Question: \(1^\alpha\)
Answer: equals \(1\)
Page: 40
Chapter: 1
Section: 8
Kind: Table

Question: \(0^\alpha\)
Answer: equals \(0\)
Page: 40
Chapter: 1
Section: 8
Kind: Table
Assuming: \(\alpha>0\)

Smaller0: \(\alpha+\beta=\alpha+\gamma\)
Greater0: \(\beta=\gamma\)
Page: 40
Chapter: 1
Section: 8
Kind: Table
Smaller to greater: iff

Smaller0: \(\alpha\cdot\beta=\alpha\cdot\gamma\)
Greater0: \(\beta=\gamma\)
Page: 40
Chapter: 1
Section: 8
Kind: Table
Smaller to greater: iff
Assuming: \(\alpha\ne0\)

Smaller0: \(1\cdot\omega\)
Greater0: \(2\cdot\omega\)
Page: 40
Chapter: 1
Section: 8
Kind: Table
Smaller to greater: =
Hide sides: yes

Smaller0: \(1+\omega\)
Greater0: \(2+\omega\)
Page: 40
Chapter: 1
Section: 8
Kind: Table
Smaller to greater: =
Hide sides: yes

Smaller0: \(\alpha^{\beta\cdot\gamma}\)
Greater0: \((\alpha^{\beta})^\gamma\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta,\gamma\) ordinals
Kind: Table
Smaller to greater: =
Hide sides: yes

Smaller0: \(\alpha>0\)
Greater0: \(\beta=\alpha\cdot \gamma+\delta\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta\) ordinals
Kind: Table
Prefix Greater: there exists unique \(\gamma,\delta\) such that
Name: division
Greater1: \(\delta<\alpha\)

Smaller0: \(\alpha>1\)
Greater0: \(\beta=\alpha^\delta\cdot\xi+\gamma\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta\) ordinals
Kind: Table
Prefix Greater: there exists unique \(\gamma,\delta,\xi\) such that
Smaller1: \(\beta>0\)
Name: logarithm
Greater1: \(\xi<\alpha\)
Context: Ordinals
Greater2: \(\gamma<\alpha^\delta\)
Greater3: \(\xi>0\)

Smaller0: \(\alpha^{S(\beta)}\)
Greater0: \(\alpha^\beta\cdot\alpha\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta,\gamma\) ordinals
Kind: Table
Smaller to greater: =

Question: Over ordinals, are sum, product and exponentiation continuous on the right
Answer: yes
Page: 40
Chapter: 1
Section: 8
Kind: Table

Question: Over ordinals, are sum, product and exponentiation continuous on the left
Answer: no
Page: 40
Chapter: 1
Section: 8
Kind: Table

Question: Difference between induction and recursion ?
Answer: Induction concerns proofs, recursion concerns definitions
Page: 41
Chapter: 1
Section: 9

Name: Factorial
Definition: The function sending \(0\) to 1 and \(S(n)\) to \(S(n)\cdot f(n)\)
Page: 41
Chapter: 1
Section: 9

Definition: \(\text{type}(\alpha_0\times\{0\}\cup\alpha_1\times\{1\},R)\) with lexicographical order
Page: 41
Chapter: 1
Section: 8
Variables: \(\alpha_0,\alpha_1\) sets.
Notation: \(\alpha_0+\alpha_1\)
Index: 4
Kind: Def

Definition: The type of \(\alpha_0\times\alpha_1\) with lexicographical order
Page: 41
Chapter: 1
Section: 8
Variables: \((\alpha_0,R_0),(\alpha_1,R_1)\) be ordered set
Notation: \(\alpha_0\cdot\alpha_1\)
Index: 4
Kind: Def

Definition: \(\{y\in A:yRx\}\).
Page: 44
Chapter: 1
Section: 6
Variables: \(A\) a class
\(x\) be sets
\(R\) be a binary relation on \(A\).
Notation: \(\text{pred}_{A,R}(x)\)
Index: 2
Kind: Def
Assuming: ZF-P^-
Notation2: \(\text{pred}_{A}(x)\)
Notation3: \(x\downarrow\)

Definition: identity if \(n=0\), \(f\circ f^{n-1}\) otherwise
Page: 43
Chapter: 1
Section: 9
Variables: \(A\) a set,
\(f:A\to A\)
\(n\in\mathbb N\)
Notation: \(f^n\)
Assuming: ZF-P^-

Definition: \(0\) if \(n=0\), \(f(n)+\sum_{j<n-1}f(n-1)\) otherwise
Page: 42
Chapter: 1
Section: 9
Variables: \(f:\mathbb N\to\mathbb N\)
\(n\in\mathbb N\)
Notation: \(\sum_{j<n}f(n)\)
Assuming: ZF-P^-

Smaller0: \(X\) non-empty
Greater0: \(X\) contains a \(R\)-minimal element
Page: 43, 45
Chapter: 1
Section: 9
Variables: \(A\) a class,
\(R\) a relation on \(A\)
\(X\subseteq A\)
Index: 3
Kind: Theo
Assuming: ZF-P^-
Smaller1: \(R\) a well-order
Name: Transfinite induction
Smaller2: \(R\) is set-like on \(A\)
Name2: Least number principle

Name: \(R\) is set-like on \(A\)
Definition: \(y\downarrow\) is a set for each \(y\in A\)
Page: 44
Chapter: I
Section: 9
Variables: \(A\) a class
\(R\) be a binary relation on \(A\).
Kind: Def
Example: \(\in\) on any class
Example2: \(\subseteq\) on any class satisfying power set axiom
Counterexample: the lexicographic order on \(ON\times ON\) since \((1,0)\downarrow\) equals \(ON\times\{0\}\)

Name: An (\(R\))-path of \(n\) steps in \(A\)
Definition: A function \(n+1\to A\), such that for each \(j<n\), \(s(j)R s(j+1)\)
Page: 45
Chapter: I
Section: 9
Variables: \(A\) a class
\(R\) be a binary relation on \(A\).
Index: 4. 1
Kind: Def
Denoted by: \(s\)
Assuming: \(n\in\omega\)

Name: An (\(R\))-path of \(n\) steps in \(A\) from \(a\) to \(b\)
Definition: A path \(s\) with \(s(0)=a\) and \(s(n)=b\)
Page: 45
Chapter: I
Section: 9
Variables: \(A\) a class
\(R\) be a binary relation on \(A\).
\(a,b\in A\)
Index: 4. 2
Kind: Def

Page: 45, 46
Definition: The relation containing \((a,b)\) iff there is a path in \(A\) from \(x\) to \(y\)
Chapter: I
Section: 9
Variables: \(A\) a class
\(R\) be a binary relation on \(A\).
Notation: \(R^*_A\)
Name: The transitive closure of \(R\) on \(A\)
Kind: Def, Lem
Index: 4. 3, 5
Transitive: Transitive relation
Equivalence: \(R^*\)
Assuming: ZF-P^-

Name: An acyclic relation on \(A\)
Definition: \(R^*\) is irreflexive on \(A\)
Page: 46
Chapter: I
Section: 9
Variables: \(A\) a class
Index: 7
Kind: Def
Example: Total order

Name: A cycle on \(A\)
Definition: A path on \(A\) from \(a\) to \(a\) for some \(a\in A\)
Page: 46
Chapter: I
Section: 9
Variables: \(A\) a class
Index: 7
Kind: Def

Smaller0: there exists a morphism \((A,R)\to (ON,<)\)
Greater0: \(R\) is well-founded
Page: 47
Chapter: I
Section: 9
Variables: \(A\) a class,
\(R\) a relation on \(A\)
Kind: Lem
Assuming: ZF-P^-
Counterexample: Any ordinal.

Definition: \(\text{sup}\{\text{rank}(x)+1\mid x Ry\}\), i.e. defined by transfinite recursion on \(G(x,s)=\bigcup\{S(t)\mid t\in ran(s)\}\)
Page: 47, 50
Chapter: I
Section: 9
Variables: \(A\) a class,
\(R\) a relation on \(A\)
\(y\in A\)
Context: Set theory
Notation: \(\text{rank}(y)\)
Index: 13
Kind: Def
Definition2: the least ordinal \(\alpha\) such that there is a morphism \((A,R)\to\alpha\)
Typ: ordinal
Assuming: ZF-P^-
Property: increasing function

Name: The transitive closure of \(a\)
Definition: \(\{x\mid x\in^*a\}\)
Page: 47, 48
Chapter: I
Section: 9
Variables: \(a\) a set
Index: 10
Kind: Def
Definition2: \(\bigcup\{\bigcup^ny:n\in\omega\}\) where \(\bigcup\) is considered as any function: (i.e. \(\bigcup^0\) is the identity operator, and \(\bigcup^{n+1}=\bigcup^n\bigcup\))
Abbreviation: \(\text{trcl}(a)\)
Assuming: ZF-P^-

Smaller0: \(a=b\)
Greater0: \(\text{trcl}(a)=\text{trcl}(b)\)
Page: 48
Chapter: I
Section: 9
Variables: \(a,b\) sets
Index: 10
Kind: Def
Smaller to greater: iff
Assuming: Foundation axiom
Hide sides: yes

Name: The empty set
Definition: The only set \(y\) such that \(\forall x. x\not\in y\)
Page: 014
Chapter: 1
Section: 2
Notation: \(\emptyset\)
Kind: Def
Assuming: Comprehension and extensionality axioms
Notation2: 0

Name: The power set of \(x\)
Definition: \(\{z:z\subseteq x\}\).
Page: 025
Chapter: 1
Section: 5
Variables: \(x\) a set.
Notation: \(\mathcal P(x)\)
Index: 4
Kind: Def

Question: \(\beta<\gamma\), then \(\alpha+\beta\) is
Answer: strictly less than \(\alpha+\gamma\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta,\gamma\) ordinals
Kind: Table

Question: \(\beta<\gamma\), then \(\alpha\cdot\beta\) is
Answer: strictly less than \(\alpha\cdot\gamma\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta,\gamma\) ordinals
\(\alpha\ne 0\)
Kind: Table

Question: \(\beta<\gamma\), then \(\alpha^\beta\) is
Answer: strictly less than \(\alpha^\gamma\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta,\gamma\) ordinals
\(\alpha\ne 0\)
Kind: Table

Question: \(\beta<\gamma\), then \(\beta^\alpha\) is
Answer: smaller than or equal to \(\gamma^\alpha\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta,\gamma\) ordinals
\(\alpha\ne 0\)
Kind: Table

Question: \(\beta<\gamma\), then \(\beta+\alpha\) is
Answer: smaller than or equal to \(\gamma+\alpha\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta,\gamma\) ordinals
Kind: Table

Question: \(\beta<\gamma\), then \(\beta\cdot\alpha\) is
Answer: smaller than or equal to \(\gamma\cdot\alpha\)
Page: 40
Chapter: 1
Section: 8
Variables: \(\alpha,\beta,\gamma\) ordinals,
\(\alpha\ne 0\)
Kind: Table

Question: \(\text{type}(X;R)\)
Answer: \(\le\text{type}(Y;R)\)
Page: 41
Chapter: 1
Section: 8
Variables: \(X\subseteq Y\) sets
\(R\) a well ordering of \(Y\)
Index: 5
Kind: Lem

Name: Transfinite Recursion on Well-founded Relations \((A,R)\)
Definition: A function \(F\) with domain \(A\) such that for all \(A\), \(F(a)=G(a,F\upharpoonright(a\downarrow))\)
Page: 47
Chapter: I
Section: 9
Variables: \(A\) a class
\(R\) an order,
\(R\) set like on \(A\)
\(G\) a binary function defined on the universe
Assuming: \(R\) well founded
ZF-P^-

Smaller0: \(G\) is defined by a formula
Greater0: \(F(a)=G(a,F\upharpoonright(a\downarrow))\) can be defined by a formula, such that this equality, its uniqueness (on \(A\)), and the fact that it is a function are provable
Page: 49
Chapter: I
Section: 9
Variables: \(A\) a class
\(R\) an order,
\(R\) set like on \(A\)
\(G\) a binary function defined on the universe
Index: 11, 12
Kind: Theo, Lem
Assuming: ZF-P^-
Smaller1: \(R\) well founded

Name: Well-founded relation on \(A\)
Page: 51
Section: 9
Chapter: I
Index: 15
Variables: \(A\) a class
Kind: Lem
Under: taking transitive closure
Condition: set-like relation

Smaller0: \(\alpha<\mathrm{rank}(a)\)
Greater0: \(\alpha=\mathrm{rank}(a')\) for some \(a'\in A\) with \(a'R^*_Aa\)
Page: 51
Chapter: I
Section: 9
Variables: \(A\) a class
\(R\) set like on \(A\)
\(a\in A\)
\(\alpha\) an ordinal
Index: 1116
Kind: Lem