p.c.
piecewise coded
論理式の有限の断片をコードした数がそれぞれ存在する
定義
ここで$ \varphi(\vec x)はパラメータを含んでいてもよい 明記されているわけではないが、そうでないとのちに行うような「$ \Delta_n^\bullet集合はp.c.」などの主張が意味を為さない $ \mathrm{code}_\varphi(f,m) \coloneqq \mathrm{mapping}(f) \land \mathrm{rng}(f) = 2 \land (\forall \vec x \le m)[(f(\vec x) = 1) \equiv \varphi(\vec x)]
$ \mathrm{p.c.}\varphi \coloneqq (\forall m)(\exists f)[\mathrm{code}_\varphi(f,m)]
$ n \ge 1とする
そうでないと$ \mathsf I\Sigma_nが列を扱えないので...
ところで，
$ \mathrm{p.c.}\varphi \coloneqq (\forall m)(\exists f)[\mathrm{code}_\varphi(f,|m|)]
補題 2.13
$ \Sigma_n論理式$ \varphiについて
$ \mathsf I\Sigma_n \vdash \mathrm{p.c.}\varphi
Proof.
$ \varphiが$ k変数の論理式だとする
$ \Psi(\hat q, \hat z) \coloneqq \text{$\hat q$ is a mapping from $(<\hat z)^k$ to $\{0,1\}$} \land (\forall \vec x < \hat z)[\varphi(\vec x) \to f(\vec x) = 1]
は$ \mathsf I\Sigma_nで$ \Pi_n
よって$ \hat q 上のの最小原理$ \mathsf L_{\hat q} \Psi(\hat q, \hat z) \in \mathsf L\Pi_n により$ (\forall z)(\exists_\mathrm{minimum} q_z)[\Psi(q_z,z)] 定関数$ q_z(\vec x) \coloneqq 1とするとこれは$ \Psi(q_z,z)を満たす
このときあらゆる$ zについて$ \mathrm{code}_\varphi(q_z, z)
$ (\vec x \le z)[\lnot \varphi(\vec x) \to q_z(\vec x) = 0] を示せばよい
$ \vec x: \lnot \varphi(\vec x)を固定する. $ q_z(\vec x) = 1と仮定する
$ q_z'(\vec y) \coloneqq \begin{cases} 0 & \text{if $\vec y = \vec x$} \\ q_z(\vec y) & \text{o.w.} \end{cases}
とすると$ \Psi(q_z',z)かつ$ q_z' < q_z.
$ q_zの最小性に矛盾
定理 2.7
$ \Sigma_0^{\Sigma_n}論理式$ \varphiについて
$ \mathsf I\Sigma_n \vdash \mathrm{p.c.}\varphi
Proof.
$ \Sigma_0^{\Sigma_n}論理式の構成に関するメタ帰納法
定理 2.7
$ \mathsf B\Sigma_{n+1}で$ \Delta_{n+1}である論理式$ \varphiについて
$ \mathsf B\Sigma_{n+1} \vdash \mathrm{p.c.}\varphi
Proof
補題 2.13 と同様に行う
よって定理：BΣn+1 = LΔn+1より$ \mathsf L_q\Psi(q,z) より$ (\forall z)(\exists_\mathrm{minimum} q_z)[\Psi(q_z,z)] を得る あとは2.13と同様
観察
$ \mathsf L\Sigma_n = \mathsf L\Pi_n = \mathsf I\Sigma_n
$ \mathsf L\Delta_{n+1} = \mathsf B\Sigma_{n+1}
で上の証明が行われている