等式論理

同義語：equational logic

概要

前提知識: 代数構造, 準同型, 同値関係, 構造的帰納法

群の公理 $(x\cdot y)\cdot z=x\cdot(y\cdot z)$、$e\cdot x=x$、$x^{-1}\cdot x=e$ や、環・束・Boole 代数の公理の多くは、変数をすべて全称的に読む等式の形をしている。等式だけを論理式とし、等式から等式を導く規則だけを使う論理を 等式論理（equational logic）という。推論規則は、等式を扱うときにふつう使う 5 つ、すなわち反射律・対称律・推移律、両辺に同じ演算を施すこと（置き換え）、変数に項を代入すること（代入）である。
等式論理の基本定理は Birkhoff の 完全性定理 である。等式の集合 $\Sigma$ を満たすすべての代数系で成り立つ等式は、$\Sigma$ から 5 つの規則で導出できる。Gödelの完全性定理の等式版にあたるが、証明ははるかに短く、項の集合を「導出できる等式」で割った代数系が求めるモデルになる。この記事では、等式論理の構文と意味を定義し、健全性と完全性定理を証明する。さらに、等式で定義される代数系のクラスが準同型像・部分代数・直積で閉じていることを示し、その逆が成り立つという Birkhoff の定理を述べ、導出の形を調べて等式の非帰結を示す例を扱う。

定義

項と等式

代数構造の記事の定義「同じ演算の型と準同型」のとおり、型 $F$ とは演算記号の集合で、各記号 $f$ に項数 $n_f\in\mathbb N$ が定まっているものである（$n_f=0$ の記号は定数記号）。型 $F$ の代数系 $A$ は、各 $f$ に写像 $f^A\colon A^{n_f}\to A$ を備えた空でない集合である。変数の可算無限集合 $X=\{x_0,x_1,\dots\}$ を固定する。

項と等式

型 $F$ の項とは、次の規則を有限回使って得られる記号列である。各変数は項である。$f\in F$ の項数が $n$ で $t_1,\dots,t_n$ が項なら、$f(t_1,\dots,t_n)$ は項である（$n=0$ なら $f$ 自身が項）。項の全体を $T(X)$ と書く。
項 $s,t$ の組を $s\approx t$ と書き、等式（identity）という。
代数系 $A$ と 割り当て $\alpha\colon X\to A$ について、項の値 $t^A[\alpha]\in A$ を $x^A[\alpha]:=\alpha(x)$、$f(t_1,\dots,t_n)^A[\alpha]:=f^A(t_1^A[\alpha],\dots,t_n^A[\alpha])$ で定める。
すべての割り当て $\alpha$ で $s^A[\alpha]=t^A[\alpha]$ となるとき、$A$ は等式 $s\approx t$ を 満たす といい、$A\models s\approx t$ と書く。等式の集合 $\Sigma$ のすべての元を満たすとき $A\models\Sigma$ と書き、$A$ を $\Sigma$ の モデル という。$\Sigma$ のすべてのモデルが $s\approx t$ を満たすとき、$\Sigma\models s\approx t$ と書く。

項の文法は Backus–Naur記法の記事の例「等式論理の項と論理式」の形で書ける。項は組み立て方がただ 1 通りに決まるので（論理式の記事の定理「一意読み取り」と同じ議論）、値は組み立てに沿った再帰で矛盾なく定まる。等号 $=$ と区別するために $\approx$ を使う。$s\approx t$ は、一階述語論理の文 $\forall x_1\cdots\forall x_k\,(s=t)$（$x_1,\dots,x_k$ は $s,t$ に現れる変数）と同じ意味をもつ。
代入とは写像 $\sigma\colon X\to T(X)$ のことで、項 $t$ の各変数 $x$ を $\sigma(x)$ に同時に置き換えた項を $t\sigma$ と書く。すなわち $x\sigma:=\sigma(x)$、$f(t_1,\dots,t_n)\sigma:=f(t_1\sigma,\dots,t_n\sigma)$ である。

導出

等式論理の導出

$\Sigma$ を等式の集合とする。等式の有限列 $s_1\approx t_1,\dots,s_k\approx t_k$ で、各 $s_i\approx t_i$ が次のどれかを満たすものを、$\Sigma$ からの導出という。

(E0) $\Sigma$ の元である。
(E1) 反射律：$t\approx t$ の形である。
(E2) 対称律：前にある $t\approx s$ から得られる $s\approx t$ である。
(E3) 推移律：前にある $s\approx u$ と $u\approx t$ から得られる $s\approx t$ である。
(E4) 置き換え：前にある $s'_1\approx t'_1,\dots,s'_n\approx t'_n$ と項数 $n$ の $f\in F$ から得られる $f(s'_1,\dots,s'_n)\approx f(t'_1,\dots,t'_n)$ である。
(E5) 代入：前にある $s\approx t$ と代入 $\sigma$ から得られる $s\sigma\approx t\sigma$ である。
最後が $s\approx t$ である導出があるとき、$\Sigma\vdash s\approx t$ と書く。

BS12 Definition 14.18（p. 94）は、(E4) の代わりに「項 $r$ の中の部分項 $s$ の 1 つの出現を $t$ に替える」形の規則を使う。その規則の結論 $r\approx r'$ は、$r$ の組み立てについての帰納法により、(E1) と (E4) を繰り返して導出できる。逆に (E4) の結論は、成分を 1 つずつ替える規則を $n$ 回使い (E3) でつなげば得られる。したがって、導出できる等式は同じである。

導出の例

2 項演算 $\cdot$ だけの型で、$\Sigma$ を結合律 $(x\cdot y)\cdot z\approx x\cdot(y\cdot z)$ と交換律 $x\cdot y\approx y\cdot x$ とする。次は $(x\cdot y)\cdot z\approx y\cdot(x\cdot z)$ の導出である。

$x\cdot y\approx y\cdot x$（(E0)、交換律）
$z\approx z$（(E1)）
$(x\cdot y)\cdot z\approx(y\cdot x)\cdot z$（1・2 に (E4)）
$(x\cdot y)\cdot z\approx x\cdot(y\cdot z)$（(E0)、結合律）
$(y\cdot x)\cdot z\approx y\cdot(x\cdot z)$（4 に $x\mapsto y$、$y\mapsto x$ の代入 (E5)）
$(x\cdot y)\cdot z\approx y\cdot(x\cdot z)$（3・5 に (E3)）
代入は変数を同時に置き換えるので、5 で $x$ と $y$ を入れ替えることができる。

健全性

代入補題

代数系 $A$、割り当て $\alpha\colon X\to A$、代入 $\sigma$ について、割り当て $\beta$ を $\beta(x):=\sigma(x)^A[\alpha]$ で定めると、すべての項 $t$ について $(t\sigma)^A[\alpha]=t^A[\beta]$ である。

$t$ の組み立てについての帰納法による。$t=x$ なら両辺とも $\sigma(x)^A[\alpha]$ である。$t=f(t_1,\dots,t_n)$ なら、値の定義と帰納法の仮定により $(t\sigma)^A[\alpha]=f^A\bigl((t_1\sigma)^A[\alpha],\dots\bigr)=f^A\bigl(t_1^A[\beta],\dots\bigr)=t^A[\beta]$ である。$\square$

健全性

$\Sigma\vdash s\approx t$ なら $\Sigma\models s\approx t$ である。

$A\models\Sigma$ とし、導出の各行 $s_i\approx t_i$ について $A\models s_i\approx t_i$ を $i$ についての帰納法で示す。(E0) は仮定、(E1) は明らかである。(E2)・(E3) は、各割り当てで値が等しいという関係が対称的・推移的であることによる。(E4) は、各割り当て $\alpha$ で $s'_j{}^A[\alpha]=t'_j{}^A[\alpha]$ なら $f^A$ を施した値も等しいことによる。(E5) は、どの $\alpha$ についても、lem-eq-substitution の $\beta$ をとれば $(s\sigma)^A[\alpha]=s^A[\beta]=t^A[\beta]=(t\sigma)^A[\alpha]$ となることによる。$\square$

Birkhoff の完全性定理

健全性の逆、すなわち「$\Sigma$ のすべてのモデルで成り立つ等式は導出できる」を示すには、$\Sigma$ のモデルで「$\Sigma$ から導出できる等式だけが成り立つ」ものを作ればよい。それが次の代数系である。

導出による商代数

$T(X)$ の上の関係 $\equiv$ を、$s\equiv t:\iff\Sigma\vdash s\approx t$ で定める。$[t]$ を $t$ の $\equiv$ による同値類とし、$F_\Sigma:=T(X)/{\equiv}$ に演算
$$ f^{F_\Sigma}([t_1],\dots,[t_n]):=[f(t_1,\dots,t_n)] $$
を入れる。

商代数は Σ のモデル

$\equiv$ は同値関係で、$F_\Sigma$ の演算は代表元のとり方によらずに定まる。
割り当て $\alpha\colon X\to F_\Sigma$ と代入 $\sigma$ が、項 $t$ に現れるすべての変数 $x$ について $\alpha(x)=[\sigma(x)]$ を満たすなら、$t^{F_\Sigma}[\alpha]=[t\sigma]$ である。
$F_\Sigma\models\Sigma$ である。

1：(E1)・(E2)・(E3) により $\equiv$ は反射的・対称的・推移的である。$s_j\equiv t_j$（$j=1,\dots,n$）なら、(E4) により $f(s_1,\dots,s_n)\equiv f(t_1,\dots,t_n)$ なので、演算の値は代表元によらない。
2：$t$ の組み立てについての帰納法による。$t=x$ なら $t^{F_\Sigma}[\alpha]=\alpha(x)=[\sigma(x)]=[x\sigma]$ である。$t=f(t_1,\dots,t_n)$ なら、帰納法の仮定と演算の定義により $t^{F_\Sigma}[\alpha]=f^{F_\Sigma}([t_1\sigma],\dots,[t_n\sigma])=[f(t_1\sigma,\dots,t_n\sigma)]=[t\sigma]$ である。
3：$p\approx q\in\Sigma$ と割り当て $\alpha\colon X\to F_\Sigma$ をとる。$p,q$ に現れる有限個の変数 $x$ についてそれぞれ $\alpha(x)$ の代表元 $\sigma(x)$ を 1 つ選び、ほかの変数では $\sigma(x):=x$ とする。2 により $p^{F_\Sigma}[\alpha]=[p\sigma]$、$q^{F_\Sigma}[\alpha]=[q\sigma]$ であり、(E0) と (E5) により $\Sigma\vdash p\sigma\approx q\sigma$ なので、両者は等しい。$\square$

Birkhoff の完全性定理

等式の集合 $\Sigma$ と等式 $s\approx t$ について
$$ \Sigma\models s\approx t\iff\Sigma\vdash s\approx t. $$

商代数で値を比べる

$\Sigma\models s\approx t$ とする。lem-eq-quotient の 3 により $F_\Sigma$ は $\Sigma$ のモデルなので、$F_\Sigma\models s\approx t$ である。割り当て $\alpha(x):=[x]$ と恒等代入 $\sigma(x):=x$ に lem-eq-quotient の 2 を使うと、$s^{F_\Sigma}[\alpha]=[s]$、$t^{F_\Sigma}[\alpha]=[t]$ である。よって $[s]=[t]$、すなわち $\Sigma\vdash s\approx t$ である。逆向きは thm-eq-soundness による。$\square$

この証明は BS12 Theorem 14.17・14.19（pp. 94–96）と同じ考え方だが、同書が完全不変な合同関係の言葉で述べているところを、導出できる等式の関係 $\equiv$ に直接まとめた。$F_\Sigma$ は、$\Sigma$ のモデル全体のクラスの $X$ 上の 自由代数 である。実際、$\Sigma$ のモデル $A$ と写像 $g\colon X\to A$ があれば、$[t]\mapsto t^A[g]$ は thm-eq-soundness により矛盾なく定まる準同型で、$[x]\mapsto g(x)$ を満たす。
選択公理は使っていない。3 で代表元を選ぶのは有限個の変数についてだけだからである。Gödelの完全性定理の証明では、無矛盾な文の集合を極大に広げる段階が要るが、等式論理では等式の否定や選言がないので、導出できる等式の全体をそのまま割ればモデルになる。

等式で定義されるクラス

型 $F$ の代数系のクラス $\mathcal K$ が 等式クラス であるとは、等式の集合 $\Sigma$ があって、$\mathcal K$ が $\Sigma$ のモデル全体 $\operatorname{Mod}(\Sigma)$ に一致することをいう。準同型像・部分代数・直積で閉じたクラスを 多様体（variety）という。ここで部分代数は、すべての演算で閉じた空でない部分集合に演算を制限したもの、直積は台集合の直積に成分ごとの演算を入れたものである。

等式クラスは多様体

等式の集合 $\Sigma$ について、$\operatorname{Mod}(\Sigma)$ は全射準同型の像・部分代数・直積で閉じている。

1 つの等式 $p\approx q$ が保たれることを示せばよい。全射準同型の像については、代数構造の記事の命題「準同型は項の計算と可換」の後半による。部分代数 $B\subset A$ については、$B$ の値への割り当て $\alpha$ で、$t^B[\alpha]=t^A[\alpha]$ が項の組み立てについての帰納法で分かるので、$A$ での等式が $B$ でも成り立つ。直積 $A=\prod_iA_i$ については、割り当て $\alpha$ の第 $i$ 成分を $\alpha_i$ とすると、同じ帰納法で $t^A[\alpha]$ の第 $i$ 成分は $t^{A_i}[\alpha_i]$ である。各成分で $p,q$ の値が等しいので、$p^A[\alpha]=q^A[\alpha]$ である。$\square$

逆に、全射準同型の像・部分代数・直積で閉じたクラス（多様体）はどれも等式クラスである（Birkhoff の HSP 定理、BS12 Theorem 11.9（p. 75）。この記事では証明しない）。この定理と thm-eq-hsp により、等式クラスであることは 3 つの構成で閉じていることと同値になる。

等式クラスとそうでないクラス

型 $\{\cdot,{}^{-1},e\}$（項数 $2,1,0$）で、結合律・$e\cdot x\approx x$・$x^{-1}\cdot x\approx e$ のモデルはちょうど群である。可換群・環（型 $\{+,\cdot,-,0,1\}$）・束・Boole代数も等式クラスである。
型 $\{+,\cdot,-,0,1\}$ で、体全体のクラスは等式クラスでない。$\mathbb Q\times\mathbb Q$ は直積だが $(1,0)\cdot(0,1)=(0,0)$ なので体でなく、thm-eq-hsp の直積についての主張に反するからである。同じ理由で整域全体も等式クラスでない。
「逆元がある」という条件を演算 ${}^{-1}$ なしで $\exists y\,(y\cdot x=e)$ と書くと等式でなくなり、型 $\{\cdot,e\}$ では群全体のクラスは部分代数で閉じない。群 $(\mathbb Z,+,0)$ の部分代数 $(\mathbb N,+,0)$ は群でない。

導出の形から分かること

完全性定理により、「$\Sigma\models s\approx t$ でない」ことを、モデルを作る代わりに導出の形を調べて示すこともできる。

釣り合った等式

各変数が $s$ と $t$ に同じ回数ずつ現れる等式 $s\approx t$ を 釣り合っている という。$\Sigma$ の元がすべて釣り合っているなら、$\Sigma\vdash s\approx t$ となる等式はすべて釣り合っている。とくに、変数 $x\ne y$ について $\Sigma\not\models x\approx y$ であり、$\Sigma$ は 2 元以上のモデルをもつ。

変数 $x$ の項 $t$ での出現回数を $\#_x(t)$ と書き、導出の長さについての帰納法で、各行が釣り合っていることを示す。(E0)・(E1)・(E2) は明らかで、(E3) は $\#_x(s)=\#_x(u)=\#_x(t)$ による。(E4) は $\#_x(f(s'_1,\dots,s'_n))=\sum_j\#_x(s'_j)$ による。(E5) は、代入した項で
$$ \#_x(s\sigma)=\sum_{y\in X}\#_y(s)\,\#_x(\sigma(y)) $$
（和は $s$ に現れる有限個の $y$ について）となり、$\#_y(s)=\#_y(t)$ がすべての $y$ で成り立つことによる。
$x\approx y$ は釣り合っていないので $\Sigma\not\vdash x\approx y$、thm-eq-completeness により $\Sigma\not\models x\approx y$ である。したがって、$x\approx y$ を満たさない $\Sigma$ のモデル、すなわち 2 つの異なる元をもつモデルがある。$\square$

たとえば結合律と交換律は釣り合っているので、それらから冪等律 $x\cdot x\approx x$ は導出できない（両辺で $x$ の回数が違う）。釣り合った等式の集合から導出できる等式が釣り合っていることは、BS12 p. 96 の例 (1) にも述べられている。

反例：規則を 1 つ外すと完全性が崩れる

thm-eq-completeness の $\Rightarrow$ は、5 つの規則のどれを除いても成り立たない。各行で、$\Sigma\models s\approx t$ だが、その規則を除いた導出では $s\approx t$ が得られない。$a,b,c$ は定数記号、$\cdot$ は 2 項演算、$e$ は定数記号とする。

外す規則	$\Sigma$ と $s\approx t$	成り立たなくなること
(E1) 反射律	$\Sigma=\emptyset$、$x\approx x$	$\Sigma\vdash x\approx x$
(E2) 対称律	$\Sigma=\{a\approx b\}$、$b\approx a$	$\Sigma\vdash b\approx a$
(E3) 推移律	$\Sigma=\{a\approx b,\ b\approx c\}$、$a\approx c$	$\Sigma\vdash a\approx c$
(E4) 置き換え	$\Sigma=\{x\cdot e\approx x\}$、$(x\cdot e)\cdot y\approx x\cdot y$	$\Sigma\vdash(x\cdot e)\cdot y\approx x\cdot y$
(E5) 代入	$\Sigma=\{x\cdot y\approx y\cdot x\}$、$z\cdot w\approx w\cdot z$	$\Sigma\vdash z\cdot w\approx w\cdot z$

反例の確かめ

どの行でも $\Sigma\models s\approx t$ は、各モデルで値を計算すれば分かる（2・3 行目は等号の対称性・推移性、4 行目は $x\cdot e$ と $x$ の値が等しいこと、5 行目は $x,y$ に $z,w$ の値を割り当てること）。導出できないことは、除いた規則以外の規則で保たれる性質を見つけて示す。

各行の不変量を開く

1 行目：(E1) がなければ、(E2)〜(E5) はどれも前の行を必要とし、$\Sigma$ が空なので最初の行が作れない。

2 行目：「$t$ は $s$ の葉のいくつかの $a$ を $b$ に替えたもの」という関係 $s\sqsupseteq t$ を考える。$a\sqsupseteq b$ であり、(E1)・(E3)・(E4)・(E5) はこの関係を保つ（代入では、変数の位置に同じ項が入るだけである）。$b\sqsupseteq a$ は成り立たないので、$b\approx a$ は導出できない。

3 行目：「$s,t$ は同じ形の木で、異なる葉の組はどれも $\{a,b\}$ か $\{b,c\}$ である」という関係を考える。$\Sigma$ の元はこれを満たし、(E1)・(E2)・(E4)・(E5) はこれを保つ。$a\approx c$ は満たさないので導出できない。

4 行目：項 $t$ の根の「$\cdot e$」を外せるだけ外した項を $R(t)$ とする（$R(u\cdot e):=R(u)$、それ以外は $R(t):=t$）。$R(p)=R(q)$ という関係を考えると、$\Sigma$ の元とその代入の例はこれを満たし、(E1)・(E2)・(E3) は明らかに保つ。(E5) も保つ。$R(p)=R(q)=r$ なら $p,q$ は $r$ の後ろに $\cdot e$ を何個か付けた形なので、代入しても両辺は $r\sigma$ の後ろに $\cdot e$ を付けた形で、$R$ の値は等しい。$R((x\cdot e)\cdot y)=(x\cdot e)\cdot y$ と $R(x\cdot y)=x\cdot y$ は異なるので、導出できない。

5 行目：項 $t$ の部分項 $u\cdot v$ のうち、$u,v$ が変数 $x,y$（どちらの順でも）であるものを記号 $\star$ にまとめて読む写像 $N$ を、$N(u\cdot v):=\star$（$\{N(u),N(v)\}=\{x,y\}$ のとき）、それ以外は $N(u)\cdot N(v)$、変数・定数ではそのもの、で定める。$N(x\cdot y)=N(y\cdot x)$ であり、(E1)〜(E4) は $N(p)=N(q)$ という関係を保つ（$N(f(\dots))$ は成分の $N$ の値だけで決まる）。$N(z\cdot w)=z\cdot w\ne w\cdot z=N(w\cdot z)$ なので、代入なしでは導出できない。