2変数論理

決定可能性

充足可能性や有限充足可能性など、2変数論理に関する重要な問題のいくつかは決定可能である。^{[ 2 ]}この結果は、特定の記述論理など、2変数論理の断片の決定可能性に関する結果を一般化するものである。ただし、2変数論理の断片の中には、充足可能性問題に関して計算複雑性がはるかに低いものもある。

対照的に、関数記号のない一階述語論理の3変数断片では、充足可能性は決定不能である。^{[ 3 ]}

関数記号のない一階述語論理の2変数断片は、^計数量化子[ ⁴^]、したがって一意性量化子を追加しても決定可能であることが知られています。これは、大きな数値に対する計数量化子がその論理では表現できないため、より強力な結果です。

計数量化子は、有限変数論理の表現力を実際に向上させます。なぜなら、次のようなノードが存在すると言えるからです。 $n$ 隣人、すなわち $\Phi =\exists x\exists ^{\geq n}yE(x,y)$ 数量詞を数えずに $n+1$ 同じ数式には変数が必要です。

2変数論理とワイスファイラー・レマン（または色洗練）アルゴリズムの間には強い関連性がある。2つのグラフが与えられたとき、任意の2つのノードが同じ安定色を持つのは、それらが同じ $C^{2}$ つまり、それらは計数を伴う2変数論理において同じ式を満たす。^{[ 5 ]}

↑ L. ヘンキン。「有限個の記号のみを含む論理システム」、報告書、モントリオール大学数学科、1967年
↑ E. Grädel、PG Kolaitis、M. Vardi、「 2変数一階述語論理の決定問題について」、The Bulletin of Symbolic Logic、第3巻、第1号（1997年3月）、53-69ページ。
↑ AS Kahr、Edward F. Moore、Hao Wang。Entscheidungsproblem Reduced to the ∀ ∃ ∀ Case、1962年。彼らの ∀ ∃ ∀ 式は 3 つの変数しか使用しないことを指摘している。
↑ E. Grädel、M. Otto、E. Rosen。「計数を用いた2変数論理は決定可能である」、第12回IEEEコンピュータサイエンスにおける論理に関するシンポジウム議事録、1997年。
↑グローエ、マーティン。「記述的複雑性理論における有限変数論理」。記号論理学紀要 4.4 (1998): 345-398。