一階述語論理

同義語:一階論理first-order predicate logicfirst-order logic

概要

一階述語論理(first-order predicate logic)とは、対象の間の演算や関係を記号で表し、台集合の元について量化する形式論理である。定数・関数・関係記号から項と論理式を作り、構造がそれらの記号を解釈すると文の真偽が定まる。自由変数を持つ式は、構造と変数への値の割り当てのもとで充足を判定する。完全性定理やコンパクト性定理は一階論理の基本定理である。

$$\newcommand{C}[0]{\mathbb{C}} \newcommand{div}[0]{\mathbin{÷}} \newcommand{N}[0]{\mathbb{N}} \newcommand{Q}[0]{\mathbb{Q}} \newcommand{R}[0]{\mathbb{R}} \newcommand{Z}[0]{\mathbb{Z}} $$

前提知識: 論理式, 命題論理, 集合論

一階述語論理とは

一階述語論理(first-order predicate logic、一階論理ともいう)は、数学的対象の間の関係を述べるための形式論理である。変数が表す対象について「すべて」や「ある」を意味する量化記号 $\forall,\exists$ を使える。命題論理が命題全体を一つの記号として扱うのに対し、一階論理は命題の内部にある対象・演算・関係を記述する(End01 Chapter 2)。

言語と論理式

一階言語 $L$ は、定数記号、引数の個数を指定した関数記号、引数の個数を指定した関係記号からなる。たとえば群を記述するときは、単位元の定数記号 $e$、二項演算記号 $\cdot$、一項演算記号 $\operatorname{inv}$ を使える。記号そのものは、まだ特定の集合上の演算を意味しない。

変数と定数記号から関数記号を用いて項を作り、項の等式や項に関係記号を適用したものを原子論理式とする。そこから否定・連言・含意などの結合子と量化記号を有限回用いて論理式を作る。自由変数が残らない論理式を文という。

群の公理を表す文

二項演算記号 $\cdot$、定数記号 $e$、一項演算記号 $\operatorname{inv}$ を持つ言語では、次の文が結合律を表す。
$$ \forall x\,\forall y\,\forall z\, ((x\cdot y)\cdot z=x\cdot(y\cdot z)). $$
同じ言語で単位元と逆元についての文も書ける。これらを同時に満たす構造が群になる。

構造と真偽

$L$ の構造 $M$ では、空でない集合 $|M|$ を台集合とし、各定数記号にその元、各関数記号に対応する演算、各関係記号に対応する関係を割り当てる。文の真偽は、この割り当てと量化記号の意味によって決まる。

たとえば $<$ を二項関係記号とする言語で
$$ \forall x\,\exists y\,(x< y) $$
は「すべての元の上に、さらに大きな元がある」という文である。通常の順序を入れた自然数全体では真だが、空でない有限全順序集合では偽である。同じ記号列でも、どの構造で解釈するかによって真偽が変わる。

自由変数を持つ式 $\varphi(x_1,\ldots,x_n)$ の場合は、構造 $M$ と元 $a_1,\ldots,a_n\in |M|$ を与えてはじめて充足するかを問う。$M$ でこの式を満たす組の集合
$$ \{(a_1,\ldots,a_n)\in |M|^n:M\models\varphi(a_1,\ldots,a_n)\} $$
は、その構造の中で定義可能な関係の例である。

一階という範囲

一階論理の $\forall x,\exists x$ が走るのは台集合 $|M|$ の元である。台集合の任意の部分集合や任意の関数を変数として量化することは、通常の一階言語の範囲には入らない。この制限の下でも、集合論や代数学の多くの公理を記述できる。

Gödelの完全性定理は、一階の文がすべての構造で成り立つことと形式的に証明できることを結び付ける。コンパクト性定理(一階論理)は、文の集合のどの有限部分もモデルを持てば全体にもモデルがあると述べる。どちらも、ここで定めた「文」と「構造」の関係に関する定理である。

関連項目

参考文献

[1]
Herbert B. Enderton, A Mathematical Introduction to Logic, Academic Press, 2001, Chapter 2 First-Order Logic(印刷 pp. 67–108):言語・項・論理式・自由変数・構造・充足関係。

Mathpediaは寄付と、参考文献の書籍リンク(Amazonアソシエイト)の紹介料で運営されています。 支援について / 寄付する