【一階述語論理1】論理式と構造

投稿者:

一階述語論理の記号

一階述語論理では以下の記号を使用する.

定義(言語)
1. 変数記号
アルファベットの小文字1文字およびアルファベットの小文字1文字に自然数添え字を付したものを変数記号という. また, 変数記号の集合を\({\rm VAR}\)と表す.

\({\rm VAR} := \{x, y, z, \cdots, x_0, x_1, x_2, \cdots\}.\)

2. 論理記号
論理記号の集合を\({\rm LG}\)で表し, 次で定める.

\({\rm LG} := \{\bot, \lnot, \land, \lor, \forall, \exists, = \}.\)

3. 定数記号
定数を表す記号の集合を\(\mathcal{C}\)と表す.

4. 関数記号
自然数\(n\)(\(n > 0\))に対し\(n\)-引数関数を表す記号の集合を\(\mathcal{F}_n\)とし, \(n\)をその関数記号のアリティという. また, 関数記号全体の集合を\(\mathcal{F}\)と表す.

\(\mathcal{F} := \bigcup \mathcal{F}_n .\)

5. 述語記号
自然数\(n\)(\(n > 0\))に対し\(n\)-引数関係を表す記号の集合を\(\mathcal{P}_n\)とし, \(n\)をその関係記号のアリティという.また, 関係記号全体の集合を\(\mathcal{P}\)と表す.

\(\mathcal{P} := \bigcup \mathcal{P}_n .\)

以上の記号すべての集合を言語といい, \(L\)と表す.

\(L := {\rm VAR} \cup {\rm LG} \cup \mathcal{C} \cup \mathcal{F} \cup \mathcal{P}.\)

\(L\)の記号から作られた記号の列を単に記号列といい, 2つの記号列\(\Phi, \Psi\)が記号の列として等しいとき\(\Phi \equiv \Psi\)と表す. これから定義する項や論理式についても特定の記号列でしかない. 項や論理式の内容が等しいことと記号列として等しいことは異なることに注意.

定義(項)
項を以下で定める.
1. 変数記号, つまり\({\rm VAR}\)の元は項である.
2. 定数記号, つまり\(\mathcal{C}\)の元は項である.
3. \(t_1, t_2, \cdots, t_n\)を項とし, \(f\)を\(n\)-変数関数(\(f \in \mathcal{F}_n\))とする. このとき, \(f(t_1, t_2, \cdots, t_n)\)も項である.
4. 以上で項であることがわかるものだけが項である.

論理式

定義(原子論理式)
\(t_1, t_2, \cdots, t_n\)を項とする. また,\(R\)を\(n\)-引数関係(\(R \in \mathcal{P}_n\))とする. このとき,

\(\bot\),
\((t_1 = t_2)\),
\(R(t_1, t_2, \cdots, t_n)\),

原子論理式という.

定義(論理式)
論理式を以下で定める.
1. 原子論理式は論理式である.
2. \(\varphi, \psi\)を論理式とする. このとき, \(\lnot \varphi, (\varphi \land \psi), (\varphi \lor \psi), (\varphi \rightarrow \psi),\)は論理式である.
3. \(\varphi\)を論理式とし, \(x\)を変数記号とする. このとき, \((\forall x \varphi), (\exists x \varphi)\).
4. 以上で論理式であることがわかるものだけが論理式である.

束縛出現・自由出現

定義(スコープ)
論理式が\((\forall x \varphi), (\exists x \varphi)\)のいずれかの形であるとき, 論理式\(\varphi\)に対応する部分を\(\forall x\)または\( \exists x\)のスコープという.

論理式\(\varphi\)に含まれる変数記号\(x\)の個数を\({\rm num}_{\varphi}(x)\)と表す.

定義(束縛出現・自由出現)
論理式\(\varphi\)に含まれる変数記号\(x\)のうち\(i\)番目(\(1 \le i \le{\rm num}_{\varphi}(x)\))のものを\(x^i\)と表すことにする. 変数記号\(x^i\)が \(\forall x\)または\( \exists x\)のスコープ内に含まれているとき変数記号\(x^i\)は束縛出現するという. \(x^i\)が束縛出現しないとき, 自由出現するという. また束縛出現する変数記号を束縛変数, 自由出現する変数記号を自由変数という.

束縛出現・自由出現は変数記号の1つ1つに定義された概念であることに注意. すなわち, 同じ\(a\)という変数記号でも\((a = a)\)のように2度現れていれば, 前者を\(a^1\)後者を\(a^2\)として区別する.

閉項・閉論理式

定義(閉項)
項\(t\)に変数記号が含まれないとき, \(t\)を閉項という.
定義(閉論理式)
論理式\(\varphi\)に現れるすべての変数記号が束縛出現しているとき, \(\varphi\)は閉論理式であるという.

全称閉包

定義(全称閉包)
論理式\(\varphi\)の自由出現する変数記号を\(x_1, \cdots, x_n\)とする. \(\varphi\)の全称閉包とは, \(\forall x_1 \cdots \forall x_n \varphi\)の形の閉論理式をさす.

\(L\)-構造

定義(\(L\)-構造)
\(L\)-構造とは, 空でない集合\(M\)と\(L\)上の写像\(F : L \to M \cup \bigcup_n P(M^n) \)の組\(\mathcal{M} = \langle M ; F\rangle\)のことである. ただし, \(F\)は次のような写像である.

1. \(c \in \mathcal{C}\)に対して\(c^{\mathcal{M}} := F(c)\)は\(M\)の元である.

\(c^{\mathcal{M}} \in M\).

2. \(f \in \mathcal{F}_n \quad (n > 0)\)に対して\(f^{\mathcal{M}} := F(f)\)は関数\(M^n \to M\)である.

\(f^{\mathcal{M}} : M^n \to M\).

3. \(R \in \mathcal{P}_n \quad (n > 0)\)に対して\(R^{\mathcal{M}} := F(R)\)は\(n\)-引数関係である.

\(R^{\mathcal{M}} \subset M^n \).

\(|\mathcal{M}| := M\)を\(\mathcal{M}\)の対象領域という.

名前による拡張\(L(\mathcal{M})\)

定義(名前・拡張言語\(L(\mathcal{M})\)):
\(L\)を言語とし\(\mathcal{M}\)を1つの\(L\)-構造とする. このとき, \(M\)の各元\(m \in M\)を表す定数記号\(C_m\)を各元の名前といい\(C_m^{\mathcal{M}} = m \)と定めることを意図した記号とする. \(L\)に\(\{C_m : m \in M\}\)を付け加えた言語を\(L\)の名前による拡張といい\(L(\mathcal{M})\)と表す.
定義(\(L\)-論理式, \(L(\mathcal{M})\)-論理式):
言語\(L\)だけを用いて作った論理式と\(L(\mathcal{M})\)を用いて作った論理式をそれぞれ\(L\)-論理式, \(L(\mathcal{M})\)-論理式と表して区別する.

参考文献

[1] 新井敏康,数学基礎論 増補版,東京大学出版会,2021.

[2] ケネス・キューネン, キューネン数学基礎論講義, 日本評論社,2016.

[3] 鹿島亮, 現代基礎数学15 数理論理学, 朝倉書店, 2009.

[4] Stephen Cole Kleene, Introduction To Meta-Mathematics, Ishi Press Internal, 1952.

[5] Joseph R. Shoenfield, Mathematical Logic, CRC Press, 1967.

[6] Richard E. Hodel, An Introduction to Mathematical Logic, Dover Publications Inc, 1995.

コメントを残す

メールアドレスが公開されることはありません。 が付いている欄は必須項目です