User:Binary198/Binary198's notepad

This is my notepad, where I just write about maths stuff. Kinda like a talk page, except just for me. I could've put this on my website, but it doesn't support MathJax / LaTeX.

List of axioms within the theories of iterated inductive definitions

ID₁

• $0\in \mathbb {N}$: 0 is a natural number.
• $\forall x(x=x)$: Equality is reflexive.
• $\forall x\forall y=x\rightarrow x=y$: Equality is symmetric.
• $\forall x\forall y\forall z(x=y\land y=z\rightarrow x=z)$: Equality is transitive.
• $\forall x\forall y(x\in \mathbb {N} \land x=y\rightarrow y\in \mathbb {N} )$: The natural numbers are closed under equality.
• $\forall x\in \mathbb {N} (S(x)\in \mathbb {N} )$: The natural numbers are closed under S (the successor operation).
• $\forall x,y\in \mathbb {N} (x=y\leftrightarrow S(x)=S(y))$: S is an injection.
• $\forall x\in N(S(x)\neq 0)$: There is no natural number who's successor is zero.
• $\forall X(0\in X\land \forall x\in \mathbb {N} (x\in X))\rightarrow \mathbb {N} \subseteq X$: If K is a set such that 0 is in K, and for every natural number n, n being in K implies that S(n) is in K, then K contains every natural number.
• The induction scheme for $L_{ID_{1}}$ formulas.
• $A(I_{A})\subseteq I_{A}$
• $A(F)\subseteq F\rightarrow I_{A}\subseteq F$

Note that the second-to-last axiom expresses that $I_{A}$ is closed under the arithmetically definable set operator $\Gamma _{A}(S)=\{x\in \mathbb {N} |\mathbb {N} \models A(S,x)\}$, while the last axiom expresses that $I_{A}$ is the least such (at least among sets definable in $L_{ID_{1}}$).

Thus, $I_{A}$ is meant to be the least pre-fixed-point, and hence the least fixed point of the operator $\Gamma _{A}$. Also, $F(x)$ represents the set $\{x\in N|F(x)\}$, $s\in F$ means $F(s)$, and for two formulas $F$ and $G$, $F\subseteq G$ means $\forall xF(x)\rightarrow G(x)$.

ID_ν

• $0\in \mathbb {N}$: 0 is a natural number.
• $\forall x(x=x)$: Equality is reflexive.
• $\forall x\forall y=x\rightarrow x=y$: Equality is symmetric.
• $\forall x\forall y\forall z(x=y\land y=z\rightarrow x=z)$: Equality is transitive.
• $\forall x\forall y(x\in \mathbb {N} \land x=y\rightarrow y\in \mathbb {N} )$: The natural numbers are closed under equality.
• $\forall x\in \mathbb {N} (S(x)\in \mathbb {N} )$: The natural numbers are closed under S (the successor operation).
• $\forall x,y\in \mathbb {N} (x=y\leftrightarrow S(x)=S(y))$: S is an injection.
• $\forall x\in N(S(x)\neq 0)$: There is no natural number who's successor is zero.
• $\forall X(0\in X\land \forall x\in \mathbb {N} (x\in X))\rightarrow \mathbb {N} \subseteq X$: If K is a set such that 0 is in K, and for every natural number n, n being in K implies that S(n) is in K, then K contains every natural number.
• The induction scheme for $L_{ID_{\nu }}$ formulas.
• $TI(\prec ,F)$ expresses transfinite induction along $\prec$ for an arbitrary $L_{ID_{\nu }}$ formula $F$.
• $\forall \mu \prec \nu ;A^{\mu }(J_{A}^{\mu })\subseteq J_{A}^{\mu }$ for an arbitrary $L_{ID_{\nu }}$ formula $F$.
• $\forall \mu \prec \nu ;A^{\mu }(F)\subseteq F\rightarrow J_{A}^{\mu }\subseteq F$ for an arbitrary $L_{ID_{\nu }}$ formula $F$.

In these last two axioms we used the abbreviation $A^{\mu }(F)$ for the formula $A(F,(\lambda \gamma y;\gamma \prec \mu \land y\in J_{A}^{\gamma }),\mu ,x)$, where $x$ is the distinguished variable. We see that these express that each $J_{A}^{\mu }$, for $\mu \prec \nu$, is the least fixed point (among definable sets) for the operator $\Gamma _{A}^{\mu }(S)=\{n\in \mathbb {N} |(\mathbb {N} ,(J_{A}^{\gamma })_{\gamma \prec \mu }\}$. Note how all the previous sets $J_{A}^{\gamma }$, for $\gamma \prec \mu$, are used as parameters.

We then define $ID_{\prec \nu }=\bigcup \limits _{\xi \prec \nu }ID_{\xi }$.

${\widehat {\mathsf {ID}}}_{\nu }$

• $0\in \mathbb {N}$: 0 is a natural number.
• $\forall x(x=x)$: Equality is reflexive.
• $\forall x\forall y=x\rightarrow x=y$: Equality is symmetric.
• $\forall x\forall y\forall z(x=y\land y=z\rightarrow x=z)$: Equality is transitive.
• $\forall x\forall y(x\in \mathbb {N} \land x=y\rightarrow y\in \mathbb {N} )$: The natural numbers are closed under equality.
• $\forall x\in \mathbb {N} (S(x)\in \mathbb {N} )$: The natural numbers are closed under S (the successor operation).
• $\forall x,y\in \mathbb {N} (x=y\leftrightarrow S(x)=S(y))$: S is an injection.
• $\forall x\in N(S(x)\neq 0)$: There is no natural number who's successor is zero.
• $\forall X(0\in X\land \forall x\in \mathbb {N} (x\in X))\rightarrow \mathbb {N} \subseteq X$: If K is a set such that 0 is in K, and for every natural number n, n being in K implies that S(n) is in K, then K contains every natural number.
• A weakened induction scheme for $L_{ID_{\nu }}$ formulas.
• $TI(\prec ,F)$ expresses transfinite induction along $\prec$ for an arbitrary $L_{ID_{\nu }}$ formula $F$.
• $\forall \mu \prec \nu ;A^{\mu }(J_{A}^{\mu })\subseteq J_{A}^{\mu }$ for an arbitrary $L_{ID_{\nu }}$ formula $F$.
• $\forall \mu \prec \nu ;A^{\mu }(F)\subseteq F\rightarrow J_{A}^{\mu }\subseteq F$ for an arbitrary $L_{ID_{\nu }}$ formula $F$.

In this weakened version, $I_{A}$ is just a fixed point, not necessarily the least fixed point, of the operator $\Gamma _{A}$.