一階構造と Tarski の充足関係 | 数理論理

1 構造と割当て

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

非空集合 $M$ 。集合 $M$ を $\mathcal M$ の台集合 (domain) という。
各 $f\in F_n$ に対する関数 $f^{\mathcal M}:M^n\to M$ 。特に $c\in F_0$ は元 $c^{\mathcal M}\in M$ として解釈する。
各 $R\in R_n$ に対する関係 $R^{\mathcal M}\subseteq M^n$ 。

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

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

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

によって定める。

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

2 項の解釈

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

\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$ -構造 $\mathcal M$ と割当て $s:\mathrm{Var}\to M$ を任意に取る。定義 2.1の再帰式を満たす写像

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

が一意に存在する。

証明.§E19.5 定理 3.1の項に対する構造再帰において、変数 $x$ へ $s(x)$ 、定数 $c$ へ $c^{\mathcal M}$ 、関数記号 $f\in F_n$ へ演算 $f^{\mathcal M}:M^n\to M$ を割り当てる。定理の存在と一意性により求める主張が得られる。▨

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

\llbracket t\rrbracket_s^{\mathcal M}=\llbracket t\rrbracket_r^{\mathcal M}

である。

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

3 Tarski の充足関係

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

\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$ -構造 $\mathcal M$ を任意に取る。定義 3.1の各節を満たす関係は、すべての割当てとすべての $\Sigma$ -論理式について一意に定まる。

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

\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_\varphi\in Y$ が一意に対応する。 $\mathcal M,s\models\varphi$ を $A_\varphi(s)=1$ と定めれば、表示された充足節をすべて満たす。

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

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

\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$ まで展開し、充足関係の否定と含意の節を適用すれば最初の二式を得る。存在量化について、

\mathcal M,s\models\neg\forall x\,\neg\varphi

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

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

例 3.5. 整数加法群の構造 $\mathcal M$ では

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

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

4 充足の局所性

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

\mathcal M,s\models\varphi \quad\Longleftrightarrow\quad \mathcal M,r\models\varphi

である。

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

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

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

\mathcal M,s[x\mapsto a]\models\psi \iff \mathcal M,r[x\mapsto a]\models\psi

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

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

\mathcal M,s\models\sigma\iff\mathcal M,r\models\sigma

である。

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

5 $\alpha$ 同値と充足

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

\mathcal M,s\models\forall x\,\varphi \iff \mathcal M,s\models\forall z\,\operatorname{ren}_{x\mapsto z}(\varphi)

である。

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

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

\mathcal M,r[x\mapsto a]\models\varphi \iff \mathcal M,r[z\mapsto a]\models\operatorname{ren}_{x\mapsto z}(\varphi)

\text{(5.1.1)}

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

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

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

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

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

定理 5.2. $\varphi\equiv_\alpha\psi$ とする。任意の $\Sigma$ -構造 $\mathcal M$ と割当て $s$ について

\mathcal M,s\models\varphi \quad\Longleftrightarrow\quad \mathcal M,s\models\psi

である。

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

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

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

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

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

7 演習

問題 7.1.

任意の論理式 $\varphi$ と変数 $x$ について $\models\forall x\,\varphi\to\exists x\,\varphi$ であることを証明せよ。また、 $P$ を一項関係記号とし、 $x\neq y$ とするとき、 $\models\exists x\,(P(x)\to\forall y\,P(y))$ であることを証明せよ。
$\mathcal M,s\models\forall x\,R(x,y)$ の真偽が $s(y)$ に依存しても $s(x)$ に依存しない理由を証明せよ。
$R$ を二項関係記号とし、 $x\neq z$ とする。構造 $\mathcal M$ と割当て $s$ で、 $\mathcal M,s\models\forall z\,R(z,z)$ かつ $\mathcal M,s\not\models\forall x\,R(x,z)$ を満たすものを構成せよ。

解答 (確認問題の解答).

構造 $\mathcal M$ と割当て $s$ を任意に取り、 $\mathcal M,s\models\forall x\,\varphi$ とする。定義 1.1 (1)により台集合 $M$ は空でないので、 $a\in M$ を一つ取ることができる。全称量化の節により $\mathcal M,s[x\mapsto a]\models\varphi$ であり、命題 3.3により $\mathcal M,s\models\exists x\,\varphi$ である。含意の節により $\mathcal M,s\models\forall x\,\varphi\to\exists x\,\varphi$ であり、 $\mathcal M$ と $s$ は任意であるから妥当である。

次に $\psi=P(x)\to\forall y\,P(y)$ とおき、構造 $\mathcal M$ と割当て $s$ を任意に取る。 $P^{\mathcal M}=M$ の場合、 $M$ が空でないので $a\in M$ を取る。全称量化の節により、任意の $b\in M$ について $(s[x\mapsto a])[y\mapsto b](y)=b\in P^{\mathcal M}$ であるから $\mathcal M,s[x\mapsto a]\models\forall y\,P(y)$ であり、含意の節により $\mathcal M,s[x\mapsto a]\models\psi$ である。 $P^{\mathcal M}\neq M$ の場合、 $a\in M\setminus P^{\mathcal M}$ を取ると、 $s[x\mapsto a](x)=a\notin P^{\mathcal M}$ であるから $\mathcal M,s[x\mapsto a]\not\models P(x)$ であり、含意の節により $\mathcal M,s[x\mapsto a]\models\psi$ である。いずれの場合も $\mathcal M,s[x\mapsto a]\models\psi$ を満たす $a$ が存在するので、命題 3.3により $\mathcal M,s\models\exists x\,\psi$ である。
自由変数集合は $\{y\}$ である。充足の局所性により $y$ 上で一致する割当ては同じ真偽を与える。量化の評価では $s[x\mapsto a]$ がすべての $a$ を調べるため、もとの $s(x)$ は用いない。
台集合を $M=\{0,1\}$ 、 $R^{\mathcal M}=\{(0,0),(1,1)\}$ とし、 $s(z)=0$ を満たす割当て $s$ を取る。任意の $a\in M$ について $s[z\mapsto a](z)=a$ であり $(a,a)\in R^{\mathcal M}$ であるから、全称量化の節により $\mathcal M,s\models\forall z\,R(z,z)$ である。一方、 $x\neq z$ であるから $s[x\mapsto1](z)=s(z)=0$ であり、 $(1,0)\notin R^{\mathcal M}$ であるから $\mathcal M,s[x\mapsto1]\not\models R(x,z)$ である。よって $\mathcal M,s\not\models\forall x\,R(x,z)$ である。この例は、 $\forall x\,R(x,z)$ の $x$ を $z$ に改名して得る $\forall z\,R(z,z)$ が、もとの論理式と同じ構造と割当てのもとで異なる真偽をとることを示す。

▨

§E19.6一階構造と Tarski の充足関係

1 構造と割当て

2 項の解釈

3 Tarski の充足関係

4 充足の局所性

5 $\alpha$ 同値と充足

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

7 演習

参考文献

前提記事

§E19.6一階構造と Tarski の充足関係

1 構造と割当て

2 項の解釈

3 Tarski の充足関係

4 充足の局所性

5 α\alphaα同値と充足

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

7 演習

参考文献

前提記事

5 $\alpha$ 同値と充足