§E16.6一階構造と充足関係

最終更新

一階論理式の意味は、非論理記号を解釈する構造と、自由変数へ値を与える割当ての組に対して定まる。本稿では項の値と論理式の充足を構造再帰によって定義し、意味が自由変数の値だけに依存することを証明する。

1 構造と割当て

定義 1.1.Σ=((Fn)n<ω,(Rn)n<ω)\Sigma=((F_n)_{n<\omega},(R_n)_{n<\omega})を一階シグネチャとする。Σ\Sigma-構造 (Sigma-structure)M\mathcal Mは、次のデータからなる。

  1. 非空集合MM。集合MMをM\mathcal Mの 台集合 (domain) という。
  2. 各f∈Fnf\in F_nに対する関数fM:Mn→Mf^{\mathcal M}:M^n\to M。特にc∈F0c\in F_0は元cM∈Mc^{\mathcal M}\in Mとして解釈する。
  3. 各R∈RnR\in R_nに対する関係RM⊆MnR^{\mathcal M}\subseteq M^n。

論理記号==は常にMM上の同一性として解釈する。

定義 1.2.M\mathcal Mを台集合MMの構造とする。写像s:Var→Ms:\mathrm{Var}\to Mを変数割当て (variable assignment) という。x∈Varx\in\mathrm{Var}、a∈Ma\in Mに対して、更新 (assignment update)s[x↦a]s[x\mapsto a]を

s[x↦a](y)={ay=x,s(y)y≠xs[x\mapsto a](y)= \begin{cases} a&y=x,\\ s(y)&y\ne x \end{cases}

によって定める。

例 1.3 (整数加法群の構造). 群のシグネチャに対し、台集合をZ\mathbb Z、eM=0e^{\mathcal M}=0、iM(a)=−ai^{\mathcal M}(a)=-a、mM(a,b)=a+bm^{\mathcal M}(a,b)=a+bと置くと構造を得る。構文上の項m(x,i(y))m(x,i(y))の値は割当てssの下でs(x)−s(y)s(x)-s(y)である。

2 項の解釈

定義 2.1.Σ\Sigma-構造M\mathcal Mと割当てs:Var→Ms:\mathrm{Var}\to Mに対し、項ttの値 (interpretation of a term)⟦t⟧sM∈M\llbracket t\rrbracket_s^{\mathcal M}\in Mを

⟦x⟧sM=s(x),⟦c⟧sM=cM,⟦f(t1,…,tn)⟧sM=fM(⟦t1⟧sM,…,⟦tn⟧sM)\begin{aligned} \llbracket x\rrbracket_s^{\mathcal M}&=s(x),\\ \llbracket c\rrbracket_s^{\mathcal M}&=c^{\mathcal M},\\ \llbracket f(t_1,\ldots,t_n)\rrbracket_s^{\mathcal M} &=f^{\mathcal M}(\llbracket t_1\rrbracket_s^{\mathcal M},\ldots, \llbracket t_n\rrbracket_s^{\mathcal M}) \end{aligned}

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

命題 2.2.Σ\Sigma-構造M\mathcal Mと割当てs:Var→Ms:\mathrm{Var}\to Mを任意に取る。定義 2.1の再帰式を満たす写像

Term⁡Σ(Var)→M\operatorname{Term}_\Sigma(\mathrm{Var})\to M

が一意に存在する。

証明.§E16.5 定理 3.1の項に対する構造再帰において、変数xxへs(x)s(x)、定数ccへcMc^{\mathcal M}、関数記号f∈Fnf\in F_nへ演算fM:Mn→Mf^{\mathcal M}:M^n\to Mを割り当てる。定理の存在と一意性が求める主張を与える。▨

補題 2.3.M\mathcal MをΣ\Sigma-構造、ttをΣ\Sigma-項、s,r:Var→Ms,r:\mathrm{Var}\to Mを割当てとする。すべてのx∈Var⁡(t)x\in\operatorname{Var}(t)についてs(x)=r(x)s(x)=r(x)なら

⟦t⟧sM=⟦t⟧rM\llbracket t\rrbracket_s^{\mathcal M}=\llbracket t\rrbracket_r^{\mathcal M}

である。

証明.ttに関する構造帰納法を用いる。t=xt=xの場合は仮定から従う。定数の場合は両辺がcMc^{\mathcal M}である。t=f(t1,…,tn)t=f(t_1,\ldots,t_n)の場合、Var⁡(ti)⊆Var⁡(t)\operatorname{Var}(t_i)\subseteq\operatorname{Var}(t)であるから、帰納法の仮定により各引数の値が一致する。同じ関数fMf^{\mathcal M}を適用すれば項全体の値も一致する。▨

3 Tarski の充足関係

定義 3.1.Σ\Sigma-構造M\mathcal M、割当てs:Var→Ms:\mathrm{Var}\to M、論理式φ\varphiに対する関係M,s⊨φ\mathcal M,s\models\varphi (Tarski satisfaction relation) を次の再帰で定める。

M,s⊨t=u  ⟺  ⟦t⟧sM=⟦u⟧sM,M,s⊨R(t1,…,tn)  ⟺  (⟦t1⟧sM,…,⟦tn⟧sM)∈RM,M,s⊨¬φ  ⟺  M,s⊭φ,M,s⊨φ→ψ  ⟺  M,s⊭φ または M,s⊨ψ,M,s⊨∀x φ  ⟺  すべての a∈M について M,s[x↦a]⊨φ.\begin{aligned} \mathcal M,s\models t=u &\iff \llbracket t\rrbracket_s^{\mathcal M}=\llbracket u\rrbracket_s^{\mathcal M},\\ \mathcal M,s\models R(t_1,\ldots,t_n) &\iff (\llbracket t_1\rrbracket_s^{\mathcal M},\ldots, \llbracket t_n\rrbracket_s^{\mathcal M})\in R^{\mathcal M},\\ \mathcal M,s\models\neg\varphi &\iff \mathcal M,s\not\models\varphi,\\ \mathcal M,s\models\varphi\to\psi &\iff \mathcal M,s\not\models\varphi\text{ または }\mathcal M,s\models\psi,\\ \mathcal M,s\models\forall x\,\varphi &\iff \text{すべての }a\in M\text{ について } \mathcal M,s[x\mapsto a]\models\varphi. \end{aligned}

命題 3.2.Σ\Sigma-構造M\mathcal Mを任意に取る。定義 3.1の各節を満たす関係は、すべての割当てとすべてのΣ\Sigma-論理式について一意に定まる。

証明. 割当て全体の集合をS=MVarS=M^{\mathrm{Var}}とし、再帰の値域を関数集合Y=2SY=\mathbf2^Sとする。各原子論理式θ\thetaには、s∈Ss\in Sをその原子の真理値へ写す関数を割り当てる。A,B∈YA,B\in Yとx∈Varx\in\mathrm{Var}に対して

N(A)(s)=1−A(s),I(A,B)(s)={0A(s)=1 かつ B(s)=0,1それ以外,Qx(A)(s)=1  ⟺  すべての a∈M について A(s[x↦a])=1\begin{aligned} N(A)(s)&=1-A(s),\\ I(A,B)(s)&= \begin{cases}0&A(s)=1\text{ かつ }B(s)=0,\\1&\text{それ以外},\end{cases}\\ Q_x(A)(s)&=1\iff\text{すべての }a\in M\text{ について }A(s[x\mapsto a])=1 \end{aligned}

と定める。論理式上の構造再帰定理をこれらの演算へ適用すると、各論理式φ\varphiに関数Aφ∈YA_\varphi\in Yが一意に対応する。M,s⊨φ\mathcal M,s\models\varphiをAφ(s)=1A_\varphi(s)=1と定めれば、表示された充足節をすべて満たす。

同じ節を満たす二つの関係が一致することは、論理式の構造帰納法により、原子、否定、含意、全称量化の順に従う。量化の場合には、すべての更新s[x↦a]s[x\mapsto a]に直下の論理式に対する帰納法の仮定を適用する。▨

命題 3.3.Σ\Sigma-構造M\mathcal M、割当てss、論理式φ,ψ\varphi,\psi、変数xxについて次が成り立つ。

M,s⊨φ∧ψ  ⟺  M,s⊨φ かつ M,s⊨ψ,M,s⊨φ∨ψ  ⟺  M,s⊨φ または M,s⊨ψ,M,s⊨∃x φ  ⟺  M,s[x↦a]⊨φ を満たす a∈M が存在する.\begin{aligned} \mathcal M,s\models\varphi\land\psi &\iff \mathcal M,s\models\varphi\text{ かつ }\mathcal M,s\models\psi,\\ \mathcal M,s\models\varphi\lor\psi &\iff \mathcal M,s\models\varphi\text{ または }\mathcal M,s\models\psi,\\ \mathcal M,s\models\exists x\,\varphi &\iff \mathcal M,s[x\mapsto a]\models\varphi \text{ を満たす }a\in M\text{ が存在する}. \end{aligned}

証明.∧\landと∨\lorの定義を¬,→\neg,\toまで展開し、充足関係の否定と含意の節を適用すれば最初の二式を得る。存在量化について、

M,s⊨¬∀x ¬φ\mathcal M,s\models\neg\forall x\,\neg\varphi

であることは、すべてのa∈Ma\in MについてM,s[x↦a]⊭φ\mathcal M,s[x\mapsto a]\not\models\varphiである、という主張の否定と同値である。古典的な量化の否定により、M,s[x↦a]⊨φ\mathcal M,s[x\mapsto a]\models\varphiを満たすa∈Ma\in Mが存在することと同値になる。▨

注意 3.4 (等号の解釈). 等号を任意の二項関係としてではなく同一性として解釈したため、反射律と関数・関係に関する代入可能性は各構造で自動的に成り立つ。

例 3.5 (量化式の評価). 整数加法群の構造M\mathcal Mでは

M,s⊨∀x m(x,e)=x\mathcal M,s\models\forall x\,m(x,e)=x

がすべての割当てssについて成り立つ。実際、任意のa∈Za\in\mathbb Zについてa+0=aa+0=aである。一方、M,s⊨∃x m(x,x)=e\mathcal M,s\models\exists x\,m(x,x)=eも成り立つが、証人は00に限られる。

4 充足の局所性

定理 4.1.M\mathcal MをΣ\Sigma-構造、φ\varphiをΣ\Sigma-論理式、s,r:Var→Ms,r:\mathrm{Var}\to Mを割当てとする。すべてのx∈FV⁡(φ)x\in\operatorname{FV}(\varphi)についてs(x)=r(x)s(x)=r(x)なら

M,s⊨φ⟺M,r⊨φ\mathcal M,s\models\varphi \quad\Longleftrightarrow\quad \mathcal M,r\models\varphi

である。

証明.φ\varphiに関する構造帰納法を用いる。等号原子と関係原子の場合、各項に現れる変数はFV⁡(φ)\operatorname{FV}(\varphi)に含まれる。補題 2.3により各項の値が一致するので、原子の真偽も一致する。

否定の場合は直下の論理式に対する帰納法の仮定から従う。含意の場合は二つの直下の論理式に対する帰納法の仮定と含意の充足節から従う。

φ=∀x ψ\varphi=\forall x\,\psiとする。ssとrrはFV⁡(ψ)∖{x}\operatorname{FV}(\psi)\setminus\{x\}上で一致する。任意のa∈Ma\in Mについて、s[x↦a]s[x\mapsto a]とr[x↦a]r[x\mapsto a]はFV⁡(ψ)\operatorname{FV}(\psi)上で一致する。帰納法の仮定により

M,s[x↦a]⊨ψ  ⟺  M,r[x↦a]⊨ψ\mathcal M,s[x\mapsto a]\models\psi \iff \mathcal M,r[x\mapsto a]\models\psi

である。すべてのa∈Ma\in Mを量化し、全称量化の充足節を適用すれば主張を得る。▨

系 4.2.σ∈Sent⁡(Σ)\sigma\in\operatorname{Sent}(\Sigma)、M\mathcal MをΣ\Sigma-構造とする。任意の二つの割当てs,rs,rについて

M,s⊨σ  ⟺  M,r⊨σ\mathcal M,s\models\sigma\iff\mathcal M,r\models\sigma

である。

証明.FV⁡(σ)=∅\operatorname{FV}(\sigma)=\varnothingであるから、定理 4.1の割当て一致条件は空虚に成り立つ。▨

5 α\alpha同値と充足

補題 5.1.∀x φ\forall x\,\varphiから捕獲回避的に∀z ren⁡x↦z(φ)\forall z\,\operatorname{ren}_{x\mapsto z}(\varphi)を得たとする。任意のΣ\Sigma-構造M\mathcal Mと割当てssについて

M,s⊨∀x φ  ⟺  M,s⊨∀z ren⁡x↦z(φ)\mathcal M,s\models\forall x\,\varphi \iff \mathcal M,s\models\forall z\,\operatorname{ren}_{x\mapsto z}(\varphi)

である。

証明. 改名の対象である外側の束縛を有効とする印を一つ置く。構文木を下るとき、内側の∀x\forall xに入った箇所では外側の印を無効にし、それ以外では印を保つ。ren⁡x↦z\operatorname{ren}_{x\mapsto z}は、印が有効な位置にあるxxだけをzzへ変える操作である。捕獲回避条件は、印が有効なxxの出現が内側の∀z\forall zの作用域に無いことと、z∉FV⁡(φ)z\notin\operatorname{FV}(\varphi)を含む。

印付きの項と論理式について、任意の割当てrrと任意のa∈Ma\in Mに対して

M,r[x↦a]⊨φ  ⟺  M,r[z↦a]⊨ren⁡x↦z(φ)(*)\mathcal M,r[x\mapsto a]\models\varphi \iff \mathcal M,r[z\mapsto a]\models\operatorname{ren}_{x\mapsto z}(\varphi) \tag{*}

を、項と論理式について同時に構造帰納的に示す。項が変数の場合、印が有効なxxは左でaa、改名後のzzは右でaaを与える。ほかの変数は両割当てで同じ値をもつ。特にzzの改名対象外の出現は、捕獲回避条件により有効な領域には存在しない。定数と関数適用では項評価の再帰式と各引数への帰納法の仮定を用いる。原子論理式では各項の値の一致を用い、否定と含意では充足節と直下の論理式への帰納法の仮定を用いる。

内側の量化式∀y η\forall y\,\etaでは、次の三場合を別々に扱う。

  1. y=xy=xの場合、内側の束縛が外側のxxを遮蔽するため、その本体では印を無効にし、改名を停止する。任意のb∈Mb\in Mについて (r[x↦a])[x↦b]=r[x↦b](r[x\mapsto a])[x\mapsto b]=r[x\mapsto b] である。右側でも量化評価はxxをbbへ上書きする。両割当てに残り得る差はzzの値だけであるが、z∉FV⁡(φ)z\notin\operatorname{FV}(\varphi)なので定理 4.1によりη\etaの真偽を変えない。従ってこの量化式の両評価は一致する。この場合が∀x∀x R(x)\forall x\forall x\,R(x)の内側で改名を停止する shadowing を処理する。
  2. y=zy=zの場合、捕獲回避条件により、この∀z\forall zの作用域には印が有効なxxの出現がない。従って当該部分式は改名されない。量化評価でzzをbbへ上書きした後に残る両割当ての差はxxだけであり、印が有効な自由なxxは本体に無い。再び局所性により真偽が一致する。もし作用域に改名対象のxxがあれば、xxをzzへ変えた出現がこの量化子に捕獲されるため、そもそも生成的改名の仮定を満たさない。
  3. y≠x,zy\ne x,zの場合、割当て更新は (r[x↦a])[y↦b]=(r[y↦b])[x↦a],(r[z↦a])[y↦b]=(r[y↦b])[z↦a](r[x\mapsto a])[y\mapsto b]=(r[y\mapsto b])[x\mapsto a], \qquad (r[z\mapsto a])[y\mapsto b]=(r[y\mapsto b])[z\mapsto a] と交換する。任意のb∈Mb\in Mについて、基礎割当てをr[y↦b]r[y\mapsto b]として本体η\etaへの帰納法の仮定を適用する。すべてのbbを量化すれば、全称量化の充足節から両評価の同値を得る。

以上で項、原子、否定、含意、および三つの量化子の場合を尽くしたため(∗)(*)が成り立つ。

最後にr=sr=sとする。全称量化の充足節により、補題の左辺はすべてのa∈Ma\in Mについて(∗)(*)の左辺が成り立つこと、右辺はすべてのa∈Ma\in Mについて(∗)(*)の右辺が成り立つことと同値である。ゆえに両辺は同値である。▨

定理 5.2.φ≡αψ\varphi\equiv_\alpha\psiとする。任意のΣ\Sigma-構造M\mathcal Mと割当てssについて

M,s⊨φ⟺M,s⊨ψ\mathcal M,s\models\varphi \quad\Longleftrightarrow\quad \mathcal M,s\models\psi

である。

証明.α\alpha同値は捕獲回避的な一回の束縛変数改名を含む最小の合同同値関係である。一回の生成的改名では補題 5.1が主張を与える。反射律、対称律、推移律は充足の同値関係を保存する。否定、含意、全称量化の各合同規則も、それぞれの充足節により同値を保存する。したがってα\alpha同値の生成に関する帰納法により主張が従う。▨

6 真・充足可能・妥当・帰結

定義 6.1.M\mathcal MをΣ\Sigma-構造、φ\varphiを論理式、σ\sigmaを文、Γ\Gammaを論理式の集合とする。

  1. M⊨φ\mathcal M\models\varphi (satisfaction in a structure) とは、すべての割当てssについてM,s⊨φ\mathcal M,s\models\varphiであることをいう。文σ\sigmaでは割当てに依存しないため、M,s⊨σ\mathcal M,s\models\sigmaと同値である。
  2. φ\varphiが充足可能 (satisfiable) であるとは、M,s⊨φ\mathcal M,s\models\varphiを満たすΣ\Sigma-構造M\mathcal MとMM上の割当てssが存在することをいう。
  3. φ\varphiが妥当 (valid) であるとは、すべてのΣ\Sigma-構造M\mathcal Mとすべての割当てssについてM,s⊨φ\mathcal M,s\models\varphiであることをいい、⊨φ\models\varphiと書く。
  4. Γ⊨φ\Gamma\models\varphi (semantic consequence) とは、すべてのΣ\Sigma-構造M\mathcal Mと割当てssについて、M,s⊨γ\mathcal M,s\models\gammaがすべてのγ∈Γ\gamma\in\Gammaについて成り立つならM,s⊨φ\mathcal M,s\models\varphiが成り立つことをいう。

例 6.2 (真と妥当の相違). 群のシグネチャにおける文∀x m(x,e)=x\forall x\,m(x,e)=xは、整数加法群では真である。しかし、eeとmmを任意に解釈したすべての構造で真とは限らないので、群公理を前提にしない一階論理の妥当式ではない。妥当性は特定の構造ではなく、同じシグネチャのすべての構造を量化する。

7 演習

問題 7.1.

  1. 台集合を非空とする条件が、∀x φ\forall x\,\varphiと∃x φ\exists x\,\varphiの意味にどのように影響するか述べよ。
  2. M,s⊨∀x R(x,y)\mathcal M,s\models\forall x\,R(x,y)の真偽がs(y)s(y)に依存してもs(x)s(x)に依存しない理由を証明せよ。
  3. ∀x R(x,z)\forall x\,R(x,z)のxxをzzに改名する操作が許されない理由を意味論から説明せよ。
解答 (確認問題の解答).
  1. 非空性により全称量化が空虚に真、存在量化が常に偽となる空領域固有の挙動を除外する。
  2. 自由変数集合は{y}\{y\}である。充足の局所性によりyy上で一致する割当ては同じ真偽を与える。量化の評価ではs[x↦a]s[x\mapsto a]がすべてのaaを調べるため、もとのs(x)s(x)は用いない。
  3. 改名後の∀z R(z,z)\forall z\,R(z,z)では、もとの自由なzzまで量化される。したがって割当てs(z)s(z)への依存が失われ、一般には真偽が変わる。

▨

一階意味論は、構造、割当て、有限構文木上の再帰という三つのデータを分離する。次稿では項を変数へ同時代入する操作を定め、代入後の構文評価と割当て更新が一致することを証明する。

参考文献

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

前提記事