§E16.5一階論理の構文

最終更新

一階論理では、関数記号と関係記号の個数を有限に制限する必要はない。一方、各記号のアリティと各構文木は有限でなければならない。本稿では、集合サイズの記号族から項と論理式を有限段階で構成し、後続の解釈、充足、置換が用いる構造帰納法と構造再帰を確立する。

1 一階シグネチャ

定義 1.1. 一階シグネチャ (first-order signature) を

Σ=((Fn)n<ω,(Rn)n<ω)\Sigma=((F_n)_{n<\omega},(R_n)_{n<\omega})

とする。各FnF_nはnn項関数記号の集合、各RnR_nはnn項関係記号の集合である。すべてのFn,RnF_n,R_nは集合であり、タグを付けて互いに素であるとする。F0F_0の元を定数記号と呼ぶ。等号==はR2R_2の元ではなく、すべてのシグネチャに共通する論理記号とする。

変数集合Var={x0,x1,…}\mathrm{Var}=\{x_0,x_1,\ldots\}は可算無限であり、すべての非論理記号と互いに素であるとする。原始論理記号は¬,→,∀\neg,\to,\forallと括弧である。

例 1.2 (群のシグネチャ). 群のシグネチャは、F0={e}F_0=\{e\}、F1={i}F_1=\{i\}、F2={m}F_2=\{m\}とし、それ以外のFnF_nおよびすべてのRnR_nを空集合とすることで得られる。通常はi(x)i(x)をx−1x^{-1}、m(x,y)m(x,y)をx⋅yx\cdot yと書く。この中置記法は構文の略記である。

例 1.3 (集合サイズで無限なシグネチャ). 各実数r∈Rr\in\mathbb Rに定数記号crc_rを対応させても、F0={cr:r∈R}F_0=\{c_r:r\in\mathbb R\}は集合であるから許される。一方、すべての集合を添字とする記号族は集合をなさないため、本稿のシグネチャにはならない。

2 項と論理式の有限段階構成

集合としての構成を明確にするため、すべての構成子にタグを付ける。以下の通常記法はタグ付き組の略記である。

定義 2.1. 高さが高々mmのΣ\Sigma-項の集合TmT_mを

T0={⟨var,x⟩:x∈Var}∪{⟨const,c⟩:c∈F0},T_0=\{\langle\mathrm{var},x\rangle:x\in\mathrm{Var}\} \cup\{\langle\mathrm{const},c\rangle:c\in F_0\},Tm+1=Tm∪⋃1≤n<ω{⟨fun,n,f,t1,…,tn⟩:f∈Fn, (t1,…,tn)∈Tmn}T_{m+1}=T_m\cup \bigcup_{1\le n<\omega}\{\langle\mathrm{fun},n,f,t_1,\ldots,t_n\rangle: f\in F_n,\ (t_1,\ldots,t_n)\in T_m^n\}

によって定める。項 (term) 全体を

Term⁡Σ(Var)=⋃m<ωTm\operatorname{Term}_\Sigma(\mathrm{Var})=\bigcup_{m<\omega}T_m

とする。変数と定数のタグ付き組はx,cx,cと書き、正アリティのタグ付き組はf(t1,…,tn)f(t_1,\ldots,t_n)と書く。

定義 2.2. 原子論理式 (atomic formula) の集合を

Atom⁡Σ={⟨eq,t,u⟩:t,u∈Term⁡Σ(Var)}∪⋃n<ω{⟨rel,n,R,t1,…,tn⟩:R∈Rn, (t1,…,tn)∈Term⁡Σ(Var)n}\begin{aligned} \operatorname{Atom}_\Sigma={}& \{\langle\mathrm{eq},t,u\rangle:t,u\in\operatorname{Term}_\Sigma(\mathrm{Var})\}\\ &\cup\bigcup_{n<\omega} \{\langle\mathrm{rel},n,R,t_1,\ldots,t_n\rangle: R\in R_n,\ (t_1,\ldots,t_n)\in\operatorname{Term}_\Sigma(\mathrm{Var})^n\} \end{aligned}

とする。通常記法ではt=ut=u、R(t1,…,tn)R(t_1,\ldots,t_n)と書く。

高さが高々mmの論理式の集合AmA_mを

A0=Atom⁡Σ,A_0=\operatorname{Atom}_\Sigma,Am+1=Am∪{⟨¬,φ⟩:φ∈Am}∪{⟨→,φ,ψ⟩:φ,ψ∈Am}∪{⟨∀,x,φ⟩:x∈Var, φ∈Am}\begin{aligned} A_{m+1}=A_m &\cup\{\langle\neg,\varphi\rangle:\varphi\in A_m\}\\ &\cup\{\langle\to,\varphi,\psi\rangle:\varphi,\psi\in A_m\}\\ &\cup\{\langle\forall,x,\varphi\rangle:x\in\mathrm{Var},\ \varphi\in A_m\} \end{aligned}

によって定める。論理式 (first-order formula) 全体を

Form⁡Σ(Var)=⋃m<ωAm\operatorname{Form}_\Sigma(\mathrm{Var})=\bigcup_{m<\omega}A_m

とする。タグ付き組は¬φ\neg\varphi、(φ→ψ)(\varphi\to\psi)、∀x φ\forall x\,\varphiと書く。

定義 2.3. 派生結合子 (derived connective)∧,∨,↔\land,\lor,\leftrightarrowは命題論理と同じく¬,→\neg,\toから定める。存在量化 (existential quantification) は

∃x φ:=¬∀x ¬φ\exists x\,\varphi:=\neg\forall x\,\neg\varphi

と定める。

3 集合性・一意可読性・帰納法・再帰

次の定理は、後続の記事が再帰的な解釈や置換を定義するときの集合論的根拠である。集合を作る規則そのものは前提記事「集合の存在原理」が証明した形で用い、本記事は ZF・ZFC の公理を体系的には展開しない。

定理 3.1.Σ=((Fn)n<ω,(Rn)n<ω)\Sigma=((F_n)_{n<\omega},(R_n)_{n<\omega})の各記号族が集合であり、各記号のアリティが有限であるとする。このとき次が成り立つ。

  1. Term⁡Σ(Var)\operatorname{Term}_\Sigma(\mathrm{Var})、Atom⁡Σ\operatorname{Atom}_\Sigma、Form⁡Σ(Var)\operatorname{Form}_\Sigma(\mathrm{Var})は集合である。
  2. 各項と各論理式の外側構成子および直下の構成要素は一意であり、異なる構成子の像は互いに素である。
  3. 項全体は変数と定数を含み関数記号の適用で閉じた最小の集合である。論理式全体は原子論理式を含み、¬,→,∀\neg,\to,\forallの適用で閉じた最小の集合である。
  4. 項または論理式について、各構成子を保存する性質は構造帰納法によってすべての対象で成り立つ。
  5. 集合XX、変数と定数への初期値、および各n≥1n\ge1とf∈Fnf\in F_nに対する演算Xn→XX^n\to Xを与えると、それらと可換する写像Term⁡Σ(Var)→X\operatorname{Term}_\Sigma(\mathrm{Var})\to Xが一意に存在する。
  6. 集合YY、各原子論理式への初期値、演算N:Y→YN:Y\to Y、I:Y2→YI:Y^2\to Y、および各x∈Varx\in\mathrm{Var}に対する演算Qx:Y→YQ_x:Y\to Yを与えると、それらと可換する写像Form⁡Σ(Var)→Y\operatorname{Form}_\Sigma(\mathrm{Var})\to Yが一意に存在する。

証明.(1)を示す。前提記事の対・和・冪の原理§E1.13 定義 3.1と分出公理スキーマ§E1.13 定義 2.1により、有限個の集合の直積と有限和は集合である。また、置換公理スキーマ§E1.13 定義 5.1により、集合を定義域とする一意な対応の像は集合である。以下では、この二つの結果を各タグ付き像と可算族に適用する。

Var\mathrm{Var}とF0F_0は集合である。x↦⟨var,x⟩x\mapsto\langle\mathrm{var},x\rangleとc↦⟨const,c⟩c\mapsto\langle\mathrm{const},c\rangleはいずれも一意な対応なので、§E1.13 定義 5.1により二つのタグ付き像は集合である。§E1.13 定義 3.1の対と和を用いて二つの像を合わせるとT0T_0は集合になる。

TmT_mが集合であるとする。各有限n≥1n\ge1について、有限直積TmnT_m^nとFn×TmnF_n\times T_m^nは集合である。後者の各元を⟨fun,n,f,t1,…,tn⟩\langle\mathrm{fun},n,f,t_1,\ldots,t_n\rangleへ送る対応は一意なので、そのタグ付き像Cm,nC_{m,n}は§E1.13 定義 5.1により集合である。n↦Cm,nn\mapsto C_{m,n}もω∖{0}\omega\setminus\{0\}上の一意な対応であるから、同じ置換公理スキーマにより{Cm,n:1≤n<ω}\{C_{m,n}:1\le n<\omega\}は集合である。§E1.13 定義 3.1の和の原理をこの集合族へ適用し、さらにTmT_mと合わせるとTm+1T_{m+1}は集合になる。自然数に関する帰納法により各TmT_mは集合である。再帰によって各mmにTmT_mが一意に対応するため、§E1.13 定義 5.1により{Tm:m<ω}\{T_m:m<\omega\}は集合であり、和の原理によりTerm⁡Σ(Var)=⋃m<ωTm\operatorname{Term}_\Sigma(\mathrm{Var})=\bigcup_{m<\omega}T_mは集合である。

項全体が集合であるため、その有限直積と各RnR_nの直積は集合である。各n<ωn<\omegaについて、等号原子と関係原子を作るタグ付き対応の像は§E1.13 定義 5.1により集合である。さらにnnによって添字付けられた像の族も置換公理スキーマにより集合であるから、和の原理を適用するとAtom⁡Σ\operatorname{Atom}_\Sigmaは集合になる。A0=Atom⁡ΣA_0=\operatorname{Atom}_\Sigmaから、否定、含意、全称量化の有限個のタグ付き像を同じ二つの原理で合わせると、AmA_mが集合ならAm+1A_{m+1}も集合になる。最後に、m↦Amm\mapsto A_mへ置換公理スキーマを適用して{Am:m<ω}\{A_m:m<\omega\}を作り、和の原理を適用するとForm⁡Σ(Var)=⋃m<ωAm\operatorname{Form}_\Sigma(\mathrm{Var})=\bigcup_{m<\omega}A_mは集合になる。

(2)を示す。変数、定数、関数適用、等号原子、関係原子、否定、含意、全称量化には互いに異なるタグを用いた。したがって異なる構成子の像は互いに素である。同じタグの構成子では、順序組の等号から記号、アリティ、引数がすべて一致する。よって外側構成子と直下の構成要素は一意である。

(3)を項について示す。CCが変数と定数を含み、すべての有限アリティの関数適用で閉じているとする。T0⊆CT_0\subseteq Cである。Tm⊆CT_m\subseteq Cなら、TmT_mの元へ関数記号を適用して得る全項もCCに入るのでTm+1⊆CT_{m+1}\subseteq Cである。したがって項全体はCCに含まれる。論理式についても、A0=Atom⁡ΣA_0=\operatorname{Atom}_\Sigmaから始め、否定、含意、全称量化への閉性を用いる同じ帰納法で最小性を得る。

(4)を示す。項の性質P\mathcal Pがすべての変数と定数で成り立ち、t1,…,tnt_1,\ldots,t_nで成り立つならf(t1,…,tn)f(t_1,\ldots,t_n)でも成り立つとする。P\mathcal Pを満たす項の集合は(3)の閉性を満たすため、項全体に等しい。論理式の性質についても、すべての原子で成り立ち、¬,→,∀\neg,\to,\forallの各構成で保存されるなら、(3)によりすべての論理式で成り立つ。

(5)を示す。TmT_m上の写像hmh_mを帰納的に定める。T0T_0では指定された変数と定数の値を用いる。hmh_mが定まったとき、Tm+1∖TmT_{m+1}\setminus T_mの元は(2)により一意にf(t1,…,tn)f(t_1,\ldots,t_n)と表示され、各tit_iはTmT_mに属する。指定されたnn項演算を(hm(t1),…,hm(tn))(h_m(t_1),\ldots,h_m(t_n))に適用して値を定める。TmT_m上ではhm+1=hmh_{m+1}=h_mとする。一意可読性により定義は競合しない。したがってh=⋃m<ωhmh=\bigcup_{m<\omega}h_mは求める写像である。別の写像h′h'が同じ再帰式を満たすなら、TmT_m上でh=h′h=h'であることをmmに関して帰納的に示すことができるのでh=h′h=h'である。

(6)ではAmA_m上の写像kmk_mを同様に構成する。A0A_0では指定された原子論理式の値を用いる。新しい否定、含意、全称量化にはそれぞれN,I,QxN,I,Q_xを適用する。(2)の一意可読性により存在する写像k=⋃m<ωkmk=\bigcup_{m<\omega}k_mは矛盾なく定まり、AmA_mに関する帰納法により一意である。以上により、すべての項目が示された。▨

注意 3.2 (有限性を使う箇所). 記号の種類は集合サイズで無限でもよい。各構成子が有限個の直下要素をもつことと、各項・論理式について、その項・論理式を含む有限段階が存在することが構造帰納法を支える。無限個の直下要素をもつ構文木を許す無限論理では、別の高さ構成と帰納原理が必要である。

4 自由変数・束縛変数・文

定義 4.1. 項ttに 現れる変数 (variable occurring in a term) の有限集合Var⁡(t)\operatorname{Var}(t)を

Var⁡(x)={x},Var⁡(c)=∅,\operatorname{Var}(x)=\{x\},\qquad \operatorname{Var}(c)=\varnothing,Var⁡(f(t1,…,tn))=⋃i=1nVar⁡(ti)\operatorname{Var}(f(t_1,\ldots,t_n)) =\bigcup_{i=1}^n\operatorname{Var}(t_i)

によって構造再帰的に定める。

定義 4.2. 論理式φ\varphiの 自由変数集合 (set of free variables)FV⁡(φ)\operatorname{FV}(\varphi)を

FV⁡(t=u)=Var⁡(t)∪Var⁡(u),FV⁡(R(t1,…,tn))=⋃i=1nVar⁡(ti),FV⁡(¬φ)=FV⁡(φ),FV⁡(φ→ψ)=FV⁡(φ)∪FV⁡(ψ),FV⁡(∀x φ)=FV⁡(φ)∖{x}\begin{aligned} \operatorname{FV}(t=u)&=\operatorname{Var}(t)\cup\operatorname{Var}(u),\\ \operatorname{FV}(R(t_1,\ldots,t_n))&=\bigcup_{i=1}^n\operatorname{Var}(t_i),\\ \operatorname{FV}(\neg\varphi)&=\operatorname{FV}(\varphi),\\ \operatorname{FV}(\varphi\to\psi)&=\operatorname{FV}(\varphi)\cup\operatorname{FV}(\psi),\\ \operatorname{FV}(\forall x\,\varphi)&=\operatorname{FV}(\varphi)\setminus\{x\} \end{aligned}

によって構造再帰的に定める。自由でない変数出現は、それを支配する量化記号によって束縛されている (bound variable occurrence) という。FV⁡(φ)=∅\operatorname{FV}(\varphi)=\varnothingを満たす論理式を文 (sentence) といい、文全体をSent⁡(Σ)\operatorname{Sent}(\Sigma)と書く。

命題 4.3. 任意の項ttと論理式φ\varphiについて、Var⁡(t)\operatorname{Var}(t)とFV⁡(φ)\operatorname{FV}(\varphi)は有限集合である。

証明. 項について構造帰納法を用いる。変数と定数の場合は明らかであり、関数適用の場合は有限個の有限集合の和である。論理式についても構造帰納法を用いる。原子の場合は有限個の項の変数集合の和である。否定、含意、全称量化の場合は、有限和または一点の除去が有限性を保存する。▨

例 4.4 (自由出現と束縛出現). 論理式

R(x,y)→∀x R(x,z)R(x,y)\to\forall x\,R(x,z)

では、左側のxxとyy、右側のzzが自由に現れ、右側のxxは全称量化によって束縛される。したがって自由変数集合は{x,y,z}\{x,y,z\}である。

5 α\alpha同値

束縛変数の名前は意味を変えない。ただし、自由変数を捕獲する改名は許されない。

定義 5.1.∀x φ\forall x\,\varphiの直下で、外側の∀x\forall xが束縛するxxの出現だけをzzに変える操作をren⁡x↦z(φ)\operatorname{ren}_{x\mapsto z}(\varphi)と書く。内側に現れる別の∀x\forall xの内部では改名を停止する。z∉FV⁡(φ)z\notin\operatorname{FV}(\varphi)であり、改名対象の出現がφ\varphi内の∀z\forall zの作用域に入らないとき、この改名を捕獲回避的 (capture-avoiding) という。

定義 5.2. α\alpha同値 (alpha-equivalence)≡α\equiv_\alphaを、次の捕獲回避的な束縛変数の改名

∀x φ≡α∀z ren⁡x↦z(φ)\forall x\,\varphi \equiv_\alpha \forall z\,\operatorname{ren}_{x\mapsto z}(\varphi)

をすべて含み、¬,→,∀\neg,\to,\forallの各構成子と両立する最小の同値関係として定める。すなわち、≡α\equiv_\alphaは捕獲回避的な一貫した束縛変数改名が生成する最小の合同関係である。

例 5.3 (α\alpha同値と捕獲).zzがφ\varphiに自由に現れないなら

∀x R(x,y)≡α∀z R(z,y)\forall x\,R(x,y)\equiv_\alpha\forall z\,R(z,y)

である。一方、∀x R(x,z)\forall x\,R(x,z)のxxをzzに改名して∀z R(z,z)\forall z\,R(z,z)とすると、もとの自由なzzが束縛される。したがって両者はα\alpha同値ではない。

命題 5.4.φ≡αψ\varphi\equiv_\alpha\psiならFV⁡(φ)=FV⁡(ψ)\operatorname{FV}(\varphi)=\operatorname{FV}(\psi)である。

証明. 生成関係となる一回の捕獲回避的改名では、束縛されている変数名だけが変わり、自由変数の出現は変わらない。したがって自由変数集合は等しい。等号、対称律、推移律による閉包と、否定、含意、全称量化の各合同規則も自由変数集合の等しさを保存する。生成列の長さに関する帰納法により主張が従う。▨

6 演習

問題 6.1.

  1. FnF_nが各nnについて集合であるだけでなく、n<ωn<\omegaにわたる族として与えられる必要がある理由を述べよ。
  2. ∀x(R(x,y)→∃y S(x,y,z))\forall x(R(x,y)\to\exists y\,S(x,y,z))の自由変数集合を求めよ。
  3. ∀x∀y R(x,y)\forall x\forall y\,R(x,y)と∀y∀x R(x,y)\forall y\forall x\,R(x,y)が一般にはα\alpha同値でない理由を述べよ。
解答 (確認問題の解答).
  1. 項の一段階の構成でn<ωn<\omegaにわたる記号適用の和集合を取るため、その全体が集合として与えられていなければならない。
  2. 外側のxxと内側のyyは束縛されるので、自由変数集合は{y,z}\{y,z\}である。
  3. α\alpha同値が変更するのは束縛変数の名前であり、量化記号の順序ではないからである。

▨

本稿は有限構文木の生成原理を確立した。次稿では非空の台集合をもつ構造と変数割当てを定め、項の解釈と Tarski の充足関係をこの構造再帰に沿って定義する。

参考文献

  1. Wilfrid Hodges, A Shorter Model Theory, Cambridge University Press, 1997.
  2. David Marker, Model Theory: An Introduction, Graduate Texts in Mathematics, Springer, 2002.

前提記事