二階述語論理のソースを表示

'''二階述語論理'''（にかいじゅつごろんり、{{lang-en-short|second-order predicate logic}}）あるいは単に'''二階論理'''（にかいろんり、{{lang-en-short|second-order logic}}）は、[[一階述語論理]]を拡張した論理体系であり、一階述語論理自体も[[命題論理]]を拡張したものである<ref>Shapiro (1991) と Hinman (2005) に詳しい定義と紹介がある。</ref>。二階述語論理もさらに[[高階述語論理]]や[[型理論]]に拡張される。

一階述語論理と同様に[[議論領域]]（ドメイン）の考え方を使う。ドメインとは、[[量化]]可能な個々の元の集合である。一階述語論理では、そのドメインの個々の元が変項の値となり、量化される。例えば、一階の論理式 ∀''x'' (''x'' ≠ ''x'' + 1) では、変項 ''x'' は任意の個体を表す。二階述語論理は個体の集合を変項の値とし、量化することができる。例えば、二階の論理式 ∀''S'' ∀''x'' (''x'' ∈ ''S'' ∨ ''x'' ∉ ''S'') は、個体の全ての集合 ''S'' と全ての個体 ''x'' について、''x'' が ''S'' に属するか、あるいは属さないかのどちらかであるということを主張している。最も一般化された二階述語論理は関数の量化をする変項も含んでいる（詳しくは後述）。

== 二階論理の表現能力 ==
二階述語論理は一階述語論理よりも表現能力が高い。例えば、ドメインが全ての[[実数]]の集合としたとき、一階述語論理を使って「それぞれの実数には加法の逆元が存在する」ということを ∀''x'' ∃''y'' (''x'' + ''y'' = 0) と表せる。しかし、「空でなく上に有界な実数の集合があるとき常にその集合には上限が存在する」という命題を表すには、二階述語論理が必要となる。ドメインが全ての実数の集合としたとき、次の二階の論理式がこの命題を表している。
: <math>\forall A \Big[(\exists w (w \in A) \land \exists z\,\forall w ( w \in A \rightarrow w \leq z)) \rightarrow  \exists x\,\forall y  ([\forall w (w \in A \rightarrow w \leq y)] \leftrightarrow x \leq y)\Big].</math>

二階述語論理では、「ドメインは有限である」とか「ドメインは[[可算無限集合]]の[[基数|濃度]]である」といった文も形式的に表現可能である。ドメインが有限であるというには、そのドメインから同じドメインへの全ての[[単射]]関数が[[全射]]であることを論理式で表せばよい。ドメインが可算無限集合の濃度であることをいうには、そのドメインの任意のふたつの無限部分集合間に[[全単射]]があることを論理式で表せばよい。一階述語論理ではこれら（「有限集合であること」や、「可算集合であること」）を表現できないことが、[[レーヴェンハイム-スコーレムの定理]]から導かれる。

== 文法 ==
二階述語論理の文法から、どの式が[[well-formed formula|論理式]]かが示される。一階述語論理の文法に加えて、二階述語論理では変項に様々な「種（sort）」または「型（type）」がある。
* 個体の集合を値とする変項。''S'' をこの種の変項とし、一階の項 ''t'' があるとき、式 ''t'' ∈ ''S'' は[[原子論理式]]である（''S''(''t'') あるいは ''St'' とも書かれる）。個体群の集合はドメインの[[単項関係]]と見ることもできる。
* 任意の自然数 ''k'' について、個体の全ての ''k''-項関係を値とする変項。''R'' をそのような''k''-項関係の変項とし、一階の項 ''t''<sub>1</sub>,..., ''t''<sub>''k''</sub> があるとき、式 ''R''(''t''<sub>1</sub>,...,''t''<sub>''k''</sub>) は原子論理式である。
* 任意の自然数 ''k'' について、ドメインの ''k'' 個の元を引数として1つの元を値とする関数を値とする変項。''f'' をそのような''k''引数の関数シンボルとし、一階の項 ''t''<sub>1</sub>,...,''t''<sub>''k''</sub> があるとき、式 ''f''(''t''<sub>1</sub>,...,''t''<sub>''k''</sub>) は一階の項である。

これらの変項の種について、[[全称記号]]や[[存在記号]]を使った論理式を構築可能である。

二階述語論理の「文（sentence）」は、いかなる種の[[自由変項]]も持たない論理式をいう。

上記のうちドメインの部分集合だけを変項として追加したものを「単項二階述語論理（monadic second-order logic）」と呼ぶ。上記の全種の変項を追加した二階述語論理を「完全二階述語論理（full second-order logic）」と呼んで、単項版と区別することがある。

一階述語論理と同様、二階述語論理でも非論理記号を含むことがある。ただし、論理式を構成する全ての項は一階の項（一階の変項で置換可能）か二階の項（適切な種の二階の変項で置換可能）でなければならない。

== 意味論 ==
二階述語論理の意味論は、個々の文の意味を確立するものである。一階述語論理では単一の標準の意味論しかなかったが、二階述語論理では2種類の意味論 '''standard semantics''' と '''Henkin semantics''' がある。どちらの意味論でも、一階述語論理の範囲内の意味論（一階の量化、論理和や論理積など）は一階述語論理と同じである。異なるのは、二階の変項への量化の解釈である。

standard semantics では、その種の集合や関数すべてに対しての量化と捉える。従って、一階の変項のドメインが明確化されれば、全ての量化の意味が固定される。これにより、二階述語論理の表現能力がもたらされる。

Henkin semantics では、二階の変項にはそれぞれの種ごとにドメインがあり、その種の集合や関数全体の真部分集合の場合がある。[[レオン・ヘンキン | ヘンキン]](1950) がこの意味論を定義し、一階述語論理で成り立つ[[ゲーデルの完全性定理]]と[[コンパクト性定理]]が、Henkin semantics と組み合わせた二階述語論理でも成り立つことを証明した。これは Henkin semantics が多種の一階述語論理とほぼ等価であるためである。Henkin semantics を伴った二階述語論理は、一階述語論理と同等の表現能力しかない。Henkin semantics は主に[[二階算術]]の研究で使われている。

== 推論体系 ==
論理の推論体系（あるいは演繹体系）とは、[[推論規則]]と論理公理の集合であり、論理式の並びが妥当な証明となっていることの根拠となる。二階述語論理には、いくつかの推論体系があるが、standard semantics に対して完全と言えるものは存在しない。どの体系も[[健全性|健全]]であり、証明に使える全ての文は適当な意味論において論理的に妥当である。

最も弱い推論体系は、一階述語論理の標準の推論体系（例えば[[自然演繹]]）に二階の項の置換規則を加えたものである<ref>そのような体系が Hinman (2005) で注釈なしで使われている。</ref>。この推論体系は[[二階算術]]の研究で主に使われている。

Shapiro (1991) と [[レオン・ヘンキン | ヘンキン]](1950) が検討した推論体系は、内包公理と選択公理を追加したものである。これら公理は二階述語論理の standard semantics に対して健全である。Henkin semantics の場合は、それら後置を満足するよう考慮した Henkin モデルであるときだけ健全と言える。<ref>Henkin (1950) でそれらモデルが研究されている。</ref>

== 二階論理とメタ論理学の成果 ==
[[ゲーデルの不完全性定理]]の系の1つとして、以下の3つの属性を同時に満足するような二階述語論理の推論体系は存在しないとされた<ref>その系の証明とは、健全で完全で実効的な standard semantics の推論体系があったとしたとき、[[ペアノの公理|ペアノ算術]]の[[帰納的可算集合|帰納的可算]]な完全な系が存在することになり、それはゲーデルの定理によって存在できないことが明らかとなっていることを示すものである。</ref>。

*（[[健全性]]）証明可能な二階述語論理の文は常に真である。すなわち standard semantics に従ったあらゆるドメインで真である。
*（[[完全性]]）standard semantics において常に妥当な二階述語論理の論理式は、全て証明可能である。
*（[[決定可能性|実効性]]）与えられた論理式の並びが妥当な証明かどうかを正しく決定できる証明検証アルゴリズムが存在する。

この系を言い換えると、二階述語論理は完全な[[証明理論]]に従わない、とも言える。この観点で、standard semantics を伴った二階述語論理は一階述語論理とは異なり、そのせいもあって論理学者は長年、二階述語論理に関わることを避けてきた。[[ウィラード・ヴァン・オーマン・クワイン]]は二階述語論理は「論理」ではないと考える理由としてこれを挙げている<ref>{{cite book | author = W.V. Quine | title = Philosophy of Logic | date = 1970年 | publisher = Prentice-Hall | pages = 90–91}}</ref>。

上述のように Henkin は Henkin semantics を使えば二階述語論理に一階述語論理の標準的な健全で完全で実効的な推論体系を適用できることを証明した。

== 歴史と論争 ==
述語論理を数学界に初めてもたらしたのは[[チャールズ・サンダース・パース]]であり、彼は現代とよく似た記法を用いていた（彼はまた ''Second-order logic'' という用語も生み出した）。パースの数年前に[[ゴットロープ・フレーゲ]]の研究成果が発表されていたが、これは[[バートランド・ラッセル]]と[[アルフレッド・ノース・ホワイトヘッド]]が広く紹介するまであまり知られていなかった。現代ではフレーゲの業績の方がよく知られている。フレーゲは量化の種によって異なる変項を使っていたが、彼には2種類の異なる論理を扱っているという認識はなかった。[[ラッセルのパラドックス]]によって、その体系に問題があることが明らかとなった。論理学者らは問題を解決すべく、フレーゲの論理に制限を加える各種方法を検討し、それが[[一階述語論理]]となった。一階述語論理では、集合や属性は量化できないことになった。このような論理の階層化がこのころ初めてなされるようになった。

一階述語論理を使うと、[[集合論]]を公理的体系として形式化できることがわかり（完全性の問題はあるが、ラッセルのパラドックスほど悪いことではない）、[[公理的集合論]]が生まれ、集合は[[数学]]の基盤となった。[[算術]]、[[メレオロジー]]、その他の様々な論理的理論が一階述語論理の範囲内で公理的に定式化でき、ゲーデルやスコーレムが一階述語論理に固執したこともあって、二階や高階の述語論理はほとんど省みられなかった。

この状況を決定付けたのは、[[ウィラード・ヴァン・オーマン・クワイン]]などの論理学者である。クワインは ''Fx'' のような述語言語文について、''x'' を変項またはオブジェクトの名前とみなし、それ故に量化可能とし、「全ての物について…が成り立つ」という意味だとしたが、''F'' は単なる不完全な文の「省略形」であるとし、オブジェクトの名前とは考えなかった（属性のような抽象的オブジェクトとも考えなかった）。例えばそれは「…は犬である」かもしれない。しかし、そのような概念に量化を考えても何の意味もない。このような立場は、フレーゲの概念と事物を区別する立場と同じである。従って、述語を変項として扱うことは、個体変項だけが占めていた位置を共有することを意味する。そのような考え方は Boolos によって拒絶されている。

近年、二階述語論理は一種の回復の途上にある。この傾向をもたらしたのは George Boolos による二階の量化の解釈であり、彼は一階の量化と同じドメインでの複数形の量化として二階の量化を解釈した。Boolos はさらに一階述語論理では記述できない文を例に挙げ、完全な二階述語論理の量化でのみそれらを表現可能であるとした。しかし、その一部は二階述語論理を持ち出すまでもなく、一階述語論理に若干の拡張を加えるだけで表現可能である。

== 計算複雑性理論への応用 ==
有限な構造についての二階述語論理の各種形式の表現能力は、[[計算複雑性理論]]と密接に関係している。[[記述計算量]]の研究では、[[複雑性クラス]]を説明するのにそれに属する言語を表現できる論理体系の能力で表す。そのため、二階述語論理を前提として次のような複雑性クラスを説明できる。
* '''[[NP]]''' は、存在量化二階述語論理で表現できる言語の集合である（Fagin の定理、1974年）。
* [[Co-NP|co-'''NP''']] は、全称量化二階述語論理で表現できる言語の集合である。
* [[PH (計算複雑性理論)|'''PH''']] は、二階述語論理で表現できる言語の集合である。
* '''[[PSPACE]]''' は、二階述語論理に[[推移閉包]]演算子を追加したもので表現できる言語の集合である。
* '''[[EXPTIME]]''' は、二階述語論理に最小不動点演算子を追加したもので表現できる言語の集合である。
クラス間の関係は論理の表現能力にも直接影響を及ぼす。例えば、'''PH'''='''PSPACE''' であることが明らかになれば、推移閉包演算子を追加しても二階述語論理の表現能力には何の違いもないことが明らかになるだろう。

== 脚注 ==
{{Reflist}}

== 参考文献 ==
* {{cite journal | author = Henkin, L. | url = http://links.jstor.org/sici?sici=0022-4812%28195006%2915%3A2%3C81%3ACITTOT%3E2.0.CO%3B2-I | title = Completeness in the theory of types | journal = Journal of Symbolic Logic | volume = 15 | date = 1950年 | pages = 81–91}}
* {{cite book | author = Hinman, P. | title = Fundamentals of Mathematical Logic | publisher = A K Peters | date = 2005 | id = ISBN 1-56881-262-0}}
* {{cite book | author = Shapiro, S. | title = Foundations without Foundationalism: A Case for Second-order Logic | publisher = Oxford University Press | date = 2000年 | id = ISBN 0-19-825029-0}}
* {{cite conference | author = Rossberg, M. | url = http://www.st-andrews.ac.uk/~mr30/papers/RossbergCompleteness.pdf | title = First-Order Logic, Second-Order Logic, and Completeness | book-title = First-order logic revisited | editor = V. Hendricks | display-editors=etal | publisher = Logos-Verlag | location = Berlin | year = 2004 | archiveurl = https://web.archive.org/web/20080407051012/http://www.st-andrews.ac.uk/~mr30/papers/RossbergCompleteness.pdf | archivedate = 2008-04-07 | url-status=dead}}
* {{cite journal | author = Vaananen, J. | url = http://www.math.ucla.edu/~asl/bsl/0704/0704-003.ps | title = Second-Order Logic and Foundations of Mathematics | journal = Bulletin of Symbolic Logic | volume = 7 | issue = 4 | date = 2001年 | pages = 504–520 | doi = 10.2307/2687796}}

{{Logic}}
{{Mathematical logic}}

{{DEFAULTSORT:にかいしゆつころんり}}
{{Normdaten}}
[[Category:述語論理]]
[[Category:数理論理学]]
[[Category:数学に関する記事]]
[[fr:Logique d'ordre supérieur#Logique du second ordre]]