日記 2021/03/27 - ボケ日記

帰納定理の拡張

$\displaystyle{ \forall S \forall a \in S; (\forall f : N \times S \rightarrow S; \exists ! g: N \rightarrow S (g(0)=a \land \forall x \in N; g(x') = f(x, g(x))) ) }$

を示した。
それから直ちに得られる

$\displaystyle{ M(n) =\{x | x \in N \land x \leq n \} とすると、\\ \forall S \forall a \in S; \forall n \in N; (\forall f : M(n) \times S \rightarrow S; \exists ! g : M \rightarrow S; (g(0)=a \land \forall x \in N; g(x') = f(x, g(x))) ) }$

も示した。
また、累積帰納法に対応する形の

$\displaystyle{ \forall S \forall f : \bigcup_{x \in N} S^{N(x)} \rightarrow S; \exists ! g : N \rightarrow S; (\forall x \in N; g(x) = F(g \upharpoonright N(x) )) }$

も示した( $\upharpoonright$ は写像の縮小(定義域を縮めたやつ))。疲れた。