§E19.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\Rに定数記号crc_rを対応させても、F0={cr:r∈R}F_0=\{c_r:r\in\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 集合性・一意可読性・帰納法・再帰

集合を作る規則そのものは前提§E1.13 集合の存在原理で証明された形で用い、本記事では 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.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. 項ttの高さht⁡(t)\operatorname{ht}(t)を、t∈Tmt\in T_mを満たす最小のmmと定める。n≥1n\geq1、f∈Fnf\in F_n、t1,…,tn∈Term⁡Σ(Var)t_1,\ldots,t_n\in\operatorname{Term}_\Sigma(\mathrm{Var})について ht⁡(f(t1,…,tn))=1+max⁡1≤i≤nht⁡(ti)\operatorname{ht}(f(t_1,\ldots,t_n))=1+\max_{1\leq i\leq n}\operatorname{ht}(t_i) が成り立つことを証明せよ。また、群のシグネチャにおける項(x⋅x−1)⋅e(x\cdot x^{-1})\cdot eの高さを求めよ。
  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. 定義 2.1によりTm⊆Tm+1T_m\subseteq T_{m+1}であるから、m≤m′m\leq m'ならばTm⊆Tm′T_m\subseteq T_{m'}である。t=f(t1,…,tn)t=f(t_1,\ldots,t_n)、h=max⁡iht⁡(ti)h=\max_i\operatorname{ht}(t_i)とおく。各tit_iはTht⁡(ti)⊆ThT_{\operatorname{ht}(t_i)}\subseteq T_hに属するので、Th+1T_{h+1}の定義によりt∈Th+1t\in T_{h+1}であり、ht⁡(t)≤h+1\operatorname{ht}(t)\leq h+1である。

    逆向きの不等式のため、すべてのmmについて「f(t1,…,tn)∈Tmf(t_1,\ldots,t_n)\in T_mならばm≥1m\geq1かつすべてのiiについてti∈Tm−1t_i\in T_{m-1}」が成り立つことをmmについての帰納法で示す。T0T_0の元は変数と定数のタグ付き組であり、定理 3.1 (2)により関数適用のタグ付き組とは異なるので、f(t1,…,tn)∉T0f(t_1,\ldots,t_n)\notin T_0である。f(t1,…,tn)∈Tm+1f(t_1,\ldots,t_n)\in T_{m+1}とする。TmT_mに属するならば、帰納法の仮定によりti∈Tm−1⊆Tmt_i\in T_{m-1}\subseteq T_mである。TmT_mに属さないならば、あるn′≥1n'\geq1、f′∈Fn′f'\in F_{n'}、(t1′,…,tn′′)∈Tmn′(t'_1,\ldots,t'_{n'})\in T_m^{n'}についてf(t1,…,tn)=f′(t1′,…,tn′′)f(t_1,\ldots,t_n)=f'(t'_1,\ldots,t'_{n'})であり、定理 3.1 (2)によりn=n′n=n'、f=f′f=f'、ti=ti′t_i=t'_iであるからti∈Tmt_i\in T_mである。いずれの場合も主張が成り立つ。

    m=ht⁡(t)m=\operatorname{ht}(t)に前段を適用すると、すべてのiiについてti∈Tm−1t_i\in T_{m-1}、すなわちht⁡(ti)≤m−1\operatorname{ht}(t_i)\leq m-1であるから、h≤ht⁡(t)−1h\leq\operatorname{ht}(t)-1である。前々段とあわせてht⁡(t)=h+1\operatorname{ht}(t)=h+1を得る。

    群のシグネチャでは、変数xxと定数eeはT0T_0に属するので高さは00である。公式によりht⁡(x−1)=1\operatorname{ht}(x^{-1})=1、ht⁡(x⋅x−1)=1+max⁡{0,1}=2\operatorname{ht}(x\cdot x^{-1})=1+\max\{0,1\}=2、ht⁡((x⋅x−1)⋅e)=1+max⁡{2,0}=3\operatorname{ht}((x\cdot x^{-1})\cdot e)=1+\max\{2,0\}=3である。

  2. 外側のxxと内側のyyは束縛されるので、自由変数集合は{y,z}\{y,z\}である。

  3. x=yx=yならば、二つは同じ論理式∀x∀x R(x,x)\forall x\forall x\,R(x,x)であり、α\alpha同値である。以下x≠yx\neq yとする。字面の上では改名で外側の量化記号の変数名を変えることもできる。たとえばz∉{x,y}z\notin\{x,y\}を経由して∀x∀y R(x,y)≡α∀z∀y R(z,y)≡α∀z∀x R(z,x)≡α∀y∀x R(y,x)\forall x\forall y\,R(x,y)\equiv_\alpha\forall z\forall y\,R(z,y)\equiv_\alpha\forall z\forall x\,R(z,x)\equiv_\alpha\forall y\forall x\,R(y,x)である。そこで、変数名によらず、どの出現をどの量化記号が束縛するかを不変量として取り出す。

    論理式φ\varphiの構文木から、量化記号の変数名と束縛された出現の変数名を消し、束縛された各出現にそれを束縛する量化記号の木の中の位置を付け、自由な出現には変数名を残したものをB(φ)B(\varphi)とする。生成関係の両辺∀x φ\forall x\,\varphiと∀z ren⁡x↦z(φ)\forall z\,\operatorname{ren}_{x\mapsto z}(\varphi)を比べる。改名は木の形と量化記号の位置を変えない。外側の∀x\forall xが束縛する出現はzzに変わり、改名対象の出現はφ\varphi内の∀z\forall zの作用域に入らないので、改名後も根の∀z\forall zに束縛される。内側の量化記号が束縛する出現は、名前も内側の量化記号の変数名も変わらないので、同じ量化記号に束縛される。∀x φ\forall x\,\varphiで自由な出現の変数vvはv≠xv\neq xであり、z∉FV⁡(φ)z\notin\operatorname{FV}(\varphi)からv≠zv\neq zであるので、改名後も自由なまま同じ名前をもつ。よってBBは生成関係の両辺で等しい。またB(¬φ)B(\neg\varphi)とB(φ→ψ)B(\varphi\to\psi)はB(φ)B(\varphi)とB(ψ)B(\psi)を新しい根の下に置いて得られ、B(∀x φ)B(\forall x\,\varphi)は、B(φ)B(\varphi)を新しい根の下に置き、B(φ)B(\varphi)で自由な出現のうち名前がxxのものから名前を消して根の位置を付けて得られるので、それぞれB(φ)B(\varphi)、B(ψ)B(\psi)、xxから定まる。したがってB(φ)=B(ψ)B(\varphi)=B(\psi)で定まる関係は、生成関係を含み¬,→,∀\neg,\to,\forallと両立する同値関係であり、定義 5.2の最小性により、φ≡αψ\varphi\equiv_\alpha\psiならばB(φ)=B(ψ)B(\varphi)=B(\psi)である。

    ∀x∀y R(x,y)\forall x\forall y\,R(x,y)ではRRの第一引数を根の量化記号が、第二引数をその子の量化記号が束縛する。∀y∀x R(x,y)\forall y\forall x\,R(x,y)では第一引数を子の量化記号が、第二引数を根の量化記号が束縛する。よってBBが異なり、x≠yx\neq yのとき二つはα\alpha同値でない。二つの文は論理的には同値であるので、充足のような意味論の不変量ではこの二つを区別することができない。

▨

参考文献

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

前提記事