真の算術のソースを表示

[[数理論理学]]において、'''真の算術''' ({{lang-en-short|true arithmetic}}) とは一階[[ペアノ算術]]の[[シグネチャ (論理学)|言語]]における[[自然数]]の[[理論 (数理論理学)|理論]] Th(<math>\mathcal{N}</math>) のことである<ref>{{Harvnb|Boolos|Burgess|Jeffrey|2002|p=295}}</ref>。[[タルスキの定義不可能性定理]]はこの理論が算術的に定義不可能であることを示している。

== 定義 ==
[[ペアノ算術]]の[[シグネチャ]]には加法、乗法および後者関数の関数記号、「等しい」と「より小さい」の関係記号、および0の定数記号が含まれる。このシグネチャにおける論理式は[[一階述語論理]]の通常のやり方で構築される。'''一階述語論理の言語'''はこのシグネチャにおけるすべての論理式からなる。 

[[構造 (数理論理学)|構造]] <math>\mathcal{N}</math> はペアノ算術のモデルであり、以下のように定義される:
* [[議論領域]]は自然数の集合 <math>\mathbb{N}</math> である。
* 記号0は数0と解釈される。
* 関数記号は <math>\mathbb{N}</math> 上での通常の算術演算と解釈される。
* 「等しい」と「より小さい」の関係記号は <math>\mathbb{N}</math> 上での通常の等値および順序関係と解釈される。
この構造は一階算術の[[算術の非標準モデル|標準モデル]]もしくは[[意図した解釈]]として知られる。

一階算術の言語における[[文 (数理論理学)|文]]は、いま定義した構造において真であるとき <math>\mathcal{N}</math> において真であるという。表記法 <math>\mathcal{N} \models \varphi</math> は、文 &phi; が <math>\mathcal{N}</math> において真であることを示すために使われる。

'''真の算術'''は一階算術の言語における文のうち <math>\mathcal{N}</math> において真であるものすべての集合 {{nowrap|1=Th(<math>\mathcal{N}</math>)}} である。この集合は構造 <math>\mathcal{N}</math> の (完全な) 理論と同値である<ref>[[:en:Theory (mathematical logic)#Theories associated with a structure|theories associated with a structure]]を参照。</ref>。


== 算術の定義不可能性 ==
真の算術での中心的な結果は、[[アルフレト・タルスキ]] (1936) の[[タルスキの定義不可能性定理|定義不可能性定理]]である。この定理は集合 {{nowrap|1=Th(<math>\mathcal{N}</math>)}} が算術的に定義可能でないと述べる。これは一階算術のシグネチャに以下のような「万能論理式」 <math>\varphi(x)</math> が存在しないという意味である: このシグネチャにおける任意の文 <math>\theta</math> に対して、
:<math>\mathcal{N} \models \theta \qquad</math> if and only if <math>\mathcal{N} \models \varphi(\underline{\#(\theta)}).</math>
ここで <math>\underline{\#(\theta)}</math> は文 ''<math>\theta</math>'' の正規[[ゲーデル数]]の数字である。

[[ポストの定理]]は定義不可能性定理のよりシャープなバージョンであり、[[算術的階層]]を使って {{nowrap|1=Th(<math>\mathcal{N}</math>)}} の定義可能性と[[チューリング次数]]の間の関係を示す。自然数 ''n'' ごとに、算術的階層における <math>\Sigma^0_n</math> 以下の文のみからなる {{nowrap|1=Th(<math>\mathcal{N}</math>)}} の部分集合を {{nowrap|1=Th<sub>''n''</sub>(<math>\mathcal{N}</math>)}} とする。ポストの定理によって、''n'' ごとに、{{nowrap|1=Th<sub>''n''</sub>(<math>\mathcal{N}</math>)}} は算術的に定義可能であるが、<math>\Sigma^0_n</math> より複雑性が高い論理式によってのみ可能であることが示される。したがって単一の論理式で {{nowrap|1=Th(<math>\mathcal{N}</math>)}} を定義することはできない。なぜならば
:<math>\mbox{Th}(\mathcal{N}) = \bigcup_{n \in \mathbb{N}} \mbox{Th}_n(\mathcal{N})</math>
だが、いかなる単一の論理式も任意の大きな ''n'' に対して {{nowrap|1=Th<sub>''n''</sub>(<math>\mathcal{N}</math>)}} を定義できないからである。

== 計算可能性の性質 ==
上記で論じたように、タルスキの定理によれば {{nowrap|1=Th(<math>\mathcal{N}</math>)}} は算術的に定義不可能である。ポストの定理の系によって {{nowrap|1=Th(<math>\mathcal{N}</math>)}} の[[チューリング次数]]は '''0'''<sup>&omega;</sup> となり、そのため {{nowrap|1=Th(<math>\mathcal{N}</math>)}} は[[帰納的集合|決定可能]]でも[[帰納的可算集合|帰納的可算]]でもない。

{{nowrap|1=Th(<math>\mathcal{N}</math>)}} は[[半順序]]のシグネチャにおいて、帰納的可算[[チューリング次数]]の理論 {{nowrap|1=Th(<math>\mathcal{R}</math>)}} と密接な関係がある<ref>{{Harvnb|Shore|2011|p=184}}</ref>。とくに、以下のような ''S'' および ''T'' が存在する:
* 一階算術のシグネチャにおけるそれぞれの文 &phi; について、S(&phi;) が {{nowrap|1=Th(<math>\mathcal{R}</math>)}} に属するとき、かつそのときに限り &phi; は {{nowrap|1=Th(<math>\mathcal{N}</math>)}} に属する。
* 半順序のシグネチャにおけるそれぞれの文 &psi; について、T(&psi;) が {{nowrap|1=Th(<math>\mathcal{N}</math>)}} に属するとき、かつそのときに限り &psi; は {{nowrap|1=Th(<math>\mathcal{R}</math>)}} に属する。

== モデル理論的性質 ==
真の算術は[[安定な理論|不安定な理論]]であり、そのため非可算濃度 <math>\kappa</math> ごとに <math>2^\kappa</math> 個のモデルを持つ。この理論は[[完全な理論|完全]]なので、そのすべてのモデルは[[初等的同値]]である。

== 二階算術の真の理論 ==
二階算術の真の理論は[[二階算術]]の言語において二階算術の標準モデルによって充足されるすべての文からなる。二階算術の標準モデルはその一階部分が構造 <math>\mathcal{N}</math> であり、その二階部分が <math>\mathbb{N}</math> のすべての部分集合からなる。

一階算術の真の理論 {{nowrap|1=Th(<math>\mathcal{N}</math>)}} は二階算術の真の理論の部分集合であり、{{nowrap|1=Th(<math>\mathcal{N}</math>)}} は二階算術で定義可能である。しかし、ポストの定理の[[解析的階層]]への一般化により、二階算術の真の理論は二階算術のいかなる単一の論理式によっても定義可能でないことが示される。

{{Harvtxt|Simpson|1977}} は二階算術の真の理論は、半順序のシグネチャにおいて、すべての[[チューリング次数]]の半順序の理論と計算可能な解釈が可能であり、''その逆も成り立つ''ことを示した。

== 脚注 ==
{{脚注ヘルプ}}
{{Reflist|2}}

== 参考文献 ==
* {{citation
 | last1=Boolos
 | first1=George
 | last2=Burgess
 | first2=John P.
 | last3=Jeffrey
 | first3=Richard C.
 | title=Computability and logic
 | edition=4th
 | publisher=Cambridge University Press
 | year=2002
 | isbn=978-0-521-00758-0
}}.
* {{Citation
 | last1=Bovykin
 | first1=Andrey
 | last2=Kaye
 | first2=Richard
 | chapter=On order-types of models of arithmetic
 | year=2001
 | editor-last=Zhang
 | editor-first=Yi
 | title=Logic and algebra
 | series=Contemporary Mathematics
 | volume=302
 | publisher=American Mathematical Society
 | publication-date=2001
 | pages=275&ndash;285
 | isbn=978-0-8218-2984-4
 }}.
* {{Citation
 | last1=Shore
 | first1=Richard
 | chapter=The recursively enumerable degrees
 | year=2011
 | editor-last=Griffor
 | editor-first=Edward R.
 | title=Handbook of Computability Theory
 | series=Studies in Logic and the Foundations of Mathematics
 | volume=140
 | publisher=North-Holland
 | publication-date=1999
 | pages=169&ndash;197
 | isbn=978-0-444-54701-9
 }}.
* {{Citation
 | last1=Simpson
 | first1=Stephen G.
 | title=First-order theory of the degrees of recursive unsolvability
 | id={{MathSciNet | id = 0432435}}
 | year=1977
 | journal=[[Annals of Mathematics|Annals of Mathematics. Second Series]]
 | issn=0003-486X
 | volume=105
 | pages=121–139
 | doi=10.2307/1971028
 | url=http://jstor.org/stable/1971028
 | issue=1
 | publisher=Annals of Mathematics
}}
* Tarksi, Alfred (1936), "Der Wahrheitsbegriff in den formalisierten Sprachen". An English translation "The Concept of Truth in Formalized Languages" appears in {{Citation
 | editor-last=Corcoran
 | editor-first=J.
 | title=Logic, Semantics and Metamathematics: Papers from 1923 to 1938
 | year=1983
 | edition=2nd
 | publisher=Hackett Publishing Company, Inc.
 | isbn=978-0-915144-75-4
}}

== 外部リンク ==
*{{MathWorld|title=Arithmetic|urlname=Arithmetic}}
*{{MathWorld|title=Peano Arithmetic|urlname=PeanoArithmetic}}
*{{MathWorld|title=Tarski's Theorem|urlname=TarskisTheorem}}

{{DEFAULTSORT:しんのさんしゆつ}}
[[Category:算術の形式理論]]
[[Category:モデル理論]]
[[Category:数学に関する記事]]