Title: Theory / Unimportant / Math / Logic / Subsystems of second order arithmetic - Simpson
Tags: récupéré hasSeenConjDef fromImplication toBinaryRelation typToBinary fromRelation toBinaryFunction

Question: Main question of the book subsystem of second order arithmetic
Answer: Which set existence axioms are needed to prove the theorems of ordinary, non-set-theoretic mathematics?
Page: 2
Chapter: I
Section: 1

Name: number variables
Definition: Variable whose range is numbers
Page: 2
Chapter: I
Section: 1
Denoted by: \(i,j,k,m,n,\dots\)

Name: set variable
Definition: Variable whose range is set
Page: 2
Chapter: I
Section: 1
Denoted by: \(X,Y,Z\)

Name: Numerical term
Definition: Number variable, constant symbol, addition, multiplication of such elements
Page: 2
Chapter: I
Section: 1

Question: Numerical constants of \(\text Z_2\)
Answer: 0 and 1
Page: 2
Chapter: I
Section: 1

Question: Atomic formulas of \(\text Z_2\) ?
Answer: \(t=t\), \(t<t\), \(t\in X\) with \(t\) a term and \(X\) a set
Page: 2
Chapter: I
Section: 1

Question: Formulas of \(\text Z_2\)
Answer: The least set containing atomic formulas, closed under Boolean combination, quantifications over set and numbers
Page: 2
Chapter: I
Section: 1

Name: The language of second order arithmetic
Page: 3
Chapter: I
Section: 1
Notation: \(\text L_2\)
Kind: Def

Name: A model for \(\text L_2\)
Definition: \(|M|\) a non-empty set,
Page: 3
Chapter: I
Section: 2
Index: 1
Kind: Def
Definition2: \(\mathcal S_M\subseteq \mathcal P(|M|)\) non-empty,
Conjdef: A tuple with
Definition3: \(+_M,\cdot_M\) binary operation on \(|M|\),
Name2: A structure for \(\text L_2\)
Definition4: \(0_M,1_M\in|M|\)
Denoted by: \(M\)
Name3: An \(\text L_2\)-structure

Name: A sentence with parameters from \(\mathcal B\)
Definition: A sentence of the extended language \(\text L_2(\mathcal B)\)
Page: 3
Chapter: I
Variables: \((|M|,\mathcal S_M,+_M,\cdot_M,0_M,1_M,\le _M)\) a model for \(\text L_2\),
\(\mathcal B\subseteq |M|\cap\mathcal S_M\)
Index: 1
Kind: Def

Name: \(\text L_2(\mathcal B)\)
Definition: The language similar to \(\text L_2\), where an element of \(\mathcal B\) is also a term
Page: 3
Chapter: I
Variables: \((|M|,\mathcal S_M,+_M,\cdot_M,0_M,1_M,\le _M)\) a model for \(\text L_2\),
\(\mathcal B\subseteq |M|\cap\mathcal S_M\)
Index: 1
Kind: Def

Name: A sentence
Definition: A formula without free-variables
Page: 3
Chapter: I
Index: 1
Kind: Def

Name: A formula with parameters from \(\mathcal B\)
Definition: A formula of the extended language \(\text L_2(\mathcal B)\)
Page: 3
Chapter: I
Variables: \((|M|,\mathcal S_M,+_M,\cdot_M,0_M,1_M,\le _M)\) a model for \(\text L_2\),
\(\mathcal B\subseteq |M|\cap\mathcal S_M\)
Index: 1
Kind: Def

Name: A set definable over \(M\) allowing parameters from \(\mathcal B\)
Definition: A set of the form \(\{a\in|M|\mid M\models\phi(a)\}\)
Page: 3
Chapter: I
Variables: \((|M|,\mathcal S_M,+_M,\cdot_M,0_M,1_M,\le _M)\) a model for \(\text L_2\),
\(\mathcal B\subseteq |M|\cap\mathcal S_M\)
Index: 1
Kind: Def

Definition: \(\phi(a)\) is true in \(M\)
Page: 3
Chapter: I
Variables: \((|M|,\mathcal S_M,+_M,\cdot_M,0_M,1_M,\le _M)\) a model for \(\text L_2\),
\(\mathcal B\subseteq |M|\cap\mathcal S_M\),
\(\phi\) a \(\text L_2(\mathcal B)\) formula,
\(a\in M\)
Notation: \(M\models\phi(a)\)
Index: 1
Kind: Def

Name: The intended model for \(\text L_2\)
Definition: \((\omega,P(\omega),+,\cdot,0,1,<)\)
Page: 4
Chapter: I
Section: 2

Definition: the set of natural numbers
Page: 4
Chapter: I
Section: 2
Notation: \(\omega\)

Definition: The set of subsets of \(X\)
Page: 4
Chapter: I
Section: 2
Variables: \(X\) a set
Notation: \(P(X)\)

Name: The \(\omega\)-model \(\mathcal S\)
Definition: An \(L_2\)-structure of the form \((\omega,\mathcal S,+,\cdot,0,1,<)\)
Page: 4
Chapter: I
Section: 2
Variables: \(\mathcal S\subseteq P(\omega)\)
Assuming: \(\emptyset\ne\mathcal S\subseteq P(\omega)\)

Name: An \(\omega\)-model
Definition: The \(\omega\)-model \(\mathcal S\) for some \(\emptyset\ne\mathcal S\subseteq P(\omega)\)
Page: 4
Chapter: I
Section: 2

Name: Induction axiom
Definition: \((0\in X\land\forall n(n\in X\to n+1\in X))\to \forall n(n\in X)\)
Page: 4
Chapter: I
Section: 2
Index: 4(ii)
Kind: Def

Name: comprehension scheme
Definition: \(\exists X\forall n(n\in X\iff\phi(n))\) for each \(\phi(n)\) a formula of \(\text L_2\) in which \(X\) does not occur freely
Page: 4
Chapter: I
Section: 2
Index: 4(iii)
Kind: Def

Page: 4
Section: 2
Chapter: I
Axiom: \(n+1\ne 0\)
Name: basic axiom of second order arithmetic
Vocabulary: +, ×, 0, 1
Kind: Def
Index: 4(ii)
Axiom2: \(m+1=n+1\implies m=n\)
Axiom3: \(m+0=m\)
Extra: note this is only the BASIC axioms
Axiom4: \(m+(n+1)=(m+n)+1\)
Axiom5: \(m\cdot 0=0\)
Axiom6: \(m\cdot(n+1)=(m\cdot n)+m\)
Axiom8: \(m<n+1\iff(m< n\lor m=n)\)
Axiom7: \(\neg m<0\)

Name: Second order arithmetic's axiom
Definition: Basic axioms
Page: 4
Chapter: I
Section: 2
Index: 4(ii)
Kind: Def
Definition2: induction axiom
Conjdef: All of
Definition3: comprehension scheme

Name: Second order arithmetic
Definition: Axioms of second order arithmetic, and each sentences which can be deduced from this arithmetic
Page: 4, 17
Chapter: I
Section: 2, 5
Notation: \(\text Z_2\)
Index: 4(ii), 2
Kind: Def, Def
Definition2: \(\bigcup_{k\in\omega}\Pi_k^1-\mathrm{CA}_0\)
Notation2: \(\Pi^1_\infty-\text{CA}_0\)

Name: A formal system
Definition: A language and some axioms
Page: 5
Chapter: I
Section: 2

Name: A theorem of \(F\)
Definition: A formula deducible from the (universal quantification of the) axioms of \(F\)
Page: 5
Chapter: I
Section: 2
Variables: \(F\) a formal system

Name: A subsystem of \(F\)
Definition: A formal system in the language of \(F\)
Page: 5
Chapter: I
Section: 2
Variables: \(F\) a formal system

Name: A model of \(F\)
Definition: A structure over the language of \(F\) satisfiyng its axioms
Page: 5
Chapter: I
Section: 2
Variables: \(F\) a formal system

Smaller0: \(\sigma\) holds in each model of \(F\)
Greater0: \(\sigma\) is a theorem of \(F\)
Page: 5
Chapter: I
Section: 2
Variables: \(F\) a formal system
Smaller to greater: iff

Name: An \(\omega\)-model of \(F\)
Definition: Any \(\omega\)-model which satisfies the axioms of \(F\)
Page: 5
Chapter: I
Section: 2
Variables: \(F\) a formal system

Name: A \(\beta\)-model of \(F\)
Definition: Any \(\beta\)-model which satisfies the axioms of \(F\)
Page: 5
Chapter: I
Section: 2
Variables: \(F\) a formal system
Extra: beta models are defined in 1.5

Page: 6
Section: 3
Chapter: I
Axiom: induction axiom
Name: Arithmetic Comprehension Axiom
Vocabulary: +,x,0,1
Extends: Basic axioms
Axiom2: arithmetical comprehension scheme
Abbreviation: \(\text{ACA}_0\)

Name: An arithmetical formula
Definition: A formula of \(\text{L}_2(|M|\cup \mathcal S_M)\), where \(M\) is any \(\text L_2\)-structure, without set quantifiers
Page: 6
Chapter: I
Section: 3

Name: The arithmetical comprehension scheme
Definition: The comprehension scheme restricted to arithmetical formula
Page: 6
Chapter: I
Section: 3

Name: Language of first order arithmetic
Definition: Restriction of \(L_2\) without set variables
Page: 6
Chapter: I
Section: 3
Notation: \(\text L_1\)

Name: First order arithmetic
Definition: whose language is \(\text L_1\),
Page: 6, 8
Chapter: I
Section: 3
Notation: \(\text Z_1\)
Definition2: basic axioms
Conjdef: The formal system
Definition3: first-order induction scheme
Name2: Peano Aritmetic

Name: first-order induction scheme
Definition: \((\phi(0)\land\forall n(\phi(n)\to\phi(n+1)))\to\forall n\phi(n)\)
Page: 8
Chapter: I
Section: 3
Abbreviation2: PA

Smaller0: \(\sigma\) is a theorem of \(\text L_1\)
Greater0: \(\sigma\) is a theorem of \(ACA_0\)
Page: 8
Chapter: I
Section: 3
Variables: \(\sigma\) a formula of \(\text L_1\)
Hide sides: yes

Name: A conservative extension of \(F\)
Definition: \(F\) is a subsystem of \(F'\), and
Page: 8
Chapter: I
Section: 3
Variables: \(F\) a formal system
Definition2: each theorem of \(F'\) expressible in \(F\) is a theorem in \(F\)
Conjdef: A system \(F'\) such that
Extra: used but not defined

Page: 8
Section: 3
Notation: \(A_0\oplus A_1\)
Variables: \(A_0,A_1\subseteq \omega\)
Chapter: I
Name: Their recursive join
Definition: \(\{2n+i\mid n\in A_i\}\)
Commutative: not

Page: 8
Definition: the characteristic function of \(A_0\) is computable assuming an oracle for the characterisitc function of \(A_1\)
Chapter: I
Section: 3
Variables: \(A_0,A_1\subseteq \omega\)
Notation: \(A_0\le_{\text T} A_1\)
Name: \(A_1\) is Turing reducible to \(A_0\)
Transitive: transitive
Name2: \(A_1\) is recursive in \(A_0\)

Name: The Turing jump of \(A\)
Definition: The complete recursively enumerable set relative to \(A\)
Page: 8
Chapter: I
Section: 3
Variables: \(A\subseteq \omega\)
Abbreviation: \(\text{TJ}(A)\)

Definition: the set of elements arithmetical in \(\emptyset\)
Page: 8
Chapter: I
Section: 3
Variables: \(A\subseteq \omega\)
Notation: \(\mathrm{ARITH}\)
Definition2: minimum \(\omega\)-model of \(\text{ACA}_0\)

Definition: \(A\) if \(n=0\),
\(\text{TJ}(n-1,\text{TJ}(A))\) otherwise
Page: 8
Chapter: I
Section: 3
Variables: \(A\subseteq \omega\),
\(n\in\omega\)
Notation: \(\text{TJ}(n,A)\)

Question: The smallest \(\omega\)-model of \(\text{ACA}_0\) containing \(B\),
Answer: all sets which are arithemtical in \(B\)
Page: 8
Chapter: I
Section: 3
Variables: \(A\subseteq \omega\),

Page: 9
Definition: \(A_1\) is definable in some/any \(\omega\)-model \((\omega,\mathcal S,+,\cdot,0,1,<)\) by an arithmetical formula with \(A_0\) as a parameter
Chapter: I
Section: 3
Variables: \(A_0,A_1\subseteq \omega\)
Notation: \(A_0\le_{\text T} A_1\)
Name: \(A_1\) is arithmetical in \(A_0\)
Transitive: transitive
Definition2: \(A_1\le_{\text T}\text{TJ}(n,A_0)\) for some \(n\in\omega\)

Name: A well-ordered set
Definition: A totally ordered set \((X,\le)\) such that every non-empty subset of \(X\) has a minimal element
Page: 13
Chapter: 1
Section: 3

Definition: The unique set such that \(\forall n(n\in X)\)
Page: 9
Chapter: 1
Section: 4
Context: \(\mathrm{ACA_0}\)
Notation: \(\mathbb N\)

Name: numerical pairing function
Definition: The function associating a pair \(m,n\) to \((m,n)\)
Page: 9
Chapter: 1
Section: 4
Context: \(\mathrm{ACA_0}\)

Definition: \((m+n)^2+m\)
Page: 9
Chapter: 1
Section: 4
Variables: \(m,n\in\mathbb N\)
Context: \(\mathrm{ACA_0}\)
Notation: \((m,n)\)

Definition: the set of \((m,n)\) for \(m,n\in \mathbb N\)
Page: 9
Chapter: 1
Section: 4
Variables: \(X,Y\subseteq\mathbb N\)
Notation: \(X\times Y\)
Typ: subset of \(\mathbb N\)
Assuming: \(\mathrm{ACA_0}\)

Name: A function from \(X\) to \(Y\)
Definition: a subset of \(X\times Y\) such that, for each \(x\in X\) there is exactly one \(y\in Y\) such that \((x,y)\in f\)
Page: 9
Chapter: 1
Section: 4
Variables: \(X,Y\subseteq\mathbb N\)
Context: \(\mathrm{ACA_0}\)
Notation: \(X\to Y\)
Denoted by: f

Name: The function defined from \(g\) by primitive recursion
Definition: [$]\defFun
{\mathbb N\times X}
{Y}
{(n,m)}
{
\left\{
\begin{array}{ll}
f(m)&\text{ if $n=0$,}\\
g(n-1,m,h(n,m))&\text{otherwise}
\end{array}
\right.
}[/$]
Page: 9
Chapter: 1
Section: 4
Variables: \(X,Y\subseteq\mathbb N\)
\(f:X\to Y\)
\(g:\mathbb N\times X\times Y\to Y\)
Conjdef: A function \(h:\mathbb N\times X\to Y\) such that
Assuming: ACA_0

Name: The natural number system
Definition: The number system whose model is \(M\)
Page: 9
Chapter: 1
Section: 4
Variables: [$]M=(\abs{M},S_M,+_M,\cdot_M,0_M,1_M,<_M)[/$] a model
Context: \(\mathrm{ACA_0}\)

Name: The system of rational numbers in \(M\)
Definition: set: the elements of \(\mathbb Z\times\mathbb Z^+\), minimal in the equivalence class where \((m,n)\equiv (i,j)\) if \((m\cdot j)=(n\cdot i)\)
Page: 9
Chapter: 1
Section: 4
Variables: [$]M=(\abs{M},S_M,+_M,\cdot_M,0_M,1_M,<_M)[/$] a model
Context: \(\mathrm{ACA_0}\)
Notation: \(\mathbb Q\)
Definition2: \((m,n)+(i,j)=(mj+in,nj)\)
Conjdef: The system with
Definition3: \(-(m,n)=(-m,n)\)
Definition4: \((m,n)\cdot(i,j)= mi,nj\)
Definition5: \(0_{\mathbb Z}=(0,1)\)
Definition6: \(1_{\mathbb Z}=(1,1)\)
Definition7: \((m,n)<(i,j)\) if \(mj<ni\)

Name: The system of integers in \(M\)
Definition: set: the elements of \(\mathbb N\times\mathbb N\), minimal in the equivalence class where \((m,n)\equiv (i,j)\) if \((m+j)=(n+i)\)
Page: 9
Chapter: 1
Section: 4
Variables: [$]M=(\abs{M},S_M,+_M,\cdot_M,0_M,1_M,<_M)[/$] a model
Context: \(\mathrm{ACA_0}\)
Notation: \(\mathbb Z\)
Definition2: \(+\) componentwise
Conjdef: The system with
Definition3: \(-(m,n)=(n,m)\)
Definition4: \((m,n)\cdot(i,j)= mi+nj,mj+ni\)
Definition5: \(0_{\mathbb Z}=(0,0)\)
Definition6: \(1_{\mathbb Z}=(1,0)\)
Definition7: \((m,n)<(i,j)\) if \(m+j<n+i\)

Name: A sequence of element of \(X\)
Definition: A function \(\mathbb N\to X\)
Page: 9
Chapter: 1
Section: 4
Variables: [$]M=(\abs{M},S_M,+_M,\cdot_M,0_M,1_M,<_M)[/$] a model
\(X\) a set
Context: \(\mathrm{ACA_0}\)
Notation: \(\langle q_n\rangle\)

Name: A double sequence of element of \(X\)
Definition: A function \(\mathbb N\times\mathbb N\to X\)
Page: 11
Chapter: 1
Section: 4
Variables: \(M=(|M|,S_M,+_M,\cdot_M,0_M,1_M,{\lt}_M)\) a model
\(X\) a set
Context: \(\mathrm{ACA_0}\)
Notation: \(\langle q_{mn}\rangle\)

Name: A real number
Definition: A Cauchy sequence of rational numbers
Page: 12
Chapter: 1
Section: 4
Variables: [$]M=(\abs{M},S_M,+_M,\cdot_M,0_M,1_M,<_M)[/$] a model
Context: \(\mathrm{ACA_0}\)
Index: 2
Kind: Def

Name: The class of real numbers
Page: 12
Chapter: 1
Section: 4
Variables: [$]M=(\abs{M},S_M,+_M,\cdot_M,0_M,1_M,<_M)[/$] a model
Context: \(\mathrm{ACA_0}\)
Notation: \(\mathbb R\)
Index: 2
Kind: Def

Name: A sequence of real number
Definition: A double sequence of rational \(\langle q_{mn}\rangle\), with each sequence converging when second component is fixed
Page: 13
Chapter: 1
Section: 4
Variables: [$]M=(\abs{M},S_M,+_M,\cdot_M,0_M,1_M,<_M)[/$] a model
Context: \(\mathrm{ACA_0}\)
Index: 2
Kind: Def

Name: A complete separable metric space
Definition: Nonempty set \(A\subseteq \mathbb N\)
Page: 13
Chapter: 1
Section: 4
Variables: [$]M=(\abs{M},S_M,+_M,\cdot_M,0_M,1_M,<_M)[/$] a model
Index: 5
Kind: Def
Definition2: a function \(d:A\times A\to \mathbb R\) with usual distance properties
Conjdef: Tuple

Name: A point of the complete separable metric space
Definition: An equivalence class of the Cauchy sequence
Page: 13
Chapter: 1
Section: 4
Variables: [$]M=(\abs{M},S_M,+_M,\cdot_M,0_M,1_M,<_M)[/$] a model
Nonempty set \(A\subseteq \mathbb N\)
Index: 5
Kind: Def

Definition: The set of points of the complete separable metric space
Page: 14
Chapter: 1
Section: 4
Variables: [$]M=(\abs{M},S_M,+_M,\cdot_M,0_M,1_M,<_M)[/$] a model
Nonempty set \(A\subseteq \mathbb N\)
Notation: \(\hat A\)
Index: 5
Kind: Def

Name: A continuous function
Definition: \((a,r,b,s)\in\Phi\) and \((a,r,b',s')\in \Phi\) imply \(d_B(b,b')<s+s'\)
Page: 14
Chapter: 1
Section: 4
Variables: [$]M=(\abs{M},S_M,+_M,\cdot_M,0_M,1_M,<_M)[/$] a model
Nonempty sets \(A,B\subseteq \mathbb N\)
functions \(d_A,d_B\)
Index: 6
Kind: Def
Definition2: \((a,r,b,s)\in\Phi\) and \(d_B(b,b')+s<s'\) imply \((a,r,b',s')\in\Phi\)
Conjdef: A set \(\Phi\subseteq A\times\mathbb Q^+\times B\times\mathbb Q^+\)
Definition3: \((a,r,b,s)\in\Phi\) and \(d_B(a,a')+r<r'\) imply \((a',r',b,s)\in\Phi\)
Applied to3: For any \(x\in\hat A\) there exists a unique \(y\in\hat B\) such that \(d(b,y)\le s\) for all \((a,r,b,s)\in\Phi\) such that \(d_A(a,x)<r\), it is the image of \(x\) by \(\Phi\)

Name: An open set
Definition: A subset of \(A\times\mathbb Q^+\)
Page: 15
Chapter: 1
Section: 4
Variables: [$]M=(\abs{M},S_M,+_M,\cdot_M,0_M,1_M,<_M)[/$] a model
Nonempty sets \(A\subseteq \mathbb N\)
functions \(d_A\)
Index: 7
Kind: Def

Name: An open set
Definition: \(d(x,a)<r\) for some \((a,r)\in U\)
Page: 15
Chapter: 1
Section: 4
Variables: [$]M=(\abs{M},S_M,+_M,\cdot_M,0_M,1_M,<_M)[/$] a model
Nonempty sets \(A\subseteq \mathbb N\)
functions \(d_A\)
\(U\subseteq A\times\mathbb Q^+\) an open set
Notation: \(x\in U\)
Index: 7
Kind: Def

Definition: A formula \(\forall X_1\exists X_2\forall X_2\dots X_k\phi\) with \(X_i\) being set variables and \(\phi\) an arithmetical formula
Page: 15
Chapter: 1
Section: 5
Notation: A \(\Pi_k^1\)-formula
Index: 7
Kind: Def

Definition: A formula \(\exists X_1\forall X_2\exists X_2\dots X_k\phi\) with \(X_i\) being set variables and \(\phi\) an arithmetical formula
Page: 15
Chapter: 1
Section: 5
Notation: A \(\Sigma_1^1\)-formula
Index: 7
Kind: Def

Page: 17
Section: 5
Chapter: 1
Axiom: induction axioms restricted to \(\Pi_k^1\)-formulas
Extends: basic axioms
Kind: Def
Index: 2
Axiom2: comprehension scheme restricted to \(\Pi_k^1\)-formulas
Variables: \(k\in\omega\)
Assuming: \(\Pi^1_k-\mathrm{CA}_0\)

Name: A \(\beta\)-model
Definition: if \(\sigma\) is any \(\Pi^1_1\) or \(\Sigma^1_1\)-sentence with parameters from \(\mathcal S\), \((\omega,\mathcal S,+,\cdot,0,1,<)\) satisfies \(\sigma\) iff the indended model \((\omega,P(\omega),+,\cdot,0,1,<)\) satisfies \(\sigma\)
Page: 18
Chapter: 1
Section: 5
Conjdef: An \(\omega\)-model \(\mathcal S\subseteq P(\omega)\) such that

Name: A \(\beta\)-model of \(T\)
Definition: A \(\beta\)-model satisfying the axioms of \(T\)
Page: 18
Chapter: 1
Section: 5
Variables: \(T\) a subsystem of \(\mathrm Z_2\)

Name: The \(\alpha\)-th level of the constructible hierarchy
Page: 18
Chapter: 1
Section: 5
Variables: \(\alpha\) an ordinal
Context: Second order arithmetic
Notation: \(L_{\alpha}\)

Question: The minimal \(\beta\)-model of \(\Pi_k^1-\mathrm{CA}_0\) is
Answer: of the form \(L_{\alpha}\cap P(\omega)\)
Page: 18
Chapter: 1
Section: 5
Variables: \(k\in\omega\)

Definition: the ordinal such that  \(L_{\alpha}\cap P(\omega)\) is the minimal \(\beta\)-model of \(\Pi_k^1-\mathrm{CA}_0\).
Page: 18
Chapter: 1
Section: 5
Variables: \(k\in\omega\)
Notation: \(\alpha_k\)
Typ: strictly increasing

Question: The minimum \(\omega\)-model of \(\mathrm{RCA_0}\) is
Answer: \(\mathrm{REC}\)
Page: 65
Chapter: II
Section: 1
Index: 8
Kind: Cor

Definition: The set of formula of the form \(\forall X_1\exists X_2\dots X_k\theta\) with \(\theta\) is an arithmetical formula
Page: 16
Chapter: 1
Section: 5
Variables: \(i\in\mathbb N\)
Notation: \(\Pi_i^1\)
Definition2: The negation of a \(\Sigma_k^1\)-formula

Definition: The set of formula of the form \(\exists X_1\forall X_2\dots X_k\theta\) with \(\theta\) is an arithmetical formula
Page: 16
Chapter: 1
Section: 5
Variables: \(k\in\mathbb N\)
Notation: \(\Sigma_k^1\)
Definition2: The negation of a \(\Pi_k^1\)-formula

Page: 17
Section: 5
Chapter: 1
Axiom: basic axiom
Axiom2: induction axiom
Axiom3: comprehension scheme restricted to L_2 formulas which are \(\Pi_k^1\)
Notation: \(\Pi_k^1-\mathrm{CA}_0\) or \(\Sigma_k^1-\mathrm{CA}_0\)

Name: A \(\beta\)-model
Definition: if \(\sigma\) is \(\Pi_1^1\) or \(\Sigma_1^1\) sentence with parameters from \(\mathcal S\) then \((\omega,\mathcal S,+,\cdot,0,1,<)\) satisfies \(\sigma\) iff the intended model \((\omega,\P(\omega),+,\cdot,0,1,<)\) satisfies \(\sigma\)
Page: 18
Chapter: 1
Section: 5
Index: 3
Kind: Def
Conjdef: A \(\omega\)-model \(\mathcal S\subseteq P(\omega)\) with

Name: A \(\beta\)-model
Definition: if \(\sigma\) is \(\Pi_1^1\) or \(\Sigma_1^1\) sentence with parameters from \(\mathcal S\) then \((\omega,\mathcal S,+,\cdot,0,1,<)\) satsifies \(\sigma\) iff the intended model \((\omega,\P(\omega),+,\cdot,0,1,<)\) satisfies \(\sigma\)
Page: 18
Chapter: 1
Section: 5
Index: 3
Kind: Def
Conjdef: A \(\omega\)-model \(\mathcal S\subseteq P(\omega)\) with

Name: A \(\beta\)-model of \(T\)
Definition: A \(\beta\)-model satisfying the axioms of \(T\)
Page: 18
Chapter: 1eT a
Section: 5
Variables: \(T\) a subsystem of \(\mathrm Z_2\)
Index: 3
Kind: Def

Smaller0: a \(\beta\)-model of \(\Pi_1^1\)
Greater0: non-empty, closed under union
Page: 18
Chapter: 1eT a
Section: 5
Variables: \(\mathcal S\subseteq P(\omega)\)
Index: 3
Kind: Def
Smaller to greater: iff
Prefix Greater: \(\mathcal S\) is
Greater1: closed under HJ (hyperjump of \(A\))
Greater2: closed under disjoint union \(\oplus\)
Greater3: closed under taking a set hyperarithmetical in a set of \(\mathcal S\)

Smaller0: the minimal \(\beta\)-model of \(\Pi_1^1-\mathrm{CA}_0\)
Greater0: the set of \(A\in P(\omega)\) such that \(A\le_H\mathrm{HJ}(n,\emptyset)\) for some integer \(n\)
Page: 18
Chapter: 1eT a
Section: 5
Index: 3
Kind: Def
Smaller to greater: equals

Name: A countable linear ordering
Definition: A structure \((A,\le_A)\) with \(A\subseteq\mathbb N\), \(\le_A\) an irreflexive linear ordering of \(A\)
Page: 18
Chapter: 1eT a
Section: 5
Context: \(\mathrm{ACA}_0\)
Index: 3
Kind: Def

Name: A countable well ordering
Definition: A countable linear ordering \((A,\le_A)\) with no infinite decreasing sequence
Page: 18
Chapter: 1eT a
Section: 5
Context: \(\mathrm{ACA}_0\)
Index: 3
Kind: Def

Name: The ordinal encoded by \(A\)
Definition: the order type of \((A,<_A)\)
Page: 18
Chapter: 1eT a
Section: 5
Variables: \((A,<_A)\) a countable well ordering
Context: \(\mathrm{ACA}_0\)
Index: 3
Kind: Def

Smaller0: \(A\) and \(B\) encodes the same ordinal
Greater0: \((A,<_A)\) is isomorphic to \((B,<_B)\)
Page: 18
Chapter: 1eT a
Section: 5
Variables: \((A,<_{A}),(B,<_B)\) countable well orderings
Index: 3
Kind: Def
Smaller to greater: iff
Context: \(\mathrm{ACA}_0\)

Name: Comparable countable well ordering
Definition: The relation containing pair of countable well ordering such that one is isomorphic to an initial fragment of the other one
Page: 18
Chapter: 1eT a
Section: 5
Index: 3
Kind: Def

Name: A divisible group
Definition: An Abelian group \(G\) such that, for each \(a\in G\), \(n>0\), there exists \(b\in G\) such that \(nb=a\)
Page: 19
Chapter: 1eT a
Section: 5
Index: 3
Kind: Ex

Name: A reduced group
Definition: having no non-trivial divisible subgroup
Page: 19
Chapter: 1eT a
Section: 5
Index: 3
Kind: Ex
Definition2: such that \(G_{\infty}=0\)
Conjdef: An Abelian group, equivalently

Definition: \(G\) if \(\alpha=0\)
Page: 19
Chapter: 1eT a
Section: 5
Variables: \(G\) a countable Abelian \(p\)-group
\(\alpha\) an ordinal
Notation: \(G_\alpha\)
Index: 3
Kind: Ex
Definition2: \(pG_{\alpha-1}\) for \(\alpha\) successor
Definition3: \(\bigcap_{\delta<\alpha}G_\delta\) for \(\alpha\) limit

Definition: the set of \(a\in G_\alpha\) such that \(pa=0\)
Page: 19
Chapter: 1eT a
Section: 5
Variables: \(G\) a countable Abelian \(p\)-group
\(\alpha\) an ordinal
Notation: \(P_\alpha\)
Index: 3
Kind: Ex

Name: The Ulm invariants of \(G\)
Definition: The numbers \(\mathrm{dim}(P_\alpha/P_{\alpha+1})\)
Page: 19
Chapter: 1
Section: 5
Variables: \(G\) a countable Abelian \(p\)-group
\(\alpha\) an ordinal
Index: 3
Kind: Ex

Smaller0: \(G\) is isomorphic to \(H\)
Greater0: the Ulm invariants of \(G\) and \(H\) are the same
Page: 19
Chapter: 1
Section: 5
Variables: \(G,H\) countable Abelian \(p\)-groups
Index: 3
Kind: Ex
Smaller to greater: iff
Assuming: \(G,H\) reduced
Name: The Ulm theorem

Name: An isolated point of \(C\)
Definition: A point \(x\in C\) such that \(\{x\}=C\cap U\) for some open \(U\)
Page: 20
Chapter: 1
Section: 5
Variables: \(C\subseteq \mathbb R^n\)
Index: 4
Kind: Ex
Assuming: \(C\) closed
Property: the Ulm invariants of \(G\) and \(H\) are the same

Question: The number of isolated point of \(C\) is
Answer: at most countable
Page: 20
Chapter: 1
Section: 5
Variables: \(C\subseteq \mathbb R^n\) closed
Index: 4
Kind: Ex

Name: A perfect set
Definition: without isolated points
Page: 20
Chapter: 1
Section: 5
Index: 4
Kind: Ex
Definition2: equal to its derivated set
Conjdef: A closed set, equivalently

Name: The derived set of \(C\)
Definition: The set of non-isolated points of \(C\)
Page: 20
Chapter: 1
Section: 5
Variables: \(C\subseteq\mathbb R^n\) a closed set
Notation: \(C'\)
Index: 4
Kind: Ex

Definition: \(C\) if \(\alpha=0\)
Page: 20
Chapter: 1
Section: 5
Variables: \(C\subseteq\mathbb R^n\) a closed set
\(\alpha\) an ordinal
Notation: \(C_\alpha\)
Index: 4
Kind: Ex
Definition2: \(C_{\alpha-1}'\) if \(\alpha\) a successor
Definition3: \(\bigcap_{\beta<\alpha}C_\beta\) if \(\alpha\) is a successor

Name: The derived sequence of \(C\)
Definition: \((C_\alpha)_{\alpha}\) for \(\alpha\) ordinals
Page: 20
Chapter: 1
Section: 5
Variables: \(C\subseteq\mathbb R^n\) a closed set
Index: 4
Kind: Ex
Typ: An ultimately constant sequence

Name: The perfect kernel of \(C\)
Definition: \(C_\alpha\) for some \(\alpha\) such that \(C_\alpha=C_{\alpha+1}\)
Page: 20
Chapter: 1
Section: 5
Variables: \(C\subseteq\mathbb R^n\) a closed set
Notation: \(C_\infty\)
Index: 4
Kind: Ex
Definition2: the largest closed perfect subset of \(C\)

Question: \(C\) can be written as
Answer: the union of a perfect set, \(C_\infty\), and a countable set
Page: 20
Chapter: 1
Section: 5
Variables: \(C\subseteq\mathbb R^n\) a closed set
Index: 4
Kind: Ex
Name: Cantor-Bendixson theorem

Definition: \(\bigcup_{k\in\mathbb N}\mathbb N^k\)
Page: 21
Chapter: 1
Section: 5
Context: \(\mathrm{ACA}_0\)
Notation: \(\mathrm{Seq}\)
Kind: Def
Notation2: \(\mathbb N^{<\mathbb N}\)

Name: The concatenation of \(\sigma\) followed by \(\theta\)
Page: 21
Chapter: 1
Section: 5
Variables: \(\sigma,\theta\in\mathrm{Seq}\)
Context: \(\mathrm{ACA}_0\)
Notation: \(\sigma\circ\theta\)
Kind: Def

Name: A tree
Definition: A subset of \(\mathrm{Seq}\) closed under taking initial segment
Page: 21
Chapter: 1
Section: 5
Context: \(\mathrm{ACA}_0\)
Kind: Def

Name: An (infinite) path of \(T\)
Definition: A function \(f:\mathbb N\to\mathbb N\) such that for all \(k\in \mathbb N\), \(f[k]\in T\)
Page: 21
Chapter: 1
Section: 5
Variables: \(T\) a tree
Context: \(\mathrm{ACA}_0\)
Kind: Def

Definition: \(\langle f(0),\dots,f(k-1)\rangle\)
Page: 21
Chapter: 1
Section: 5
Variables: \(T\) a tree
\(f:\mathbb N\to\mathbb N\)
\(k\in\mathbb N\)
Context: \(\mathrm{ACA}_0\)
Notation: \(f[k]\)
Kind: Def

Definition: The set of pathes through \(T\)
Page: 21
Chapter: 1
Section: 5
Variables: \(T\) a tree
Context: \(\mathrm{ACA}_0\)
Notation: \([T]\)
Kind: Def

Name: A well founded tree
Definition: A tree without infinite path
Page: 21
Chapter: 1
Section: 5
Context: \(\mathrm{ACA}_0\)
Kind: Def

Name: An end node of \(T\)
Definition: A sequence \(\tau\in T\) which has no proper extension in \(T\)
Page: 21
Chapter: 1
Section: 5
Variables: \(T\) a tree
Context: \(\mathrm{ACA}_0\)
Kind: Def

Name: Compatible sequences
Definition: The relation on sequences such that one is the initial segment of the other
Page: 21
Chapter: 1
Section: 5
Context: \(\mathrm{ACA}_0\)
Kind: Def

Definition: the set of \(\tau\in T\) such that \(\sigma\) is compatible with \(\tau\)
Page: 21
Chapter: 1
Section: 5
Variables: \(T\) a tree
\(\sigma\in\mathrm{Seq}\)
Context: \(\mathrm{ACA}_0\)
Notation: \(T_\sigma\)
Index: 6
Kind: Def

Name: The derived tree of \(T\)
Definition: The set of \(\sigma\in\mathrm{Seq}\) such that \(T_\sigma\) contains a pair of incompatible sequences
Page: 21
Chapter: 1
Section: 5
Variables: \(T\) a tree
Context: \(\mathrm{ACA}_0\)
Notation: \(T'\)
Index: 6
Kind: Def

Name: A perfect tree
Definition: \(T'=T\)
Page: 21
Chapter: 1
Section: 5
Context: \(\mathrm{ACA}_0\)
Index: 6
Kind: Def
Definition2: each \(\sigma\in T\) admits incompatible extension in \(T\)
Conjdef: A tree such that, equivalently

Definition: \(T\) if \(\alpha=0\)
Page: 21
Chapter: 1
Section: 5
Variables: \(T\) a tree
\(\alpha\) an ordinal
Context: \(\mathrm{ACA}_0\)
Notation: \(T_\alpha\)
Index: 6
Kind: Def
Definition2: \(T_{\alpha-1}'\) if \(\alpha\) is a successor
Definition3: \(\bigcap_{\beta<\alpha}T_\alpha\) if \(\alpha\) is a limit

Definition: \(T_\alpha\) for an ordinal \(\alpha\) such that \(T_\alpha=T_\alpha+1\)
Page: 21
Chapter: 1
Section: 5
Variables: \(T\) a tree
Context: \(\mathrm{ACA}_0\)
Notation: \(T_\infty\)
Index: 6
Kind: Def
Definition2: the largest perfect subtree of \(T\)

Name: A code for a Borel set in \(\hat A\)
Definition: well-founded
Page: 22
Chapter: 1
Section: 5
Variables: \(\hat A\) a metric space
Context: \(\mathrm{ACA}_0\)
Index: 7
Kind: Def
Definition2: whose end node belong to \(A\times\mathbb Q^+\)
Conjdef: A tree
Definition3: containing a single sequence of length 1
Name2: A Borel code
Denoted by: \(B\)
Assuming: \(\hat A\) complete separable

Definition: the code for the basic open neighborhood \(\mathbf B(a,r)\)
Page: 22
Chapter: 1
Section: 5
Variables: \(\hat A\) a complete separable metric space
\(a\in A\)
\(r\in\mathbb Q^+\)
Context: \(\mathrm{ACA}_0\)
Notation: \(\langle(a,r)\rangle\)
Index: 7
Kind: Def
Conjdef: A tree

Definition: the empty sequence
Page: 22
Chapter: 1
Section: 5
Variables: \(\hat A\) a complete separable metric space
\(B\) a Borel code
\(n\in\mathrm{Seq}\)
\(m_0\in\mathbb N\)
Context: \(\mathrm{ACA}_0\)
Notation: \(B_n\)
Index: 7
Kind: Def
Definition2: \(\langle n\rangle\circ \tau \) for each \(\langle m_0,n\rangle \circ\tau\in B\)
Conjdef: The tree containing
Assuming: \(\langle m_0,n\rangle\in B\)

Name: The set encoded by \(B\)
Definition: \(m_0\) is odd and \(x\in B_n\) for some \(n\)
Page: 22
Chapter: 1
Section: 5
Variables: \(\hat A\) a complete separable metric space
\(B\) a Borel code
Context: \(\mathrm{ACA}_0\)
Index: 7
Kind: Def
Definition2: \(m_0\) is even and \(x\not\in B_n\) for some \(n\)
Conjdef: The set of \(x\in B\) such that, either

Name: The code for an analytic set
Definition: The code for a continuous function \(\mathbb{N^N}\to\hat A\)
Page: 22
Chapter: 1
Section: 5
Variables: \(\hat A\) a complete separable metric space
Context: \(\mathrm{ACA}_0\)
Index: 8
Kind: Def
Conjdef: The set of \(x\in B\) such that, either
Denoted by: \(\phi\)

Name: The set encoded by \(\phi\)
Definition: \(\phi^{-1}(x)\)
Page: 22
Chapter: 1
Section: 5
Variables: \(\hat A\) a complete separable metric space
\(\phi:\mathbb{N^N}\to\hat A\) a continuous function
Context: \(\mathrm{ACA}_0\)
Index: 8
Kind: Def
Conjdef: The set of \(x\in B\) such that, either
Denoted by: \(S\)