超限帰納法

$ (\forall\alpha\in X:(\forall \beta\in X_{<\alpha}:P(\beta))\implies P(\alpha))\implies\forall\alpha\in X:P(\alpha)

証明

狭義の背理法を使う

$ \forall\alpha\in X:(\forall \beta\in X_{<\alpha}:P(\beta))\implies P(\alpha)

$ \implies (

$ \{x\in X|\lnot P(x)\}\neq\varnothing

$ \implies\exist m\in\{x\in X|\lnot P(x)\}\forall x\in\{x\in X|\lnot P(x)\}:m\le x

$ \implies\exist m\in X:\lnot P(m)\land((\forall \beta\in X_{<m}:P(\beta))\implies P(m))\land\forall x\in\{x\in X|\lnot P(x)\}:m\le x

$ \implies\exist m\in X:(\exist\beta\in X_{< m}:\lnot P(\beta))\land\forall x\in\{x\in X|\lnot P(x)\}:m\le x

$ \implies\exist m\in X\exist\beta\in X_{< m}:\lnot P(\beta)\land m\le\beta

$ \implies\bot

$ )

$ \implies\{x\in X|\lnot P(x)\}=\varnothing

$ \underline{\therefore\iff\forall x\in X:P(x)\quad}_\blacksquare

$ f(\min A)=\varnothing

$ \forall x\in A\forall y\in A_{<x}:f(y)\in f(x)

References