健全性定理

同義語：soundness theorem

概要

前提知識: 一階論理の証明体系, Hilbert流の証明体系, 一階述語論理

論理で「$\Gamma$ から $\varphi$ が出る」には 2 つの意味がある。1 つは意味による帰結 $\Gamma\models\varphi$ で、$\Gamma$ を真にするどの解釈でも $\varphi$ が真になることをいう。もう 1 つは証明体系での導出可能性 $\Gamma\vdash\varphi$ で、公理と $\Gamma$ の元から推論規則を有限回使って $\varphi$ に達する記号列の並びがあることをいう。2 つは別々に定義されるので、結びつきは定理として示さなければならない。
健全性定理（soundness theorem）は、命題論理や一階述語論理の標準的な証明体系について、その一方の向き
$$ \Gamma\vdash\varphi\ \Longrightarrow\ \Gamma\models\varphi $$
を述べる定理である。導出できるものは意味の上でも正しい、すなわち証明体系は誤った結論を出さないことを保証する。証明の骨組みはどの体系でも同じで、「公理はどの解釈でも真」「推論規則は、前提が真になる解釈では結論も真にする」の 2 つを確かめ、導出の長さに関する帰納法でつなぐ。逆向きは完全性定理であり、命題論理では完全性定理(命題論理)、一階述語論理では Gödelの完全性定理である。
健全性定理の大きな使い道の 1 つは、導出できないこと の証明である。導出の候補は無限にあって調べ尽くせないが、健全性の対偶により、前提を真にして結論を偽にする解釈を 1 つ見つければ、導出がないことが分かる。この記事では、健全性を一般の「解釈の族」について定式化して判定法を示し、それを命題論理の Hilbert 流の体系 $\mathbf H_0$ と一階述語論理の体系 $\mathbf H$ に当てて健全性定理を証明する。帰結として無矛盾性と非導出性の判定を導き、一般化規則を加えた体系で「どの意味の帰結について健全か」が変わることを調べる。

定義

証明体系・導出・$\Gamma\vdash\varphi$ は一階論理の証明体系の記事の定義「証明体系・導出・証明可能性」による。すなわち証明体系は論理公理の集合 $\Lambda$ と有限個の推論規則の組であり、$\Gamma$ からの導出は、各行が論理公理か $\Gamma$ の元か、前の行から推論規則で得られる論理式の有限列である。
意味の側は、論理の種類ごとに「解釈」の範囲が違う。そこで、それらをまとめて扱うために次の形で定める。

解釈の族と帰結

論理式の全体を $F$ とする。集合 $E$ と、各 $e\in E$ に対する部分集合 $T_e\subset F$ の組 $(T_e)_{e\in E}$ を 解釈の族 という。$\varphi\in T_e$ を「$\varphi$ は $e$ で真」と読む。

$\Gamma\subset F$、$\varphi\in F$ について、$\Gamma\subset T_e$ となるすべての $e\in E$ で $\varphi\in T_e$ となるとき、$\Gamma\models_E\varphi$ と書き、$\varphi$ は $\Gamma$ の（$E$ についての）帰結であるという。
すべての $e\in E$ で $\varphi\in T_e$ となる $\varphi$、すなわち $\emptyset\models_E\varphi$ となる $\varphi$ を $E$ で妥当 であるという。

この記事で使う解釈の族は次の 4 つである。

名前	$E$ の元	$\varphi$ が $e$ で真	$\models_E$
(P) 命題論理	付値 $v$	$v(\varphi)=\mathrm T$	命題論理の論理的帰結。妥当＝恒真式
(A) 割り当てごと	構造と割り当ての組 $(\mathcal M,s)$	$\mathcal M\models\varphi[s]$	一階論理の証明体系の定義「論理的帰結と妥当性（論理式の場合）」
(S) 構造ごと	構造 $\mathcal M$	すべての割り当て $s$ で $\mathcal M\models\varphi[s]$	下の prop-soundness-gen-rule で使う
(K) Kripke	Kripke モデルと世界の組 $(\mathcal K,w)$	$\mathcal K,w\Vdash\varphi$	Kripke意味論の定義「妥当性と帰結」

(A) と (S) は、前提と結論がすべて文なら一致する。文の真偽は割り当てによらないからである（一階述語論理の系「文の真偽は割り当てによらない」）。自由変数をもつ論理式では、(A) の帰結のほうが強い条件である。

健全性

証明体系が解釈の族 $E$ について健全であるとは、すべての $\Gamma\subset F$、$\varphi\in F$ について、$\Gamma\vdash\varphi$ ならば $\Gamma\models_E\varphi$ であることをいう。$\Gamma=\emptyset$ の場合だけ、すなわち「定理はすべて $E$ で妥当」を 弱い健全性 といい、これと区別するとき前者を 強い健全性 という。

強い健全性は弱い健全性を含む。逆向きは一般には成り立たない。後の prop-soundness-gen-rule の体系 $\mathbf H^+$ は (A) について弱い健全性をもつが、強い健全性をもたない。

健全性の判定法

証明体系と解釈の族 $(T_e)_{e\in E}$ について、次の 2 つを仮定する。

（公理の妥当性）すべての $e\in E$ について $\Lambda\subset T_e$。
（規則の真理保存）各推論規則の各実例（前提 $\psi_1,\dots,\psi_k$、結論 $\chi$）と各 $e\in E$ について、$\psi_1,\dots,\psi_k\in T_e$ ならば $\chi\in T_e$。
このとき証明体系は $E$ について健全である。

導出の長さに関する帰納法

$\Gamma\vdash\varphi$ とし、$\Gamma$ からの導出 $\varphi_1,\dots,\varphi_n=\varphi$ をとる。$e\in E$ を $\Gamma\subset T_e$ となるように任意にとり、すべての $i$ について $\varphi_i\in T_e$ であることを $i$ に関する帰納法で示す。$j< i$ では $\varphi_j\in T_e$ と仮定する。

$\varphi_i\in\Lambda$ なら、1 により $\varphi_i\in T_e$ である。
$\varphi_i\in\Gamma$ なら、$e$ の選び方から $\varphi_i\in T_e$ である。
$\varphi_i$ が前の行 $\varphi_{j_1},\dots,\varphi_{j_k}$（$j_1,\dots,j_k< i$）から推論規則で得られたなら、帰納法の仮定によりそれらは $T_e$ に属し、2 により $\varphi_i\in T_e$ である。
導出の定義により場合はこれで尽きる。$i=n$ として $\varphi\in T_e$ であり、$e$ は任意だったので $\Gamma\models_E\varphi$ である。$\square$

この判定法は、形式体系の命題「定理の全体は規則で閉じた最小の集合」を、$\Lambda\cup\Gamma$ を含み規則で閉じた集合 $T_e$ に当てたものとも読める。条件 2 は「各 $e$ ごとに」真理を保つことを要求しており、「妥当な論理式から妥当な論理式を導く」という弱い条件では足りない。この違いが prop-soundness-gen-rule で表に出る。

命題論理の健全性定理

命題論理の論理式は命題変数から $\lnot,\to$ で作り、体系 $\mathbf H_0$ は公理図式

(A1) $\varphi\to(\psi\to\varphi)$
(A2) $(\varphi\to(\psi\to\chi))\to((\varphi\to\psi)\to(\varphi\to\chi))$
(A3) $(\lnot\psi\to\lnot\varphi)\to((\lnot\psi\to\varphi)\to\psi)$
のすべての実例を公理とし、前件肯定（MP：$\psi$ と $\psi\to\chi$ から $\chi$）だけを推論規則とする（Hilbert流の証明体系の定義「体系 H₀ と H₀′」）。付値と真理値は命題論理の定義「付値と真理値」による。とくに $v(\alpha\to\beta)=\mathrm F$ となるのは $v(\alpha)=\mathrm T$ かつ $v(\beta)=\mathrm F$ のときに限る。

命題論理の健全性定理

論理式の集合 $\Gamma$ と論理式 $\varphi$ について、$\Gamma\vdash_{\mathbf H_0}\varphi$ ならば、$\Gamma$ のすべての元を真にする付値はすべて $\varphi$ を真にする。とくに、$\mathbf H_0$ の定理はすべて恒真式である。

公理は恒真式で、MP は真理を保つ

解釈の族 (P) について lem-soundness-criterion の 2 条件を確かめる。付値 $v$ を任意に固定し、$\alpha,\beta,\gamma$ を任意の論理式とする。
公理。 各公理図式の実例が $v$ で偽になると仮定して矛盾を導く。

(A1)：$v(\alpha\to(\beta\to\alpha))=\mathrm F$ なら $v(\alpha)=\mathrm T$ かつ $v(\beta\to\alpha)=\mathrm F$ であり、後者から $v(\alpha)=\mathrm F$ となって矛盾する。
(A2)：全体が偽なら $v(\alpha\to(\beta\to\gamma))=\mathrm T$、$v(\alpha\to\beta)=\mathrm T$、$v(\alpha\to\gamma)=\mathrm F$、したがって $v(\alpha)=\mathrm T$、$v(\gamma)=\mathrm F$ である。$v(\alpha)=\mathrm T$ と $v(\alpha\to\beta)=\mathrm T$ から $v(\beta)=\mathrm T$、$v(\alpha)=\mathrm T$ と $v(\alpha\to(\beta\to\gamma))=\mathrm T$ から $v(\beta\to\gamma)=\mathrm T$ であり、$v(\gamma)=\mathrm T$ となって矛盾する。
(A3)：全体が偽なら $v(\lnot\beta\to\lnot\alpha)=v(\lnot\beta\to\alpha)=\mathrm T$ かつ $v(\beta)=\mathrm F$ である。$v(\lnot\beta)=\mathrm T$ なので $v(\lnot\alpha)=\mathrm T$ かつ $v(\alpha)=\mathrm T$ となって矛盾する。

MP。 $v(\psi)=v(\psi\to\chi)=\mathrm T$ で $v(\chi)=\mathrm F$ なら $v(\psi\to\chi)=\mathrm F$ となるので、$v(\chi)=\mathrm T$ である。
lem-soundness-criterion により $\mathbf H_0$ は (P) について健全である。$\Gamma=\emptyset$ とすると、定理はすべての付値で真、すなわち恒真式である。$\square$

公理の確認は、各公理図式の文字 $\alpha,\beta,\gamma$ の真理値だけを使うので、無限に多い実例に一様に通用する。(A3) の代わりに (A3′) $(\lnot\varphi\to\lnot\psi)\to(\psi\to\varphi)$ を置いた体系 $\mathbf H_0'$ でも、(A3′) が偽になるには $v(\psi)=\mathrm T$、$v(\varphi)=\mathrm F$ が要り、そのとき $v(\lnot\varphi\to\lnot\psi)=\mathrm F$ なので、同じく健全である。定理は Bil03 Theorem 4.1（p. 15）、OLT26 Theorem 12.30（p. 185）にある（体系は文献ごとに違う）。

一階論理の健全性定理

一階言語の論理式・代入・代入可能性は論理式、構造・割り当て $s$・$s_x^a$・充足関係 $\mathcal M\models\varphi[s]$ は一階述語論理の記事による。体系 $\mathbf H$ は一階論理の証明体系の定義「体系 H」のもので、結合子は $\lnot,\to$、量化記号は $\forall$、等号を論理記号とし、論理公理 $\Lambda$ は次の公理図式の実例の全称化（$\forall x_1\cdots\forall x_n\,\theta$、$n\ge0$）の全体、推論規則は MP だけである。

(A1)〜(A3) 上と同じ形（$\alpha,\beta,\gamma$ は一階の論理式）
(A4) $\forall x\,\alpha\to\alpha[t/x]$（$t$ は $\alpha$ の $x$ に代入可能）
(A5) $\forall x\,(\alpha\to\beta)\to(\forall x\,\alpha\to\forall x\,\beta)$
(A6) $\alpha\to\forall x\,\alpha$（$x\notin\operatorname{FV}(\alpha)$）
(A7) $x=x$
(A8) $x=y\to(\alpha\to\beta)$（$\alpha$ は原子論理式で、$\beta$ は $\alpha$ の中の $x$ の出現のいくつかを $y$ に置き換えたもの）

論理公理は妥当である

体系 $\mathbf H$ の論理公理はすべて、解釈の族 (A) で妥当である。すなわち、すべての構造 $\mathcal M$ と割り当て $s$ について $\mathcal M\models\lambda[s]$（$\lambda\in\Lambda$）である。

公理図式ごとに充足の定義を確かめる

$\mathcal M$ と $s$ を任意にとり、各公理図式の実例が $s$ のもとで真であることを示す。「真」は $\mathcal M$、$s$ のもとで真であることをいう。
(A1)〜(A3)：$\lnot,\to$ の充足条件は真理値表と同じなので、thm-soundness-propositional の証明の公理の段落がそのまま通る。
(A4)：$\forall x\,\alpha$ が真とし、$b:=t^{\mathcal M}[s]$ とおく。充足の定義から $\mathcal M\models\alpha[s_x^b]$ であり、$t$ は $\alpha$ の $x$ に代入可能なので、一階述語論理の補題「代入補題」の 2 により $\mathcal M\models\alpha[t/x][s]$ である。
(A5)：$\forall x\,(\alpha\to\beta)$ と $\forall x\,\alpha$ が真なら、各 $a\in M$ について $\alpha\to\beta$ と $\alpha$ が $s_x^a$ のもとで真なので、$\beta$ も真である。よって $\forall x\,\beta$ は真である。
(A6)：$\alpha$ が真とする。$x\notin\operatorname{FV}(\alpha)$ なので、各 $a\in M$ について $s$ と $s_x^a$ は $\operatorname{FV}(\alpha)$ の上で一致し、一階述語論理の補題「一致補題」により $\alpha$ は $s_x^a$ のもとでも真である。よって $\forall x\,\alpha$ は真である。
(A7)：$x^{\mathcal M}[s]=x^{\mathcal M}[s]$ なので真である。
(A8)：$s(x)=s(y)$ とする。項 $u$ の中の $x$ の出現のいくつかを $y$ に置き換えた項 $u'$ について $u'^{\mathcal M}[s]=u^{\mathcal M}[s]$ であることを、項の組み立てに関する帰納法で示す。$u$ が $x$ なら $u'$ は $x$ か $y$ で、値はどちらも $s(x)$ である。$u$ がほかの変数か定数記号なら $u'=u$ である。$u=f(u_1,\dots,u_n)$ なら $u'=f(u_1',\dots,u_n')$ で、帰納法の仮定から値は等しい。原子論理式 $\alpha$ は $u_1=u_2$ か $R(u_1,\dots,u_n)$ の形で、$\beta$ はそれぞれ $u_1'=u_2'$、$R(u_1',\dots,u_n')$ なので、各項の値が変わらず、$\alpha$ が真なら $\beta$ も真である。
全称化：$\theta$ が妥当なら、任意の $\mathcal M$、$s$、$a\in M$ について $\theta$ は $s_x^a$ のもとで真なので、$\forall x\,\theta$ も妥当である。公理図式の実例は妥当なので、その全称化も、付ける $\forall$ の個数に関する帰納法で妥当である。$\square$

一階論理の健全性定理

体系 $\mathbf H$ で $\Gamma\vdash\varphi$ ならば、すべての構造 $\mathcal M$ と割り当て $s$ について、$\Gamma$ のすべての元が $\mathcal M$、$s$ のもとで真なら $\varphi$ も真である（一階論理の証明体系の定義「論理的帰結と妥当性（論理式の場合）」の意味で $\Gamma\models\varphi$）。とくに $\mathbf H$ の定理はすべて妥当であり、文の集合 $\Gamma$ と文 $\varphi$ について、$\Gamma\vdash\varphi$ なら $\Gamma$ のどのモデルでも $\varphi$ は真である。

判定法に当てる

解釈の族 (A) について lem-soundness-criterion の 2 条件を確かめる。1 は lem-soundness-axioms-valid である。2：$\mathbf H$ の規則は MP だけで、$\mathcal M\models\psi[s]$ かつ $\mathcal M\models(\psi\to\chi)[s]$ なら、$\to$ の充足条件から $\mathcal M\models\chi[s]$ である。よって $\mathbf H$ は (A) について健全である。最後の主張は、文の真偽が割り当てによらないことから従う。$\square$

文についての形は Bil03 Theorem 8.1（p. 47）にある（同書は証明を演習としている）。OLT26 Theorem 22.36（p. 346）は、量化記号の推論規則をもつ別の Hilbert 流の体系について、文の帰結に対する健全性を述べている。

帰結

論理式の集合 $\Gamma$ が 矛盾する とは、ある $\varphi$ について $\Gamma\vdash\varphi$ かつ $\Gamma\vdash\lnot\varphi$ となることをいい、そうでないとき 無矛盾 という（無矛盾性）。

充足可能な集合の無矛盾性

$\Gamma$ のすべての元を真にする付値があれば、$\Gamma$ は $\mathbf H_0$ で無矛盾である。
$\Gamma$ のすべての元を真にする構造 $\mathcal M$ と割り当て $s$ があれば、$\Gamma$ は $\mathbf H$ で無矛盾である。
とくに $\emptyset$ はどちらの体系でも無矛盾であり、$\vdash\varphi$ と $\vdash\lnot\varphi$ がともに成り立つ $\varphi$ はない。

2 を示す（1 も同じ）。$\Gamma\vdash\varphi$ かつ $\Gamma\vdash\lnot\varphi$ とすると、thm-soundness-first-order により $\mathcal M\models\varphi[s]$ かつ $\mathcal M\models\lnot\varphi[s]$ となり、$\lnot$ の充足条件に反する。$\emptyset$ については、すべての命題変数を真にする付値と、台集合 $\{0\}$ の構造と割り当てをとればよい。$\square$

2 は無矛盾性の定理「モデルをもてば無矛盾」と同じ内容で、命題論理の 1 は Bil03 Proposition 4.2（p. 15）にある。

導出できない論理式

$\{q,\ p\to q\}\vdash_{\mathbf H_0}p$ ではない。$v(p)=\mathrm F$、$v(q)=\mathrm T$ の付値は前提を真にし、$p$ を偽にする。
$P$ を 1 項関係記号とする。$\vdash_{\mathbf H}\exists x\,P(x)\to\forall x\,P(x)$ ではない。台集合 $\{0,1\}$ で $P$ を $\{0\}$ と解釈すると、前件は真で後件は偽である。
$\{P(x)\}\vdash_{\mathbf H}\forall x\,P(x)$ ではない。2 の構造と $s(x)=0$ をとると、$P(x)$ は真で $\forall x\,P(x)$ は偽である。

3 は、一階論理の証明体系の定理「汎化定理」の条件「$x$ が $\Gamma$ の元に自由に現れない」が外せないことを示している。

Peirce の法則と直観主義論理

Peirce の法則 $((p\to q)\to p)\to p$ は恒真式である（$v(p)=\mathrm T$ なら後件が真、$v(p)=\mathrm F$ なら $v(p\to q)=\mathrm T$ から前件が偽）。完全性定理(命題論理) により $\vdash_{\mathbf H_0}((p\to q)\to p)\to p$ である。
一方、直観主義論理の公理系 $\vdash_{\mathrm I}$ では導出できない。Kripke意味論の定理「Kripke 意味論の健全性」は、$\vdash_{\mathrm I}$ が解釈の族 (K) について健全であることを述べている。世界 $w_0\le w_1$ の 2 点からなるモデルで $V(p)=\{w_1\}$、$V(q)=\emptyset$ とする。$w_1\Vdash p$、$w_1\not\Vdash q$ なので、$w_0$ でも $w_1$ でも $p\to q$ は強制されない。したがって $(p\to q)\to p$ は両方の世界で強制される（強制すべき場合がない）が、$w_0\not\Vdash p$ なので $w_0\not\Vdash((p\to q)\to p)\to p$ である。健全性により、Peirce の法則は $\vdash_{\mathrm I}$ の定理でない。

この例のように、健全性は「どの解釈の族について健全か」を変えることで、2 つの証明体系の違いを示す道具にもなる。

一般化規則と 2 つの帰結

$\mathbf H$ では「$x$ について一般化してよい」という推論を規則として置かず、論理公理を全称化で閉じている。規則として置くと、健全性が成り立つ帰結の意味が変わる。

一般化規則を加えた体系の健全性

$\mathbf H$ に 一般化規則「$\psi$ から $\forall x\,\psi$ を導く」（$x$ は任意の変数）を加えた体系を $\mathbf H^+$ とする。

$\mathbf H^+$ は解釈の族 (S) について健全である。すなわち $\Gamma\vdash_{\mathbf H^+}\varphi$ なら、$\Gamma$ のすべての元がすべての割り当てで真になる構造 $\mathcal M$ では、$\varphi$ もすべての割り当てで真である。とくに $\mathbf H^+$ の定理はすべて妥当である。
$\mathbf H^+$ は解釈の族 (A) について健全でない。

判定法の条件 2 を構造ごとに確かめる

1：(S) について lem-soundness-criterion の 2 条件を確かめる。論理公理は lem-soundness-axioms-valid によりどの構造でもすべての割り当てで真である。MP：$\psi$ と $\psi\to\chi$ が $\mathcal M$ のすべての割り当てで真なら、各割り当てで $\chi$ も真である。一般化規則：$\psi$ が $\mathcal M$ のすべての割り当てで真とする。任意の $s$ と $a\in M$ について $s_x^a$ も割り当てなので $\mathcal M\models\psi[s_x^a]$ であり、$\mathcal M\models\forall x\,\psi[s]$ である。よって $\mathbf H^+$ は (S) について健全である。$\Gamma=\emptyset$ なら、定理はすべての構造ですべての割り当てで真、すなわち妥当である。
2：2 行の列 $P(x),\ \forall x\,P(x)$ は $\{P(x)\}$ からの $\mathbf H^+$ の導出である。ex-soundness-underivable の 3 の $\mathcal M$、$s$ は $P(x)$ を真にし $\forall x\,P(x)$ を偽にするので、$\{P(x)\}\models\forall x\,P(x)$ は (A) の意味で成り立たない。$\square$

2 で lem-soundness-criterion が使えないのは、一般化規則が「$\mathcal M$、$s$ で $\psi$ が真なら $\forall x\,\psi$ も真」という割り当てごとの真理保存を満たさないからである。$\Gamma$ と $\varphi$ がすべて文なら (A) と (S) の帰結は一致するので、文だけを扱う限り $\mathbf H$ と $\mathbf H^+$ の違いは表に出ない。$\mathbf H^+$ で演繹定理に変数の制限が要ることは、一階論理の証明体系の例「反例：一般化を推論規則にした場合」にある。

条件を外した反例

lem-soundness-criterion の 2 条件と、$\mathbf H$ の公理図式に付いた条件は、どれも外すと健全性が崩れる。各行は 1 つの条件だけを外している。

外す条件	反例	成り立たなくなること
公理が恒真式（命題論理）	$\mathbf H_0$ に公理図式 $(\varphi\to\psi)\to(\psi\to\varphi)$ を加えた体系	(P) についての弱い健全性
推論規則が付値ごとに真理を保つ	$\mathbf H_0$ に後件肯定「$\psi$ と $\varphi\to\psi$ から $\varphi$」を加えた体系	(P) についての健全性
(A4) の $t$ が代入可能	$\forall x\,\exists y\,\lnot(x=y)\to\exists y\,\lnot(y=y)$ を公理に加える	(A) についての弱い健全性
推論規則が割り当てごとに真理を保つ	$\mathbf H^+$（一般化規則を加えた体系）	(A) についての健全性（(S) については健全）

反例の確かめ

表の各行を確かめる。

各行の確かめを開く

$(p\to q)\to(q\to p)$ は 1 行で導出できる定理だが、$v(p)=\mathrm F$、$v(q)=\mathrm T$ で $v(p\to q)=\mathrm T$、$v(q\to p)=\mathrm F$ となり、恒真式でない。
前提 $q$、$p\to q$ から 1 回で $p$ が導出できるが、ex-soundness-underivable の 1 の付値により $\{q,\ p\to q\}\models p$ は成り立たない。
$y$ は $\exists y\,\lnot(x=y)$ の $x$ に代入可能でない。台集合 $\{0,1\}$ の構造では、どの元にも異なる元があるので前件は真、$\exists y\,\lnot(y=y)$ は偽で、この論理式はどの割り当てでも偽である。1 行の導出があるので定理だが妥当でない。
prop-soundness-gen-rule の 2 による。

(A6)・(A8) の条件を外した場合も同じく妥当でない論理式が定理になる（一階論理の証明体系の例「反例：公理図式の条件を外す」）。

完全性定理との関係

健全性の逆、すなわち $\Gamma\models\varphi$ なら $\Gamma\vdash\varphi$ を 完全性 という。$\mathbf H_0$ は完全であり（完全性定理(命題論理)）、$\mathbf H$ は文の帰結について完全である（Gödelの完全性定理）。健全性と合わせると、命題論理では $\vdash_{\mathbf H_0}$ と恒真式による帰結が、一階述語論理では文の間の $\vdash_{\mathbf H}$ と $\models$ が一致する。
2 つの向きの重さは違う。健全性は、公理と規則を 1 つずつ確かめて導出の長さで帰納するだけで済む。完全性は、「導出できない」という否定の情報から「偽にする解釈がある」という存在を引き出す必要があり、極大無矛盾集合などの構成を要する。健全性は完全性を含まない。公理も規則もない体系では、$\Gamma\vdash\varphi$ となるのは $\varphi\in\Gamma$ のときだけなので健全だが、恒真式 $p\to p$ を導出できない。

ほかの証明体系の健全性

流儀の違う証明体系でも、健全性の証明は lem-soundness-criterion と同じ形をとる（導出が列でなく木なら、木の高さに関する帰納法になる）。

自然演繹：仮定を外す規則が帰結を保つことを確かめる（自然演繹の定理「自然演繹の健全性」）。
シーケント計算：シーケントの妥当性を定め、各規則が妥当性を保つことを確かめる。量化記号の規則では固有変数の条件が要る（シーケント計算の定理「LK の健全性」）。
直観主義論理：解釈を Heyting 代数での値や Kripke モデルの世界にとる（直観主義論理の定理「Heyting 代数に関する健全性」、Kripke意味論の定理「Kripke 意味論の健全性」）。
様相論理：公理系と Kripke フレームの性質の組ごとに健全性を示す（様相論理）。
健全かつ完全な 2 つの体系では、証明可能性がどちらも同じ意味の帰結に一致するので、体系の見た目によらず同じ式が導出できる（一階論理の証明体系の節「流儀の比較」）。ただし一階述語論理では完全性が文についての主張なので、これは文に限る。$\mathbf H$ と $\mathbf H^+$ は $\{P(x)\}$ から導出できる式が違う（prop-soundness-gen-rule）。