Title: Theory / Unimportant / Math / Logic / Subsystems of second order arithmetic - Simpson / II
Tags: récupéré

Definition: \(\forall n(n<t\implies \phi)\)
Page: 63
Chapter: II
Section: 1
Variables: \(n\) a number variable
\(t\) a numerical term not containing \(n\)
Notation: \((\forall n<t)\phi\)
Kind: Def

Definition: \(\forall n(n<t\land\phi)\)
Page: 63
Chapter: II
Section: 1
Variables: \(n\) a number variable
\(t\) a numerical term not containing \(n\)
Notation: \((\exists n<t)\phi\)
Kind: Def

Name: Bounded quantifiers
Definition: \(\forall n\) or \(\exists n<t\) with \(n\) a number variable \(t\) a numerical term not containing \(n\)
Page: 63
Chapter: II
Section: 1
Kind: Def

Definition: atomic formulas
Page: 63
Chapter: II
Section: 1
Notation: \(\Sigma_0^0\)-formula
Index: 2
Kind: Def
Definition2: propositional connectives applying to such formula
Conjdef: Either
Definition3: bounded quantifiers followed by such formulas

Name: \(k\in\omega\)
Definition: \(\exists n_1\forall n_2\dots n_k\theta\) with \(\theta\in\Sigma_0^0\)
Page: 63
Chapter: II
Section: 1
Notation: \(\Sigma_k^0\)-formula
Index: 2
Kind: Def

Definition: \(\forall n_1\exists n_2\dots n_k\theta\) with \(\theta\in\Sigma_0^0\)
Page: 63
Chapter: II
Section: 1
Variables: \(k\in\omega\)
Notation: \(\Pi_k^0\)-formula
Index: 2
Kind: Def

Name: The scheme of \(\Sigma_k^0\) induction
Definition: all axioms of the form \((\phi(0)\land\forall n(\phi(n)\implies\phi(n+1)))\implies \forall n\phi(n)\) where \(\phi(n)\) is any \(\Sigma^0_k\) formula of the language of second order arithmetic
Page: 64
Chapter: II
Section: 1
Variables: \(k\in\omega\)
Index: 3
Kind: Def

Name: The scheme of \(\Pi_k^0\) induction
Definition: all axioms of the form \((\phi(0)\land\forall n(\phi(n)\implies\phi(n+1)))\implies \forall n\phi(n)\) where \(\phi(n)\) is any \(\Pi^0_k\) formula of the language of second order arithmetic
Page: 64
Chapter: II
Section: 1
Variables: \(k\in\omega\)
Index: 3
Kind: Def

Name: The scheme of \(\Delta^0_1\) comprehension
Definition: All axioms of the form \(\forall n(\phi(n)\iff\psi(n))\implies\exists X \forall n(n\in X\iff \phi(n))\) where \(\phi(n)\) is any \(\Pi^0_k\), \(\psi(n)\) is any \(\Pi^0_k\) formula and \(X\) is not free in \(\phi(n)\)
Page: 64
Chapter: II
Section: 1
Variables: \(k\in\omega\)
Index: 4
Kind: Def

Page: 64
Section: 1
Chapter: II
Axiom: schemes of \(\Sigma^0_1\) induction
Extends: basic axioms
Kind: Def
Index: 5
Axiom2: schemes of \(\Delta^0_1\) comprehension
Assuming: \(\mathrm{RCA_0}\)

Name: A Turing ideal
Definition: nonempty
Page: 64
Chapter: II
Section: 1
Index: 7
Kind: Lem
Definition2: closed under disjoint union
Conjdef: Some \(\mathcal S\subseteq P(\omega)\)
Definition3: closed under Turing reducibility

Definition: The set of recursive subsets of \(\omega\)
Page: 64
Chapter: II
Section: 1
Notation: \(\mathrm{REC}\)
Index: 7
Kind: Lem