Peano算術の原始再帰関数に対しての保存的拡大について
証明が終わっていない
参考文献
主張
関数$ \mathsf{f}:\N^k \to \Nが原始再帰関数であるとする．
算術の言語$ \mathscr{L}_\mathsf{A}に，$ k変項関数記号$ fを追加した言語$ \mathscr{L}_{\mathsf{A}+f}とする．
$ f(\vec{\bar{x}}) = \bar{y} \iff \mathsf{f}(\vec{x}) = yが守られている適当な公理を追加した，言語$ \mathscr{L}_{\mathsf{A}+f}上の任意の$ \sf PAの拡大理論$ \sf PA+fは$ \sf PAの保存的拡大になる．
すなわち，あらゆる原始再帰関数（を表す記号）が$ \sf PAに最初から入っていると仮定しても証明可能性や表現可能性には問題を及ぼさない．
例えば，普通はPeano算術にべき乗は入ってないが入れても構わない．べき乗は原始再帰関数として表すことができるから． 言語$ \mathscr{L}上の適当な理論$ T, T'とする．
$ \mathscr{L}の文$ \sigmaに対し以下が成り立つとき，$ T'は$ Tの保存的拡大という．
$ T \vdash \sigma \iff T' \vdash \sigma
メモ
$ T'の言語は$ \mathscr{L}とは違っても良い．ただし，$ Tが$ \mathscr{L}'の理論であるなら$ \mathscr{L} \sube \mathscr{L}'でなくてはならない．
$ xを自由変項とする任意の論理式$ \varphi(x)に対し，$ \Sigma_1論理式$ {\exists!}_x \varphi(x)を↓とする．
$ {\exists!}_x \varphi(x) \equiv \exists_x\lbrack \varphi(x) \land \forall_{y,y'}\lbrack\varphi(y) \land \varphi(y') \to y = y\rbrack \rbrack
Thm 1
$ \mathscr{L}の論理式$ \varphi(\vec{x},y)は$ \vec{x},y以外に自由変項を持たないとする．また，$ \vec{x} \coloneqq x_1,\dots,x_kとする．
$ \mathscr{L}に新しく$ kアリティ関数記号$ fを追加した言語を$ \mathscr{L}'とする．
$ \mathscr{L}'の理論$ T \coloneqq T + \forall_{\vec{x}}\varphi(\vec{x},f(\vec{x}))とする．
$ T \vdash \forall_{\vec{x}}\exists_y\varphi(\vec{x},y)なら$ T'は$ Tの保存的拡大．
Cor 1
$ T' \coloneqq T + \forall_{\vec{x}}\forall_y(\varphi(\vec{x},y) \leftrightarrow f(\vec{x}) = y)とする．
$ T \vdash \forall_{\vec{x}}{\exists!}_y\varphi(\vec{x},y)なら$ T'は$ Tの保存的拡大．
proof:Thm.1より明らか．
Cor 2
1. $ T \vdash \forall_{\vec{x}}{\exists!}_y\varphi(\vec{x},y)ならば，関数記号$ fを含みうる言語$ \mathscr{L}'の論理式$ \psiから，関数記号$ fを取り除いた論理式$ \psi^{-f}を構成することができる．
$ \psi^{-f}は$ \mathscr{L}の論理式と考えることができる．
Cor 3
$ T \vdash \forall_{\vec{x}}{\exists!}_y\varphi(\vec{x},y)ならば，理論$ Tの言語に$ \varphi(\vec{x},f(\vec{x}))を満たすような関数記号$ fを適当に導入して議論しても，$ Tの証明可能性や表現可能性などには影響を及ぼさない．
多分?
Peano算術は任意の原始再帰的関数$ f(\vec{x})のグラフ$ F(\vec{x},y) \iff y = f(\vec{x})を表現できる． したがってPeano算術$ \sf{PA}に任意の原始再帰関数$ fを表す記号及びその公理を導入しても構わない．
メモ
$ fが原始再帰関数であるとき，$ fは$ Tにおいて可証再帰的．