Oreyの定理
証明述語$ \mathrm{Proof}_T(x,y)を一つ固定する． $ \varphiを$ \Pi_1文とし，$ \mathcal{N} \models \varphiかつ$ T \vdash \varphi \to \mathrm{Con}_Tとする．
このとき，別の証明述語$ \mathrm{Proof}'_T(x,y)が取れて，$ T \vdash \varphi \leftrightarrow \mathrm{Con}'_T． 意義
例えば，$ Tを$ \mathsf{PA}，$ \varphiを$ \mathrm{Con}_\mathsf{ZFC}とする．
理論としての強さは$ \mathsf{PA} \leq \mathsf{ZFC}なので，$ \mathsf{PA} \vdash \mathsf{Con}_\mathsf{ZFC} \to \mathsf{Con}_\mathsf{PA}が言える．
$ \mathcal{N} \vDash \mathrm{Con}_\mathsf{ZFC}なら，Oreyの定理より，$ \mathsf{PA} \vdash \mathrm{Con}_\mathsf{ZFC} \leftrightarrow \mathrm{Con}'_\mathsf{PA}となるような証明述語が取れる．
つまり
素朴には無矛盾性の強さが違いそうな$ \sf PAと$ \sf ZFCであっても，その形式的無矛盾性に関しては算術化の方法によっては$ \sf PA上で同値になることもある．
あるいは無矛盾性の強さが同じであっても，その形式的無矛盾性は同値にならない，ということもある．
形式的無矛盾性の強さは算術化の方法に強く依存する，ということを意味している．
refernce