本質的決定不能性
定義
理論$ Tが本質的に決定不能であるとは,任意の$ Tの無矛盾な再帰的可算拡大理論$ T'が全て決定不能になることである.
ここでの決定不能とは: 理論の決定可能性
$ Tの言語における任意の論理式$ \varphiが$ T \vdash \varphiか$ T \nvdash \varphiのどちらか?をを有限時間で判定するアルゴリズムが存在しないことを指す.
本質的に決定不能な理論の一覧
Robinson算術$ \sf Q
Tarski-Mostowski-Robinson算術$ \sf R
Alfred Tarski, A. Mostowski, M. Robinson; "Undecidable Theories"
Cobhamの最弱の算術$ \sf R_0
R. L. Vaught; "On a Theorem of Cobham Concerning Undecidable Theories"
Jones-Shaperdsonの最弱の算術$ \sf R_1
J. P. Jones, J. C. Shepherdson; "Variants of Robinson’s essentially undecidable theory R"
連結の理論$ \sf TC
A. Grzegorczyk, K. Zdanowski; "Undecidability and concatenation"
弱い連結の理論$ \sf WTC
H. Yoshihiro; "算術体系とconcatenationの体系"
Memo
理論の解釈可能性$ \rhdとする.
$ Uを本質的に決定不能な理論とすると,$ U \rhd Tなら$ Tは本質的に決定不能になる.
example:
連結の理論$ \sf TCの本質的決定不能性は,Robinson算術$ \sf Qとの間で$ \sf TC \lhd\rhd Qであることが分かったので系として得られている.
S. Rachel; "Concatenation as a basis for Q and the intuitionistic varient of Nelson’s classic result"
V. Svejdar; "On interpretability in the theory of concatenation"
M. Ganea; "Arithmetic on semigroups"
Thm. Alfred Tarski, A. Mostowski, M. Robinson; "Undecidable Theories"による
$ Uが無矛盾で,$ U \rhd Tだとする.
$ Tは本質的に決定不能ならば$ Uは決定不能.
更に,$ Uが再帰的公理化可能なら,$ Uは不完全.
remark:
T. Kurahashi; "不完全性定理の数学的発展"では$ Uが$ \Sigma_1定義可能であるという条件だったが本当に同値かはちょっと怪しい