算術体系と concatenation の体系
堀畑 佳宏（Yoshihiro HORIHATA）
東北大学大学院理学研究科
本研究では，文字列の結合，つまり concatenation に関する新たな理論 WTC を構築し，この理論が，Tarski ら [8] によって導入された非常に弱い，しかし本質的決定不可能な算術 R と互いに翻訳可能であることを証明した．この系として，WTC も本質的決定不可能であることが導ける．

1 concatenation に関する理論について
文字列の concatenation に関する理論 TC は，2005 年に A. Grzegorczyk[2] によって導入された．TC の言語は (_ , ε, α, β) で，以下の公理を持つ：(TC1) ∀x(x_ ε = ε_ x = x)(TC2) ∀x∀y∀z(x_ (y _ z) = (x_ y)_ z)(TC3) ∀x∀y∀u∀v(x_ y = u_ v → ∃w((x_ w = u ∧ y = w_ v) ∨ (x = u_ w ∧ w_ y = v)))
(TC4) α 6= ε ∧ ∀x∀y(x_ y = α → x = ε ∨ y = ε)(TC5) β 6= ε ∧ ∀x∀y(x_ y = β → x = ε ∨ y = ε)(TC6) α 6= β

Grzegorczyk はその論文で，TC が決定不可能であることを証明している．ここで理論 T が決定不可能であるとは，T の言語における全ての論理式に対しそれが T で証明可能であるかそうでないかを判定するアルゴリズムが存在しないことをいう．

TC に関する研究は活発に行われ，2008 年には Grzegorczyk と K. Zdanowski[3] によって，TC が本質的決定不可能であることが証明された．ここで理論 T が本質的決定不可能であるとは，T の無矛盾で r.e. な拡大理論は全て決定不可能であることをいう．さらに，2009 年には，
TC と Robinson 算術 Q（Peano 算術 PA から帰納法を抜いた算術）が互いに翻訳可能である
ことが，A. Visser および S. Rachel[10, 6]，V. Svejdar[7]，M. Ganea[1] らによって独立に証明された．この結果は，Q が本質的決定不可能であることが良く知られているので，本質的決定不可能性が翻訳によって保存されることから，TC の本質的決定不可能性を系として導く．

2 本研究における結果
本研究では，Q よりも真に弱い算術 R に着目した．算術 R は Robinson ら [8] によって導入された理論で，以下の公理をもつ：ただし言語は (+, ·, S, 0) とする．
(R1) n̄ + m̄ = n + m(R2) n̄ · m̄ = n · m(R3) n̄ 6= m̄ for n 6= m
(R4) ∀x(x ≤ n̄ → x = 0̄ ∨ · · · ∨ x = n̄)(R5) ∀x(x ≤ n̄ ∨ n̄ ≤ x)1

ただし，不等号は x ≤ y ≡ ∃z(x + z = y) で定義し，numeral を 0̄ = 0，n + 1 = S(n̄) と再帰的に定義する．Robinson らによって R が本質的決定不可能であることが示されている [8]．
さらに Cobham によって，R から (R5) を外した算術 R0 が R と互いに翻訳可能であること，従って R0 も本質的決定不可能であることが示されている（[9] を参照）
．一方，R0 からどれか一つでも公理図式を外した算術が本質的決定不可能でないことも示されている [5]．このように，算術 R は，「どれくらい弱い算術で第一不完全性定理が導けるか」という観点において特に興味をもたれている．
本研究では，次の公理をもつ concatenation に関する理論 WTC を新たに導入した：(WTC1)∀x v u(x_ ε = ε_ x = x)

(WTC2)∀x∀y∀z[[x_ (y _ z) v u ∨ (x_ y)_ z v u] → x_ (y _ z) = (x_ y)_ z](WTC3)∀x∀y∀s∀t[(x_ y = s_ t ∧ x_ y v u) → ∃w((x_ w = s ∧ y = w_ t) ∨ (x = s_ w ∧ w_ y = t))]

(WTC4)

α 6= ε ∧ ∀x∀y(x_ y = α → x = ε ∨ y = ε)

(WTC5)

β 6= ε ∧ ∀x∀y(x_ y = β → x = ε ∨ y = ε)(WTC6)

γ 6= ε ∧ ∀x∀y(x_ y = γ → x = ε ∨ y = ε)(WTC7)

α 6= β ∧ β 6= γ ∧ γ 6= α

この理論に対し，本発表の主結果である以下の定理を導いた：
定理 1 ([4]) WTC は R と互いに翻訳可能である．
この定理から，WTC が本質的決定不可能であること，また WTC が TC を翻訳できないことも示される．さらに，この定理と Visser[11] による結果を合わせると次が得られる：
定理 2 ([4]) 理論 T が WTC で翻訳可能であることと，T が局所的有限充足可能であること，つまり T の有限部分理論は有限モデルをもつこと，は同値である．
本研究では，今回構成した R の WTC への翻訳の構成手法を応用し，また，言語の異なる理論間の強弱を測れるという翻訳の利点を用いて，算術やそれ以外の諸理論の強さを調べ比較する．さらに，そこで得た翻訳可能であることの特徴の蓄積を利用し，逆に翻訳できないことの特徴の模索およびその証明手法を確立したい．

参考文献[1] M. Ganea. Arithmetic on semigroups. The Journal of Symbolic Logic, 74(1):265–278, 2009.
[2] A. Grzegorczyk. Undecidability without arithmetization. Studia Logica, 79(1):163–230, 2005.
[3] A. Grzegorczyk and K. Zdanowski. Undecidability and concatenation. In V. W. Marek A. Ehrenfeucht andM. Srebrny, editors, Andrzej Mostowski and foudational studies, pages 72–91. IOS Press, 2008.
[4] Y. Horihata. Interpretations between weak theories of concatenation and arithmetic. preprint.
[5] J. P. Jones and J. C. Shepherdson. Variants of robinson’s essentially undecidable theory R. Archive for Math.
Logic, 23:65–77, 1983.
[6] Sterken Rachel. Concatenation as a basis for Q and the intuitionistic varient of Nelson’s classic result. Master’sthesis, Universiteit van Amsterdam, October 2008.
[7] V. Svejdar. On interpretability in the theory of concatenation. Nortre Dame Journal of Formal Logic, 50(1):87–95, 2009.
[8] A. Tarski, A. Mostowski, and R. M. Robinson. Undecidable theories. North-Holland, 1953.
[9] R. L. Vaught. On a theorem of cobham concerning undecidable theories. In E. Negel, P. Suppes, and A. Tarski,editors, Logic, Methodology, and Philosophy of Science. Stanford University Press, 1962.
[10] A. Visser. Growing commas – a study of sequentiality and concatenation. Nortre Dame Journal of Formal
Logic, 50(1):61–85, 2009.
[11] A. Visser. Why the theory R is special. preprint, August 10, 2009.

2