数理論理学の基礎：等式論理

\( \newcommand{\Pow}[1]{\mathcal{P}(#1)} \newcommand{\nat}{\mathbb{N}} \) \(\newcommand{\name}[1]{\underline{#1}}\) \( \newcommand{\blank}{ {-} } \)

2. 等式論理

等式論理 (equational logic) は先程までの命題論理とは異なり命題同士の関係ではなく命題の中身、特に $s=t$ という形をした等式による命題に注目する論理である。。 等式論理に対しても命題論理と同様に統語論、意味論を考える。命題論理と同様に形式的証明と、命題論理での真理値に対応するモデル (model) というのを紹介する。

形式的証明は等式の以下に上げる基本的な性質による書き換え操作によって得られる。

1. 反射律 (reflexivity) $s=s$ である。
2. 対称律 (symmetricity) $s=t$ ならば $t=s$ である。
3. 推移律 (transitivity) $s=t$ かつ $t=r$ ならば $s=r$ である。
4. 代入 (substitution) $s(u)=t(u)$ ならば $s(r)=t(r)$ である。
5. 関数との両立 (compatibility with functions) 任意の $i<n+1$ に対して $s_i=t_i$ ならば $f(s_0,\ldots,s_n)=f(t_0,\ldots,t_n)$ である。

一方、モデルによる意味論はある種の数学的な代数構造 (algebraic structure) を用いて定義される。具体的には構造が与えられたとき、その構造で満たされることを真と見做す。ここで構造というのは台集合 (underlying set) とその上の関数からなる組のことである。

2.1 等式論理の統語論

定義 1 (等式論理の記号)

等式論理の論理記号 (logical symbol) は以下からなる。

• 変数記号 (variable symbol) $u,v,w,\ldots$ 。
• 等号記号 (equality symbol) $=$ 。
• 括弧 (brackets) $(,).$ 及びカンマ (comma) $,$ 。

変数記号の集合を \(\mathrm{EqVar}\) とし、変数記号は無限個あることを仮定する。

定義 2 (等式論理の代数言語)

代数言語 (algebraic language) は関数記号 (function symbol) からなる集合で各関数記号には項数 (arity) という自然数が割り当てられているとする。

また特に項数が $0$ である関数記号を定数記号 (constant symbol) という。言語の元を非論理記号 (non-logical symbol) という。関数記号は有限個でも無限個あっても良い。

便宜上、代数言語を集合ではなく組として扱うこともある。

例 3 (代数言語の例)

代数言語の例をいくつかあげる。

• 集合の言語 $\mathscr{L}_\mathsf{Set}:=\emptyset$ 。
• 群の言語 $\mathscr{L}_\mathsf{Grp}:=\{\mathtt{1},\mathrel{\hat{\cdot}},{-}^{\hat{-1}}\}$ 。項数は順に $0,2,1$ 。
• 環の言語 $\mathscr{L}_\mathsf{Ring}:=\{\mathtt{0},\mathtt{1},\mathrel{\hat{+}},\mathrel{\hat{-}},\mathrel{\hat{\cdot}}\}$ 。項数は順に $0,0,2,1,2$ 。
• 束の言語 $\mathscr{L}_\mathsf{Lat}:=\{\hat{\top},\hat{\bot},\mathrel{\hat{\land}},\mathrel{\hat{\lor}}\}$ 。項数は順に $0,0,2,2$ 。
• Boole代数の言語 $\mathscr{L}_\mathsf{BA}:=\{\hat{\top},\hat{\bot},\mathrel{\hat{\land}},\mathrel{\hat{\lor}},\mathrel{\hat{\lnot}}\}$ 。項数は順に $0,0,2,2,1$ 。
• $\mathcal{A}=\langle|\mathcal{A}|;0,1,+,-,\cdot\rangle$ を可換環としたとき $\mathcal{A}$-加群の言語は $\mathscr{L}_{\mathsf{Mod}_\mathcal{A}}:=\mathscr{L}_\mathsf{Grp}\cup\{\hat{a}\mid a\in|\mathcal{A}|\}$ とする。\(\hat{a}\) の項数は全て $1$ である。

定義 4 (等式論理の項)

$\mathscr{L}$ を代数言語とする。このとき $\mathscr{L}$-項 ($\mathscr{L}$-term) は以下のように帰納的に定義される文字列である。

1. 変数 $u,v,w,\ldots$ は $\mathscr{L}$-項である。
2. 関数記号 $\mathtt{f}$ に対し、その項数が $n$ であるとき、$\mathscr{L}$-項 $t_0,\ldots,t_{n-1}$ に対して $\mathtt{f}(t_0,\ldots,t_n)$ は$\mathscr{L}$-項である。

特に定数記号は $\mathscr{L}$-項であることに注意しよう。$\mathscr{L}$-項の集合を $\mathrm{EqTm}_\mathscr{L}$ と表す。

項数が $2$ の関数記号 $\mathtt{f}$ に対して $\mathtt{f}(s,t)$ の代わりに $s\mathrel{\mathtt{f}} t$ と中置記法 (infix notation) で表し、適当に括弧を補うことがある。

定義 5 ($\mathscr{L}$-項の例)

項の例をいくつかあげる。

• $(u\mathrel{\hat{\cdot}}\mathtt{1})^{\hat{-1}},\mathtt{1}\mathrel{\hat{\cdot}}v$ は $\mathscr{L}_\mathsf{Grp}$-項である。
• $(\mathtt{1}\mathrel{\hat{+}}\mathtt{1})\mathrel{\hat{\cdot}} (\mathrel{\hat{-}}\mathtt{0}),(u\mathrel{\hat{+}}\mathtt{1})\mathrel{\hat{\cdot}}((\mathrel{\hat{-}}\mathtt{0})\mathrel{\hat{\cdot}}v)$ は $\mathscr{L}_\mathsf{Ring}$-項である。
• $u\mathrel{\hat{\land}} (v\mathrel{\hat{\lor}}w),(\hat{\top}\mathrel{\hat{\land}}u)\mathrel{\hat{\lor}}\hat{\bot}$ は $\mathscr{L}_\mathsf{Lat}$-項である。
• $u\mathrel{\hat{\land}}(\mathrel{\hat{\lnot}} v),(\mathrel{\hat{\lnot}}\hat{\top})\mathrel{\hat{\land}}\hat{\bot}$ は $\mathscr{L}_\mathsf{BA}$-項である。

定義 6 (等式論理の論理式)

$\mathscr{L}$ を代数言語とする。このとき $\mathscr{L}$-論理式 ($\mathscr{L}$-formula) は以下のように定義される文字列である。

1. $\mathscr{L}$-項 $s,t$ に対して $s=t$ は$\mathscr{L}$-論理式である。

$\mathscr{L}$-論理式の集合を $\mathrm{EqFml}_\mathscr{L}$ と表す。

また等式論理の論理式を原子論理式 (atomic formula) と呼ぶこともある。

定義 7 (項の出現)

$\mathscr{L}$-項 $s$ が $\mathscr{L}$-項 $t$ に出現する (occur) あるいは単に現れるということを $\mathscr{L}$-項 $t$ の定義に沿って帰納的に定義する。

1. 変数 $u$ に対して $s$ が $u$ であるとき $u$ に $s$ が現れている。
2. $\mathscr{L}$-項 $f(t_0,\ldots,t_{n-1})$ に対して、ある $i<n$ が存在し $t_i$ に $s$ が現れているか、または $s$ が $f(t_0,\ldots,t_{n-1})$ であるとき、$s$ が $f(t_0,\ldots,t_{n-1})$ に現れている。

また$\mathscr{L}$-項 $s$ が $\mathscr{L}$-論理式 $\varphi$ に現れるということを定義する。

1. $t=r$ に $\mathscr{L}$-項 $s$ が現れるのは $t$ か $r$ のいずれかに現れるときである。

$\mathscr{L}$-項 $t$ に $s_0,\ldots,s_n$ が現れているとき $t(s_0,\ldots,s_n)$ などど表す。

定義 8 (項の代入)

$\mathscr{L}$-項 $s,t$ 、変数 $u$ に対して $s$ に現れる $u$ に $t$ を代入 (substitution) した結果 $s[u:=t]$ を $s$ の定義に沿って帰納的に定義する。

1. $s$ に $u$ が現れていないとき $s[u:=t]$ は $s$ である。
2. $u[u:=t]$ を $t$ のこととする。
3. $\mathtt{f}(t_0,\ldots,t_{n-1})[u:=t]$ を　$\mathtt{f}(t_0[u:=t],\ldots,t_{n-1}[u:=t])$　のこととする。

また $\mathscr{L}$-論理式 $\varphi$ 、 $\mathscr{L}$-項 $t$ 、変数 $u$ に対して $\varphi$ に現れる $u$ に $t$ を代入 (substitution) した結果 $\varphi[u:=t]$ を定義する。

1. $\varphi$ に $u$ が現れていないとき $\varphi[u:=t]$ は $\varphi$ である。
2. $(s=r)[u:=t]$ を $s[u:=t]=t[u:=t]$ のこととする。

また $s(u)$ に対して $s(u)[u:=t]$ を単に $s(t)$ と表す。

表記 9 (省略記法)

$\mathscr{L}$-項、$\mathscr{L}$-論理式などの「$\mathscr{L}$-」という接頭辞は、どの言語を指しているか明らかなとき、あるいは言語に拠らない議論をするとき省略する。

また命題論理と同様に以下の記法を用いる。

• 論理式の集合 $T$ を 公理系 (axiomatic system, axioms, axiomata) 、等式理論 (equational theory) 、あるいは単に理論 (theory) という。
• 理論 $T$ と論理式 $\varphi$ に対して $T+\varphi$ で $T\cup\{\varphi\}$ を表す。

2.2 等式論理のモデル

定義 10 (代数構造)

$\mathscr{L}$ を言語とする。このとき $\mathscr{L}$-代数構造 ($\mathscr{L}$-algebraic structure) $\mathcal{M}$ は領域 (domain) あるいは宇宙 (universe) 、台集合 (underlying set) と言われる空でない集合 $M$ と以下に定義される$\mathscr{L}$-解釈 ($\mathscr{L}$-interpretation) ${-}^\mathcal{M}$ の組 $\langle M;{-}^\mathcal{M}\rangle$ である。

$\mathscr{L}$-解釈 ${-}^\mathcal{M}$ は以下を満たす言語 $\mathscr{L}$ からの写像である。

• 関数記号 $\mathtt{f}\in\mathscr{L}$ に対して $\mathtt{f}$ の項数が $n$ であるとき、$\mathtt{f}^\mathcal{M}\colon M^n\to M$ である。

定数記号の解釈は一つの $M$ の要素を返す関数となる。よってその返す値と同一視することで定数記号 $\mathtt{c}$ に対して $\mathtt{c}^\mathcal{M}\in M$ と見做すことができることに注意する。このような同一視を今後断りなく行うことに注意する。

代数構造 $\mathcal{M}$ が与えられたとき、$|\mathcal{M}|$ を $\mathcal{M}$ の台集合を表すことにする。また数学の慣習に基づき構造 $\mathcal{M}$ とその台集合 $|\mathcal{M}|$ を誤解を与えない範囲で同一視する。例えば $a\in |\mathcal{M}|$ の代わりに $a\in\mathcal{M}$ と表すことがある。

また $\mathcal{M}=\langle M;{-}^\mathcal{M}\rangle$ と表す代わりに解釈後の関数、関係をリストし $\mathcal{M}=\langle M;\mathtt{f}_0^\mathcal{M},\ldots,\mathtt{f}_i^\mathcal{M}\rangle$ と表すことがある。

例 11 (代数構造の例)

任意の群 $\mathcal{G}:=\langle|\mathcal{G}|;e,\cdot,{-}^{-1}\rangle$ は $\mathtt{1}^\mathcal{G}:=e,\hat{\cdot}^\mathcal{G}:=\cdot,{{-}^{\hat{-1}}}^\mathcal{G}:={-}^{-1}$ と定めることで $\mathscr{L}_\mathsf{Grp}$-構造として見做すことができる。しかし、別に群でなくても $a\in A,f\colon A^2\to A,g\colon A\to A $ に対して $\langle A;a,f,g\rangle$ は同様に $\mathscr{L}_\mathsf{Grp}$-構造として見做すことができる。

定義 12 (項の解釈)

$\mathscr{L}$-代数構造 $\mathcal{M}=\langle M;{-}^\mathcal{M}\rangle$ と $\mathscr{L}$-閉項 $t$ に対して $t^\mathcal{M}\in M$ を帰納的に定義する。

• $\mathtt{f}(t_0,\ldots,t_{n-1})$ に対して $(\mathtt{f}(t_0,\ldots,t_{n-1}))^\mathcal{M}$ を $\mathtt{f}^\mathcal{M}(t_0^\mathcal{M},\ldots,t_{n-1}^\mathcal{M})$ と定める。

定義 13 (拡大と縮約)

言語 $\mathscr{L}\subseteq\mathscr{L}'$ とし、$\mathcal{M}$ を $\mathscr{L}$-代数構造とし、$\mathcal{M}'$ を $\mathscr{L}'$-代数構造とする。$|\mathcal{M}|=|\mathcal{M}'|$ とし、$\mathtt{f}\in\mathscr{L}$ に対し $\mathtt{f}^\mathcal{M}=\mathtt{f}^{\mathcal{M}'}$ が成り立つとする。このとき $\mathcal{M}'$ を $\mathcal{M}$ の拡大 (expansion) といい、$\mathcal{M}$ を $\mathcal{M}'$ の縮約 (reduct) という。

例 14 (拡大と縮約の例)

任意の環 $\mathcal{R}=\langle|\mathcal{R}|;\mathtt{0}^\mathcal{R},\mathtt{1}^\mathcal{R},\hat{+}^\mathcal{R},\hat{-}^\mathcal{R},\hat{\cdot}^\mathcal{R}\rangle$ はその加法群 $\mathcal{R}^+=\langle|\mathcal{R}|;\mathtt{0}^\mathcal{R},\hat{+}^\mathcal{R},{-}^\mathcal{R}\rangle$ の拡張となる。ここで群の言語は $\{\mathtt{1},\hat{\cdot},{-}^{\hat{-1}}\}$ であったが記号を変えて $\{\mathtt{0},\hat{+},\hat{-}\}$ としても本質的になにも変わらない。実際、Abel群に対してはこのように書かれることが多い。 一方、加法群と違い、乗法群 $\mathcal{R}^\times=\langle|\mathcal{R}|\setminus\{\mathtt{0}^\mathcal{R}\};\mathtt{0}^\mathcal{R},\hat{+}^\mathcal{R},{-}^\mathcal{R}\rangle$ は領域がことなるため拡張にはならない。

定義 15 (名前)

$\mathscr{L}$-代数構造 $\mathcal{M}$ に対して言語 $\mathscr{L}(\mathcal{M})$ と $\mathscr{L}(\mathcal{M})$-代数構造 $\mathcal{M}_\mathrm{par}$ を定義する。

• $\mathscr{L}(\mathcal{M})$ には $\mathscr{L}$ の元に加え、$a\in|\mathcal{M}|$ に対する定数記号 $\underline{a}$ を持つ。この定数記号 $\underline{a}$ を $a$ の 名前(name) やパラメータ (parameter) という。名前を単に $a$ と表すこともある。
• $\mathcal{M}_\mathrm{par}$ は $\mathcal{M}$ の拡大であり、$\underline{a}^{\mathcal{M}_\mathrm{par}}:=a$ とする。

誤解を生じないとき $\mathcal{M}_\mathrm{par}$ を単に $\mathcal{M}$ と表す。

定義 16 (充足可能性関係)

$\mathscr{L}$-代数構造 $\mathcal{M}$ と $\mathscr{L}(\mathcal{M})$-論理式 $s(u_0,\ldots,u_{n-1})=t(v_0,\ldots,v_{m-1})$ に対し 充足可能性関係 (satisfiability relation) $\mathcal{M}\models s(u_0,\ldots,u_{n-1})=t(v_0,\ldots,v_{m-1})$ を定義する。 ここで $s(u_0,\ldots,u_{n-1})=t(v_0,\ldots,v_{m-1})$ に現れる変数は $u_0,\ldots,u_{n-1},v_0,\ldots,v_{m-1}$ に限るとする。

1. 　$\mathcal{M}\models s(u_0,\ldots,u_{n-1})=t(v_0,\ldots,v_{m-1})$ となるのは任意の $a_0,\ldots,a_{n-1},b_0,\ldots,b_{m-1}\in |\mathcal{M}|$ に対して $(s(u_0,\ldots,u_{n-1})[u_0:=\underline{a_0}]\cdots[u_{n-1}:=\underline{a_{n-1}}])^{\mathcal{M}_\mathrm{par}}=(t(v_0,\ldots,v_{m-1})[v_0:=\underline{b_0}]\cdots[v_{m-1}:=\underline{b_{m-1}}])^{\mathcal{M}_\mathrm{par}})$ が成り立つことである。

ここで $\mathcal{M}\models s(u_0,\ldots,u_{n-1})=t(v_0,\ldots,v_{m-1})$ に含まれる $=$ は等号記号だが、$(s(u_0,\ldots,u_{n-1})[u_0:=\underline{a_0}]\cdots[u_{n-1}:=\underline{a_{n-1}}])^{\mathcal{M}_\mathrm{par}}=(t(v_0,\ldots,v_{m-1})[v_0:=\underline{b_0}]\cdots[v_{m-1}:=\underline{b_{m-1}}])^{\mathcal{M}_\mathrm{par}})$　に表れる $=$ は実際の等号であることに注意されたい。また $\models$ に対していくつかの用語を定める。

• $T$ を理論とし、任意の $\varphi\in T$ に対して $\mathcal{M}\models\varphi$ となっているとする。このとき $\mathcal{M}$ を $T$ のモデル (model) であるといい、$\mathcal{M}\models\varphi$ と表す。
• $T$ の任意のモデル $\mathcal{M}$ に対して $\mathcal{M}\models\varphi$ であるとき $\varphi$ は $T$ からの論理的帰結 (logical consequence) であるといい、$T\models \varphi$ と表す。

例 17 (モデルの例)

$\mathscr{L}_\mathsf{Grp}$-理論 $\mathsf{Grp}$ を以下の論理式からなるものとする。

• $u\mathrel{\hat{\cdot}}(v\mathrel{\hat{\cdot}}w)=(u\mathrel{\hat{\cdot}}v)\mathrel{\hat{\cdot}}w$ 。
• $u\mathrel{\hat{\cdot}}\mathtt{0}=u$ 。
• $u\mathrel{\hat{\cdot}}(u^{\hat{-1}})=\mathtt{0}$ 。

$\mathsf{Grp}$ のモデルは群そのものである。

$\mathscr{L}_\mathsf{Ring}$-理論 $\mathsf{Ring}$ を以下の論理式からなるものとする。

• $u\mathrel{\hat{+}}(v\mathrel{\hat{+}}w)=(u\mathrel{\hat{+}}v)\mathrel{\hat{+}}w$ 。
• $u\mathrel{\hat{+}}\mathtt{0}=u$ 。
• $u\mathrel{\hat{+}}(\mathrel{\hat{-}}u)=\mathtt{0}$ 。
• $u\mathrel{\hat{+}}v=v\mathrel{\hat{+}}u$ 。
• $u\mathrel{\hat{\cdot}} (v\mathrel{\hat{\cdot}} w)=(u\mathrel{\hat{\cdot}} v)\mathrel{\hat{\cdot}} w$ 。
• $u\mathrel{\hat{\cdot}} (v\mathrel{\hat{+}}w)=(u\mathrel{\hat{\cdot}} v)\mathrel{\hat{+}}(u\mathrel{\hat{\cdot}} w)$ 。
• $u\mathrel{\hat{\cdot}}\mathtt{1}=u$ 。

$\mathsf{Ring}$ のモデルも同様に環である。

言語 $\mathscr{L}_{\mathsf{Mod}_\mathcal{A}}$ 上の理論 $\mathsf{Mod}_\mathcal{A}$ はアーベル群の公理と任意の \(a,b\in |\mathcal{A}|\) に対して以下の論理式からなるものとする。

• $\hat{a}(x\mathrel{\hat{+}}y)=\hat{a}(x)\mathrel{\hat{+}}\hat{a}(y)$ 。
• $\widehat{a\mathrel{+_\mathcal{A}}b}(x)=\hat{a}(x)\mathrel{\hat{+}}\hat{b}(x)$ 。
• $\widehat{a\mathrel{\cdot_\mathcal{A}} b}(x)=\hat{a}(\hat{b}(x))$ 。
• $\widehat{1_{\mathcal{A}}}(x)=x$

言語 $\mathscr{L}_\mathsf{Set}$ 上の理論 \(\emptyset\) のモデルは 空でない集合 \(X\) に対して \(\langle X\rangle\) という形をした構造である。これは空でない集合と同一視できる。

言語 $\mathscr{L}_\mathsf{SGrp}:=\{\hat{\cdot}\}$ とし、理論 $\mathsf{SGrp}$ を

• $u\mathrel{\hat{\cdot}}(v\mathrel{\hat{\cdot}}w)=(u\mathrel{\hat{\cdot}}v)\mathrel{\hat{\cdot}}w$ 。

とする。このとき理論 $\mathsf{SGrp}$ のモデルは空でない半群全体となる。

2.3 代数構造の理論

定義 18 (準同型、同型)

$\mathscr{L}$-代数構造 $\mathcal{M},\mathcal{N}$ に対して $\sigma\colon|\mathcal{M}|\to|\mathcal{N}|$ が準同型射 (homomorphism) であるとは、任意の $\mathtt{f}\in\mathscr{L}$ 、$a_0,\ldots,a_{n-1}\in|\mathcal{M}|$ に対し $\sigma(\mathtt{f}^\mathcal{M}(a_0,\ldots,a_{n-1}))=\mathtt{f}^\mathcal{N}(\sigma(a_0),\ldots,\sigma(a_{n-1}))$ が成り立つことである。すなわち、以下の図式を可換にするような写像である。

また準同型 $\sigma\colon|\mathcal{M}|\to|\mathcal{N}|,\tau\colon|\mathcal{N}|\to|\mathcal{M}|$ が存在し $\tau\circ\sigma =\mathrm{id}_\mathcal{M},\sigma\circ\tau =\mathrm{id}_\mathcal{N}$ となるとき $\mathcal{M}$ と $\mathcal{N}$ は同型 (isomorphic))であるといい $\mathcal{M}\cong\mathcal{N}$ と表し、$\sigma,\tau$ を同型射 (isomorphism) であるという。 ここで $\mathrm{id}_\mathcal{M}\colon|\mathcal{M}|\to|\mathcal{M}|,\mathrm{id}_\mathcal{M}(a)=a,\mathrm{id}_\mathcal{N}\colon|\mathcal{N}|\to|\mathcal{N}|,\mathrm{id}_\mathcal{N}(b)=b$ とする。

定義 19 (部分代数)

$\mathscr{L}$-代数構造 $\mathcal{M},\mathcal{N}$ に対して、$\mathcal{N}$ が $\mathcal{M}$ の部分代数 (subalgebra) であるとは $|\mathcal{N}|\subseteq|\mathcal{M}|$ かつ、任意の $\mathtt{f}\in\mathscr{L}$ 、任意の $b_0,\ldots,b_{n-1}\in|\mathcal{N}|$ に対し $\mathtt{f}^\mathcal{N}(b_0,\ldots,b_{n-1})=\mathtt{f}^\mathcal{M}(b_0,\ldots,b_{n-1})$ を満たすことである。

定義 20 (直積代数)

$\{\mathcal{M}_{i\in I}\}$ を \(I\) によって添字付けられた $\mathscr{L}$-代数構造の族とする。$\{\mathcal{M}_{i\in I}\}$ の直積 (direct product) 、\(\prod_{i\in I}\mathcal{M}_i\) は以下のように定義される $\mathscr{L}$-代数構造である。

1. 台集合は台集合の直積とする。すなわち \(|\prod_{i\in I}\mathcal{M}_i|:=\prod_{i\in I}|\mathcal{M}_i|\) とする。
2. \(n\)-変数関数記号 \(\mathtt{f}\in\mathscr{L}\) に対して \(\mathtt{f}^{\prod_{i\in I}\mathcal{M}_i}\colon\left(\prod_{i\in I}\mathcal{M}_i\right)^n\to\prod_{i\in I}\mathcal{M}_i\) を \(\mathtt{f}^{\prod_{i\in I}\mathcal{M}_i}(a_0,\ldots,a_{n-1}):=\lambda i\in I.\mathtt{f}^{\mathcal{M}_i}(a_0(i),\ldots,a_{n-1}(i))\) とする。ここで \(\lambda i\in I.\mathtt{f}^{\mathcal{M}_i}(a_0(i),\ldots,a_{n-1}(i))\) は \(i\mapsto\mathtt{f}^{\mathcal{M}_i}(a_0(i),\ldots,a_{n-1}(i))\) となる写像を表すものとする。

命題2.3.3（代数構造の同型に対する必要十分条件）

$\mathcal{M}\cong\mathcal{N}$ であるのは全単射準同型 $\upsilon\colon\mathcal{M}\to\mathcal{N}$ が存在するときであり、またそれに限る。

証明　$\mathcal{M}\cong\mathcal{N}$ であると仮定する。仮定より準同型 $\sigma\colon\mathcal{M}\to\mathcal{N},\tau\colon\mathcal{N}\to\mathcal{M}$ で $\sigma\circ\tau,\tau\circ\sigma$ が恒等となるものを取る。$\sigma,\tau$ は互いに逆写像であり、よって全単射である。

逆を示す。$\upsilon\circ\upsilon^{-1},\upsilon^{-1}\circ\upsilon$ が恒等になるのは明らかである。よって $\upsilon^{-1}\colon\mathcal{N}\to\mathcal{M}$ が準同型となることを確認すれば良い。 $\upsilon$ は全単射であるから、ある $a_0,\ldots,a_{n-1}\in|\mathcal{M}|$ が存在して $\upsilon(a_0)=b_0,\ldots,\upsilon(a_{n-1})=b_{n-1}$ である。 よって $\upsilon^{-1}(\mathtt{f}^\mathcal{N}(b_0,\ldots,b_{n-1}))=\upsilon^{-1}(\mathtt{f}^\mathcal{N}(\upsilon(a_0),\ldots,\upsilon(a_{n-1})))$ であり、$\upsilon$ は準同型であるから $\upsilon^{-1}(\mathtt{f}^\mathcal{N}(\upsilon(a_0),\ldots,\upsilon(a_{n-1})))=\upsilon^{-1}(\upsilon(\mathtt{f}^\mathcal{M}(a_0,\ldots,a_{n-1})))$ となる。 従って $\upsilon^{-1}(\upsilon(\mathtt{f}^\mathcal{M}(a_0,\ldots,a_{n-1})))=\mathtt{f}^\mathcal{M}(a_0,\ldots,a_{n-1})$　であり、$a_0=\upsilon^{-1}(b_0),\ldots,a_{n-1}=\upsilon^{-1}(b_{n-1})$ より良い。□

定義2.3.4（合同関係）

$\mathcal{M}$ を代数構造とし、$\equiv$ を $|\mathcal{M}|$ 上の同値関係で $\mathtt{f}\in\mathscr{L}$ に対して $\mathtt{f}^\mathcal{M}$ と両立する、すなわち任意の $a_0,\ldots,a_{n-1},b_0,\ldots,b_{n-1}\in |\mathcal{M}|$ に対して、任意の $i<n$ について $a_i\equiv b_i$ $\equiv$ であるならば $\mathtt{f}^\mathcal{M}(a_0,\ldots,a_{n-1})\equiv\mathtt{f}^\mathcal{M}(b_0,\ldots,b_{n-1})$ が成り立つとき $\equiv$ は $\mathcal{M}$ 上の合同関係 (congruence relation) である、あるいは同値関係 $\equiv$ は $\mathtt{f}^\mathcal{M}$ に対して　well-definedであるという。

定義2.3.5（剰余代数）

$\mathcal{M}$ を代数構造とし、$\equiv$ を $\mathcal{M}$ 上の合同関係とする。剰余代数 (factor algebra, quotient algebra) $\mathcal{M}/{\equiv}:=\langle|\mathcal{M}|/{\equiv};{-}^{\mathcal{M}/{\equiv}}\rangle$ を以下のように定める。

• $|\mathcal{M}|/{\equiv}$ は $|\mathcal{M}|$ の $\equiv$ による商集合とし $a\in|\mathcal{M}|$ に対して $[a]_\equiv$ を $\equiv$ による同値類とする。
• $\mathtt{f}\in\mathscr{L}$ に対して $\mathtt{f}^{\mathcal{M}/{\equiv}}([a_0]_\equiv,\ldots,[a_{n-1}]_\equiv):=[\mathtt{f}^\mathcal{M}(a_0,\ldots,a_{n-1})]_\equiv$ とする。

例2.3.6（剰余代数の例）

$\mathcal{G}$ を群、$\mathcal{H}$ を $\mathcal{G}$ の正規部分群、すなわち $\mathcal{H}$ は $\mathcal{G}$ の部分代数で、任意の $g\in|\mathcal{G}|,h\in|\mathcal{H}|$ に対し $(g\hat{\cdot}^\mathcal{G} h){\hat{\cdot}}^\mathcal{G}\left(g^{\hat{-1}^\mathcal{G}}\right)\in|\mathcal{H}|$ であるとする。$|\mathcal{G}|$ 上の合同関係　$\equiv_\mathcal{H}$ を $x\equiv_\mathcal{H} y:\Leftrightarrow x\hat{\cdot}^\mathcal{G}\left(y^{\hat{-1}^\mathcal{G}}\right)\in|\mathcal{H}|$ と定める。 このとき $\mathcal{G}/{\equiv_\mathcal{H}}$ を $\mathcal{G}/\mathcal{H}$ と表す。

$\mathcal{M}$ を可換環、$\mathcal{I}:=\langle|\mathcal{I}|;\mathtt{0}^\mathcal{I},\mathtt{1}^\mathcal{I},\hat{+}^\mathcal{I},\hat{-}^\mathcal{I},\hat{\cdot}^\mathcal{I}\rangle$ を $\mathcal{M}$ のイデアル、すなわち以下を満たすとする。

• $\langle|\mathcal{I}|;\mathtt{0}^\mathcal{I},\hat{+}^\mathcal{I},\hat{-}^\mathcal{I}\rangle$ は $\langle|\mathcal{M}|;\mathtt{0}^\mathcal{M},\hat{+}^\mathcal{M},\hat{-}^\mathcal{M}\rangle$ の部分構造である。
• 任意の $a\in|\mathcal{M}|,x\in|\mathcal{I}|$ に対し $a\hat{\cdot}^\mathcal{M}x\in|\mathcal{I}|$ である。

このとき上記の例と同様に $\equiv_\mathcal{I}$ を定義でき $\mathcal{M}/{\equiv_\mathcal{I}}$ を $\mathcal{M}/\mathcal{I}$ を表す。

補題2.3.7（剰余代数と準同型）

代数構造 $\mathcal{M}$ と合同関係 $\equiv$ に対して $\pi_\equiv\colon|\mathcal{M}|\to|\mathcal{M}|/{\equiv},\pi_\equiv(a):=[a]_\equiv$ とする。このとき $\pi_\equiv$ は準同型となる。この準同型を $\equiv$ に対する自然な準同型という。

証明　剰余代数の定義より明らかである。□

補題2.3.8（準同型と合同関係）

代数構造 $\mathcal{M},\mathcal{N}$ 、準同型 $\sigma\colon|\mathcal{M}|\to|\mathcal{N}|$ に対して $|\mathcal{M}|$ 上の二項関係 $\equiv_\sigma$ を $a\equiv_\sigma b:\Leftrightarrow\sigma(a)=\sigma(b)$ とする((これを $\sigma$ による核 (kernel) ということがある。))。このとき $\equiv_\sigma$ は合同関係である。

証明　$\equiv_\sigma$ が同値関係であることは明らかである。よって関数と両立することを示そう。 今 $\mathtt{f}$ の項数を $n$ とし任意の $i<n$ に対して $a_i\equiv_\sigma b_i$ であると仮定し、$\mathtt{f}^\mathcal{M}(a_0,\ldots,a_{n-1})\equiv_\sigma \mathtt{f}^\mathcal{M}(b_0,\ldots,b_{n-1})$ 、すなわち $\sigma(\mathtt{f}^\mathcal{M}(a_0,\ldots,a_{n-1}))=\sigma(\mathtt{f}^\mathcal{M}(b_0,\ldots,b_{n-1}))$ を示せば良い。 $\sigma$ が準同型であるという仮定から $\sigma(\mathtt{f}^\mathcal{M}(a_0,\ldots,a_{n-1}))=\mathtt{f}^\mathcal{N}(\sigma(a_0),\ldots,\sigma(a_{n-1}))$ であり、 $\equiv_\sigma$ の定義から $\mathtt{f}^\mathcal{N}(\sigma(a_0),\ldots,\sigma(a_{n-1}))=\mathtt{f}^\mathcal{N}(\sigma(b_0),\ldots,\sigma(b_{n-1}))$ 、よってもう一度 $\sigma$ が準同型であることから $\mathtt{f}^\mathcal{N}(\sigma(b_0),\ldots,\sigma(b_{n-1}))=\sigma(\mathtt{f}^\mathcal{M}(b_0,\ldots,b_{n-1}))$ 。□

定理2.3.9（準同型定理 (homomorphism theorem) ）

全射準同型 $\sigma\colon|\mathcal{M}|\to|\mathcal{N}|$ に対して、同型 $\tau_{\equiv_\sigma}\colon|\mathcal{M}/{\equiv_\sigma}|\to|\mathcal{N}|$ が存在して $\sigma=\tau_{\equiv_\sigma}\circ\pi_{\equiv_\sigma}$ となる。 ここで $a\equiv_\sigma b:\Leftrightarrow\sigma(a)=\sigma(b)$ 、$\pi_{\equiv_\sigma}\colon|\mathcal{M}|\to|\mathcal{M}/{\equiv_\sigma}|,\pi_{\equiv_\sigma}(a)=[a]_{\equiv_\sigma}$ とする。

証明　まず $\tau_{\equiv_\sigma}([a]_{\equiv_\sigma}):=\sigma(a)$ とする。これが写像となることを示す。左全域性は明らかなので右一意性を示そう。 $[a]_{\equiv_\sigma}=[b]_{\equiv_\sigma}$ とすれば $\equiv_\sigma$ の定義から、$\sigma(a)=\sigma(b)$ であり良い。 同様に逆も言えるため左一意性、すなわち $\tau_{\equiv_\sigma}$ が単射であることも従う。また $\sigma$ が全射であることから $\tau_{\equiv_\sigma}$ も全射である。命題2.3.3より 準同型であることを示せば十分である。 剰余代数の定義から $\tau_{\equiv_\sigma}(\mathtt{f}^{\mathcal{M}/{\equiv_\sigma}}([a_0]_{\equiv_\sigma},\ldots,[a_{n-1}]_{\equiv_\sigma}))=\tau_{\equiv_\sigma}([\mathtt{f}^\mathcal{M}(a_0,\ldots,a_{n-1})]_{\equiv_\sigma})$ であり、$\tau_{\equiv_\sigma}$ の定義から $\tau_{\equiv_\sigma}([f^\mathcal{M}(a_0,\ldots,a_{n-1})]_{\equiv_\sigma})=\sigma(f^\mathcal{M}(a_0,\ldots,a_{n-1}))$ である。 $\sigma$ が準同型であることから $\sigma(\mathtt{f}^\mathcal{M}(a_0,\ldots,a_{n-1}))=\mathtt{f}^\mathcal{N}(\sigma(a_0),\ldots,\sigma(a_{n-1}))$ であり $\tau_{\equiv_\sigma}$ の定義が $\mathtt{f}^\mathcal{N}(\sigma(a_0),\ldots,\sigma(a_{n-1}))=\mathtt{f}^\mathcal{N}(\tau_{\equiv_\sigma}([a_0]_{\equiv_\sigma},\ldots,[a_{n-1}]_{\equiv_\sigma}))$ となる。□

系2.3.10

準同型 $\sigma\colon|\mathcal{M}|\to|\mathcal{N}|$ と $|\mathcal{M}|$ 上の合同関係 $\equiv_\sigma$ は $a\equiv_\sigma b$ ならば $\sigma(a)=\sigma(b)$ を満たすとする。 このとき準同型 $\tau_{\equiv_\sigma}\colon|\mathcal{M}/{\equiv}|\to|\mathcal{N}|$ が存在し $\sigma=\tau_{\equiv_\sigma}\circ\pi_{\equiv_\sigma}$ となる。 ただし $\pi_{\equiv_\sigma}\colon|\mathcal{M}|\to|\mathcal{M}/{\equiv_\sigma}|,\pi_{\equiv_\sigma}(a)=[a]_{\equiv_\sigma}$ とする。

証明　定理2.3.9の証明とほとんど同様で良い。□

例2.3.11（準同型定理の具体例）

群準同型 $\sigma\colon|\mathcal{G}|\to|\mathcal{H}|$ に対して $\mathrm{Ker}(\sigma):=\{g\in|\mathcal{G}|\mid\sigma(g)=\mathtt{0}^\mathcal{H}\}$ とする。このとき $\langle \mathrm{Ker}(\sigma),\mathtt{0}^\mathcal{G},\hat{\cdot}^\mathcal{G},{-}^{\hat{-1}^\mathcal{G}}\rangle$ は $\mathcal{G}$ の部分群であり、例2.2.6で定められる同値関係を $\equiv_{\mathrm{Ker}(\sigma)}$ とすれば $g_0\equiv_{\mathrm{Ker}(\sigma)}g_1$ と $g_0\equiv_\sigma g_1$ は同値であり、従って定理2.3.9及び系2.3.10から以下の群論に於ける準同型定理が従う。

• 群準同型 $\sigma\colon|\mathcal{G}|\to|\mathcal{H}|$ 、自然な準同型 $\pi\colon|\mathcal{G}|\to|\mathcal{G}/\equiv_{\mathrm{Ker(\sigma)}}|$ に対して、準同型 $\tau\colon |\mathcal{G}/\equiv_{\mathrm{Ker(\sigma)}}|\to|\mathcal{H}|$ が存在して $\sigma=\tau\circ\pi$ であり、また $\tau$ は $\mathcal{G}/\equiv_{\mathrm{Ker(\sigma)}}$ から $\langle\mathrm{Im}(\sigma),\underline{0}^\mathcal{H},+^\mathcal{H},-^\mathcal{H}\rangle$ への同型射である。

2.4. 等式論理の形式的証明

定義2.4.1（等式理論）

理論 $T$ 論理式 $\varphi$ に対して $T\vdash\varphi$ を帰納的に定義する。

1. $(\mathsf{refl})$　任意の項 $t$ に対して $T\vdash t=t$ である。

2. $(T)$　任意の $\varphi\in T$ に対して $T\vdash\varphi$ である。

3. $(\mathsf{sym})$　任意の項 $s,t$ に対して $T\vdash s=t$ ならば $T\vdash t=s$ である。

4. $(\mathsf{trans})$　任意の項 $s,t,r$ に対して $T\vdash s=t$ かつ $T\vdash t=r$ ならば $T\vdash s=r$ である。

5. $(\mathsf{sub})$　任意の変数 $u$ 、項 $s(u),t(u),r$ に対して $T\vdash s(u)=t(u)$ ならば $T\vdash s(r)=t(r)$ である。

6. $(\mathsf{comp})$　任意の関数記号 $f\in\mathscr{L}$ 、任意の項 $s_0,\ldots,s_{n-1},t_0,\ldots,t_{n-1}$ に対して、全ての$i<n$　について $T\vdash s_i=t_i$ ならば $T\vdash f(s_0,\ldots,s_{n-1})=f(t_0,\ldots,t_{n-1})$ である。

$\vdash$ に関して命題論理と同様に用語を定める。

• $T\vdash\varphi$ であるとき $T$ から $\varphi$ は証明可能 (provable) であるという。また $\emptyset\vdash\varphi$ であるとき単に証明可能であるといい、$\vdash\varphi$ と表す。
• $\mathrm{Th}(T):=\{\varphi\in\mathrm{EqFml}\mid T\vdash\varphi\}$ とする。また言語を明示するとき $\mathrm{Th}_\mathscr{L}(T)$ と表す。

2.5. Birkhoffの完全性定理、$\mathsf{HSP}$ 定理

定義2.5.1（生成）

代数構造 $\mathcal{M}$ 、$X\subseteq|\mathcal{M}|$ とする。このとき $X\subseteq\mathcal{N}$ で $\mathcal{M}$ の部分代数のなか、領域の包含関係において最小であるとき、$\mathcal{N}$ を $X$ によって生成される (generated) 部分代数であるという。

定義2.5.2（自由 $\mathcal{K}$-代数）

$\mathcal{K}$ を代数構造からなるクラスとする。このとき $\mathcal{M}\in\mathcal{K}$ が $X$ によって生成される自由 $\mathcal{K}$-代数 (free $\mathcal{K}$-代数) であるとは以下を満たすことである。

• $\mathcal{M}$ は $X$ で生成される。
• 任意の $\mathcal{N}\in\mathcal{K}$ 、写像 $\sigma\colon X\to|\mathcal{N}|$ に対し、ある準同型 $\overline{\sigma}\colon|\mathcal{M}|\to|\mathcal{N}|$ で $\overline{\sigma}$ は $\sigma$ の拡大である、すなわち任意の $x\in X$ に対して $\sigma(x)=\overline{\sigma}(x)$ となるものが一意に存在する。

命題2.5.3（自由生成と濃度）

代数構造 $\mathcal{M},\mathcal{N}\in\mathcal{K}$ でそれぞれ集合 $X,Y$ によって自由生成されていて、$X,Y$ が等濃であれば $\mathcal{M}\cong\mathcal{N}$ である。

証明　全単射 $\sigma\colon X\to Y$ を取る。 自由代数の定義から $\sigma,\sigma^{-1}$ は準同型 $\overline{\sigma}\colon|\mathcal{M}|\to|\mathcal{N}|,\overline{\sigma^{-1}}\colon|\mathcal{N}|\to|\mathcal{M}|$ に拡張され $\overline{\sigma^{-1}}\circ\overline{\sigma}$ は $X$ 上の恒等写像の拡張となる準同型 $|\mathcal{M}|\to|\mathcal{M}|$ で拡張の一意性から $\overline{\sigma^{-1}}\circ\overline{\sigma}=\mathrm{id}_{|\mathcal{M}|}$ 、 同様に $\overline{\sigma}\circ\overline{\sigma^{-1}}=\mathrm{id}_{|\mathcal{N}|}$ であり、$\mathcal{M}\cong\mathcal{N}$ である。

参考文献

[田中19] 田中一之、数学基礎論序説、裳華房、2019。

[Sankappanavar–Burris] H.P. Sankappanavar, S. Burris, A course in universal algebra, Graduate Texts Math 78, 1981.