正則論理

要点：2 は像が「経由するモノ射のうち最小のもの」であることから、3・4 は像の引き戻し安定性から従う。

要点：項・論理式の構成に関する帰納法による。$\exists$ の段は、束縛変数を付け替えたうえで Beck–Chevalley（lem-reglog-sub の 3）を使う。

導出の長さに関する帰納法で、各規則が「$M$ で成り立つ列から $M$ で成り立つ列を作る」こと、公理が $M$ で成り立つことを示す。$\mathbb T$ の列は $M$ がモデルなので成り立つ。以下 $\{\vec x\mid\varphi\}$ を $[\varphi]$ と略すことがある。
恒等・切断・連言。 $\operatorname{Sub}(M\vec x)$ が順序集合で、$\wedge$ がその最大下界、$\top$ が最大元であることから直ちに従う。
代入。 $[\varphi]\le[\psi]$ なら、$\sigma^*$ が単調なので $\sigma^*[\varphi]\le\sigma^*[\psi]$ であり、lem-reglog-substitution によりこれは $\{\vec y\mid\varphi[\vec s/\vec x]\}\le\{\vec y\mid\psi[\vec s/\vec x]\}$ である。
等号。 $\{x\mid x=x\}=\langle\operatorname{id},\operatorname{id}\rangle^*\Delta$ は、$\langle\operatorname{id},\operatorname{id}\rangle$ が $\Delta$ を経由するので最大元である。次に $\vec z$ を $x,x'$ を含む文脈とし、代入 $[x'/x]$ に対応する射を $\tau\colon M\vec z\to M\vec z$（$x$ 成分を $x'$ 成分で置き換え、他の成分はそのまま）とする。lem-reglog-substitution により $\{\vec z\mid\varphi[x'/x]\}=\tau^*\{\vec z\mid\varphi\}$ である。$\{\vec z\mid(x=x')\wedge\varphi\}$ の代表を $m\colon P\rightarrowtail M\vec z$ とする。$m$ は $\pi_x$ と $\pi_{x'}$ の等化子を経由するので $\pi_x\circ m=\pi_{x'}\circ m$ であり、成分ごとに比べて $\tau\circ m=m$ である。$m$ は $\{\vec z\mid\varphi\}$ を経由するから $\tau\circ m$ もそうであり、引き戻しの普遍性により $m\le\tau^*\{\vec z\mid\varphi\}$ である。
存在。 $y$ のソートを $B$、$\pi\colon M\vec x\times MB\to M\vec x$ を射影とする。文脈 $\vec x$ の $\psi$ を文脈 $\vec x,y$ で解釈すると、lem-reglog-substitution により $\{\vec x,y\mid\psi\}=\pi^*\{\vec x\mid\psi\}$ である。lem-reglog-sub の 2 により
$$ \{\vec x,y\mid\varphi\}\le\pi^*\{\vec x\mid\psi\}\iff\exists_\pi\{\vec x,y\mid\varphi\}\le\{\vec x\mid\psi\} $$
であり、右辺の左側は $\{\vec x\mid\exists y\,\varphi\}$ なので、存在規則の両方向が $M$ で成り立つ列を保つ。
Frobenius。 同じ記号で、lem-reglog-sub の 4 と lem-reglog-substitution から
$$ [\varphi\wedge\exists y\,\psi]=[\varphi]\wedge\exists_\pi\{\vec x,y\mid\psi\}=\exists_\pi\bigl(\pi^*[\varphi]\wedge\{\vec x,y\mid\psi\}\bigr)=\exists_\pi\{\vec x,y\mid\varphi\wedge\psi\}=[\exists y\,(\varphi\wedge\psi)] $$
であり、Frobenius の列は（等号で）成り立つ。$\square$

ソート $X,Y,Z,W$ と関係記号 $R\rightarrowtail XY$、$S\rightarrowtail YZ$、$T\rightarrowtail ZW$ からなる言語の構造 $M$ を、与えられた対象と関係で定める。定義と lem-reglog-substitution（文脈を広げると射影で引き戻される）から $\{x,y,z\mid R(x,y)\wedge S(y,z)\}=p_{XY}^*R\wedge p_{YZ}^*S$ なので、$\{x,z\mid\exists y\,(R(x,y)\wedge S(y,z))\}=S\circ R$ である。同様にして
$$ T\circ(S\circ R)=\{x,w\mid\Phi\},\quad\Phi:=\exists z\,\bigl(\exists y\,(R(x,y)\wedge S(y,z))\wedge T(z,w)\bigr), $$
$$ (T\circ S)\circ R=\{x,w\mid\Psi\},\quad\Psi:=\exists y\,\bigl(R(x,y)\wedge\exists z\,(S(y,z)\wedge T(z,w))\bigr) $$
となる。thm-reglog-soundness（公理のない理論に当てる）により、$\Phi\vdash_{x,w}\Psi$ と $\Psi\vdash_{x,w}\Phi$ が導けることを示せばよい。
$\Phi\vdash_{x,w}\Psi$ を導く。存在規則により、$\exists y\,(R\wedge S)\wedge T\vdash_{x,w,z}\Psi$ を導けばよい（ここで $R=R(x,y)$ などと略す）。Frobenius 規則と $\wedge$ の可換性から $\exists y\,(R\wedge S)\wedge T\vdash_{x,w,z}\exists y\,(R\wedge S\wedge T)$ なので、切断と存在規則により $R\wedge S\wedge T\vdash_{x,w,z,y}\Psi$ を導けばよい。$S\wedge T\vdash_{y,w,z}\exists z\,(S\wedge T)$ を文脈 $x,w,z,y$ へ広げ、連言の規則と合わせて $R\wedge S\wedge T\vdash_{x,w,z,y}R\wedge\exists z\,(S\wedge T)$ を得る。また $R\wedge\exists z\,(S\wedge T)\vdash_{x,w,y}\Psi$（$\chi\vdash\exists y\,\chi$ の形）を文脈 $x,w,z,y$ へ広げ、切断すればよい。$\Psi\vdash_{x,w}\Phi$ も、$x$ 側と $w$ 側の役割を入れ替えて同じ手順で導ける。$\square$

項の値は成分ごとに計算される（$t^M(\vec a)=(t^{M_i}(\vec a_i))_i$）ことが帰納法で分かる。論理式の構成に関する帰納法で主張を示す（ex-reglog-set により解釈は通常の充足である）。関係記号の段は $MR$ の定義、等号の段は「組が等しいことと全成分が等しいことは同値」であること、$\top$ と $\wedge$ の段は明らかである。$\exists y\,\varphi$ の段：$(\vec a,b)\in\{\vec x,y\mid\varphi\}_M$ となる $b=(b_i)_i$ があれば、帰納法の仮定により各 $i$ で $(\vec a_i,b_i)\in\{\vec x,y\mid\varphi\}_{M_i}$ である。逆に各 $i$ でそのような $b_i\in M_iB$ が存在するなら、選択公理によって各 $i$ に一つずつ選んで $b=(b_i)_i$ とすれば、帰納法の仮定により $(\vec a,b)\in\{\vec x,y\mid\varphi\}_M$ である。
後半：各 $M_i$ がモデルで $\vec a\in\{\vec x\mid\varphi\}_M$ なら、前半により各 $\vec a_i$ は $\varphi$ を満たし、したがって $\psi$ を満たすので、前半により $\vec a\in\{\vec x\mid\psi\}_M$ である。$\square$