9 再帰

9.1 自然数上の再帰定理

自然数の上で、各段の値を前の値から決める写像が在る。\(G\) を「\(\langle n, x\rangle\) に値 \(y\) を対応させる」対応（\(\langle\langle n, x\rangle, y\rangle\) の集合）とし、\(c\) を最初の値とする。最小の閉じた集合を \(f\) として、\(n\) についての帰納法で、各 \(n\) にただ1つの値が対応することを示す（REC）。
word(ss,s)F … \(\)
ap. … \(f \in X \to Y , x \in X \Longrightarrow \langle x , f ( x ) \rangle \in f\)
REC … \(G \subset ( \mathbb{M} \times A ) \times A , \forall n \in \mathbb{M} . \forall x \in A . \exists! y \, \langle \langle n , x \rangle , y \rangle \in G , c \in A \Longrightarrow \exists f \, ( f \in \mathbb{M} \to A , \langle 0 , c \rangle \in f , \forall n \in \mathbb{M} . \forall x , y \, ( \langle n , x \rangle \in f , \langle \langle n , x \rangle , y \rangle \in G \Longrightarrow \langle ( n + 1 ) , y \rangle \in f ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
値の形：\(f(0) = c\)、\(f(n+1) = y\)（\(y\) は \(G\) が \(\langle n, f(n)\rangle\) に対応させる値）。
RECap … \(G \subset ( \mathbb{M} \times A ) \times A , \forall n \in \mathbb{M} . \forall x \in A . \exists! y \, \langle \langle n , x \rangle , y \rangle \in G , c \in A \Longrightarrow \exists f \in ( \mathbb{M} \to A ) . ( f ( 0 ) = c , \forall n \in \mathbb{M} . \forall y \, ( \langle \langle n , f ( n ) \rangle , y \rangle \in G \Longrightarrow f ( ( n + 1 ) ) = y ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，ap.

9.2 パラメータ付きの再帰定理

上の再帰定理に、パラメータ \(p \in P\) をつけた形。\(\langle p, n\rangle\) ごとに値を決める（二重の添字 \(s(n)(m)\) を対の \(s(\langle n, m\rangle)\) として作るのに使う）。
REC2 … \(G \subset ( ( P \times \mathbb{M} ) \times A ) \times A , \forall p \in P . \forall n \in \mathbb{M} . \forall x \in A . \exists! y \, \langle \langle \langle p , n \rangle , x \rangle , y \rangle \in G , c \in A \Longrightarrow \exists f \, ( f \in ( P \times \mathbb{M} ) \to A , \forall p \in P . \langle \langle p , 0 \rangle , c \rangle \in f , \forall p \in P . \forall n \in \mathbb{M} . \forall x , y \, ( \langle \langle p , n \rangle , x \rangle \in f , \langle \langle \langle p , n \rangle , x \rangle , y \rangle \in G \Longrightarrow \langle \langle p , ( n + 1 ) \rangle , y \rangle \in f ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
値の形：\(f(\langle p, 0\rangle) = c\)、\(f(\langle p, n+1\rangle) = y\)（\(y\) は \(G\) が \(\langle\langle p, n\rangle, f(\langle p, n\rangle)\rangle\) に対応させる値）。
RECap2 … \(G \subset ( ( P \times \mathbb{M} ) \times A ) \times A , \forall p \in P . \forall n \in \mathbb{M} . \forall x \in A . \exists! y \, \langle \langle \langle p , n \rangle , x \rangle , y \rangle \in G , c \in A \Longrightarrow \exists f \in ( ( P \times \mathbb{M} ) \to A ) . ( \forall p \in P . f ( \langle p , 0 \rangle ) = c , \forall p \in P . \forall n \in \mathbb{M} . \forall y \, ( \langle \langle \langle p , n \rangle , f ( \langle p , n \rangle ) \rangle , y \rangle \in G \Longrightarrow f ( \langle p , ( n + 1 ) \rangle ) = y ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，ap.

9.3 写像の補題

写像の値は一意（Lfu・Lfap）。値を1点だけ変えた写像が在る（UPD）。先頭に1項を足した写像が在る（SEQ）。
Lfu … \(f \in X \to Y , \langle z , u \rangle \in f , \langle z , v \rangle \in f \Longrightarrow u = v\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ap.
Lfap … \(f \in X \to Y , x \in X , \langle x , y \rangle \in f \Longrightarrow f ( x ) = y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ap.
UPD … \(f \in ( X \to Y ) , k \in X , p \in Y \Longrightarrow \exists g \in ( X \to Y ) . ( g ( k ) = p , \forall i \in X . ( i \neq k \Longrightarrow g ( i ) = f ( i ) ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ap.
SEQ … \(f \in ( \mathbb{M} \to A ) , p \in A \Longrightarrow \exists g \in ( \mathbb{M} \to A ) . ( g ( 0 ) = p , \forall i \in \mathbb{M} . g ( ( i + 1 ) ) = f ( i ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，ap. ，=_.
定数写像は写像（Lcst）。
Lcst … \(c \in B \Longrightarrow ( A \times \{ c \} ) \in ( A \to B )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ap.