Hilbert流の証明体系

同義語：ヒルベルト流の証明体系Hilbert型の証明体系公理的証明体系Hilbert-style proof systemHilbert systemaxiomatic derivation

概要

前提知識: 命題論理, 一階論理の証明体系

証明体系には、公理をたくさん用意して推論規則をほとんど前件肯定（modus ponens）だけにする作り方がある。これを Hilbert 流の証明体系（公理的な証明体系）という。規則が 1 つしかないので、「導出の長さに関する帰納法」で体系そのものについての定理を示すのが易しい。その代わり、個々の導出は長くなり、見つけるのも難しい。たとえば、$\lnot$ と $\to$ だけを使う命題論理の典型的な体系は、次の 3 つの公理図式と前件肯定だけからなる。
$$ \varphi\to(\psi\to\varphi),\qquad(\varphi\to(\psi\to\chi))\to((\varphi\to\psi)\to(\varphi\to\chi)),\qquad(\lnot\psi\to\lnot\varphi)\to((\lnot\psi\to\varphi)\to\psi). $$
これだけで、真理値表で確かめられる恒真式がすべて導出できる。
公理の選び方は 1 通りではなく、文献ごとに違う。基本の結合子を増やして公理を十数個にする体系もあれば、3 つ目の公理を別の形にする体系もある。そこで、「違う公理系が同じ論理を与えるのはいつか」「3 つの公理のうちどれかは他から導けて不要ではないか」が問題になる。本記事では、命題論理の Hilbert 流の体系を 1 つ固定し、3 つ目の公理を取り替えた体系と同じ式を導出すること、および 3 つの公理がどれも他の 2 つから導出できないこと（公理の独立性）を証明する。一階述語論理の Hilbert 流の体系と、その演繹定理・健全性定理は一階論理の証明体系の記事が扱っている。

定義

論理式

命題論理の論理式・付値・恒真式は命題論理の記事の定義「論理式」「付値と真理値」「恒真式・充足可能性・論理的帰結」による。ただし本記事では、命題変数から $\lnot$ と $\to$ だけで作った論理式を扱い、$\land,\lor$ は略記とする。
$$ \varphi\land\psi:=\lnot(\varphi\to\lnot\psi),\qquad\varphi\lor\psi:=(\lnot\varphi\to\psi). $$
どちらも命題論理の記事の $\land,\lor$ と同じ真理値をとる。外側の括弧は省き、$\to$ は右から結合させる（$\varphi\to\psi\to\chi$ は $\varphi\to(\psi\to\chi)$）ことがある。

Hilbert 流の証明体系

公理図式 とは、$\varphi\to(\psi\to\varphi)$ のように、論理式を表す文字 $\varphi,\psi,\chi$ を含む式の形のことで、文字に任意の論理式を（同じ文字には同じ論理式を）入れた論理式をその実例という。1 つの公理図式は無限に多くの論理式を表す。

Hilbert 流の証明体系

命題論理の Hilbert 流の証明体系 とは、有限個の公理図式と、有限個の推論規則の組である。推論規則は前件肯定（MP：$\psi$ と $\psi\to\chi$ から $\chi$ を導く）だけとすることが多い。公理図式の実例を公理という。
論理式の集合 $\Gamma$ からの導出とは、論理式の有限列 $\varphi_1,\dots,\varphi_n$ で、各 $\varphi_i$ が公理であるか、$\Gamma$ の元であるか、それ以前の行から推論規則で得られるものをいう。最後の行が $\varphi$ である導出があるとき $\Gamma\vdash\varphi$ と書き、$\emptyset\vdash\varphi$ を $\vdash\varphi$ と書いて $\varphi$ をその体系の定理という。体系の名前を添えて $\vdash_{S}$ とも書く。

これは一階論理の証明体系の記事の定義「証明体系・導出・証明可能性」の特別な場合である。同記事の命題「導出可能性の基本性質」（反射性・単調性・有限性・推移性）は、導出が前の行だけを参照する有限列であることだけから証明されているので、本記事の体系でもそのまま成り立つ。以下、とくに推移性「$\Delta$ のすべての元が $\Gamma$ から導出でき、$\Delta\vdash\psi$ なら $\Gamma\vdash\psi$」を、導出をつなぐときに断らずに使う。

体系 $\mathbf H_0$ と $\mathbf H_0'$

体系 H₀ と H₀′

次の公理図式を考える。

(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)$
(A3′) $(\lnot\varphi\to\lnot\psi)\to(\psi\to\varphi)$
(A1)・(A2)・(A3) と MP からなる体系を $\mathbf H_0$、(A1)・(A2)・(A3′) と MP からなる体系を $\mathbf H_0'$ とする。

$\mathbf H_0$ は一階論理の証明体系の記事の体系 $\mathbf H$ の、命題論理の部分（同記事の (A1)〜(A3) と MP）である。これは Bil03 の命題論理の体系と同じである（Definition 3.1〜3.3、pp. 11–12）。(A3′) は対偶の形の公理で、$\mathbf H_0$ ではその実例が定理になる（Bil03 Problem 3.9 の (3)、p. 14。thm-hilbert-style-proof-system-equivalence の証明で確かめる）。
Hilbert 流の体系にはほかにも多くの流儀がある。代表的なものを並べる。

	$\mathbf H_0$	$\mathbf H_0'$	OLT26 の体系	直観主義論理の記事の体系	一階論理の証明体系の記事の $\mathbf H$
基本の記号	$\lnot,\to$	$\lnot,\to$	$\lnot,\land,\lor,\to,\top,\bot$	$\land,\lor,\to,\bot$	$\lnot,\to,\forall,=$
公理図式の数	3	3	14	9	8（全称化で閉じる）
推論規則	MP	MP	MP	MP	MP
定理全体と一致するもの	恒真式	恒真式	恒真式	恒真式の一部（排中律を含まない）	妥当な文（文に限る）

OLT26 の体系は Definition 12.5〜12.6（p. 178）で、$\land,\lor$ の導入・除去にあたる公理を結合子ごとに置く。同書はこの体系の健全性と完全性を Theorem 12.30（p. 185）と Corollary 13.7（p. 192）で示している。直観主義論理の記事の体系は、排中律 $\varphi\lor\lnot\varphi$ を公理に加えると古典論理になり（同記事の定義「直観主義命題論理の公理系」の後の段落）、加えなければ $p\lor\lnot p$ は定理にならない（同記事の系「直観主義論理で証明できない式」）。表の最後の行のうち、恒真式や妥当な文がすべて定理になることは各体系の完全性であり、本記事では $\mathbf H_0$ についても証明しない（rem-hilbert-style-proof-system-completeness）。$\mathbf H_0'$ の行は thm-hilbert-style-proof-system-equivalence により $\mathbf H_0$ の行と同じになる。

直感

Hilbert 流の体系では、「仮定を置いて議論し、最後に仮定を外す」という普通の証明の動きが規則として存在しない。(A1)・(A2) はその代わりをするために選ばれた公理であり、これらと MP から「$\Gamma\cup\{\varphi\}\vdash\psi$ なら $\Gamma\vdash\varphi\to\psi$」（演繹定理）が導出の外側の定理として得られる。いったん演繹定理が手に入ると、導出を書き下さずに導出の存在を示せるようになる。一方、公理を 1 つ取り去ったり取り替えたりすると何が導出できなくなるかは、導出を全部調べ尽くすことができないので、別の道具が要る。そこで、真理値を 2 つ以外に増やした「偽の真理値表」を作り、その表では公理と MP は「真」を保つのに、ある式は「真」にならない、という状況を作る。これが公理の独立性の証明法である。

例と反例

導出の例

含意の推移

$\{\varphi\to\psi,\ \psi\to\chi\}\vdash_{\mathbf H_0}\varphi\to\chi$ である。次の列が導出である（Bil03 Example 3.2、p. 12 と同じ）。

$(\psi\to\chi)\to(\varphi\to(\psi\to\chi))$ ——(A1)
$\psi\to\chi$ ——前提
$\varphi\to(\psi\to\chi)$ ——1、2 から MP
$(\varphi\to(\psi\to\chi))\to((\varphi\to\psi)\to(\varphi\to\chi))$ ——(A2)
$(\varphi\to\psi)\to(\varphi\to\chi)$ ——3、4 から MP
$\varphi\to\psi$ ——前提
$\varphi\to\chi$ ——6、5 から MP

恒等式 $\vdash_{\mathbf H_0}\varphi\to\varphi$ の 5 行の導出は一階論理の証明体系の記事の補題「恒等式の導出」にある。その導出は (A1)・(A2) と MP しか使わないので、$\mathbf H_0'$ でも同じ導出が通る。
体系 $\mathbf H_0$ と $\mathbf H_0'$ では 演繹定理「$\Gamma\cup\{\varphi\}\vdash\psi\iff\Gamma\vdash\varphi\to\psi$」が成り立つ。一階論理の証明体系の記事の定理「演繹定理」の証明は、推論規則が MP だけであることと、(A1)・(A2) の実例と恒等式の導出しか使わないので、$\mathbf H_0$ と $\mathbf H_0'$ でもそのまま通る（$\mathbf H_0$ については Bil03 Theorem 3.8、p. 13）。以下、演繹定理を断らずに使う。

二重否定の除去

$\vdash_{\mathbf H_0}\lnot\lnot\varphi\to\varphi$ である。演繹定理により $\{\lnot\lnot\varphi\}\vdash\varphi$ を示せばよい。

$\lnot\lnot\varphi$ ——前提
$\lnot\lnot\varphi\to(\lnot\varphi\to\lnot\lnot\varphi)$ ——(A1)
$\lnot\varphi\to\lnot\lnot\varphi$ ——1、2 から MP
$(\lnot\varphi\to\lnot\lnot\varphi)\to((\lnot\varphi\to\lnot\varphi)\to\varphi)$ ——(A3) の実例（$\psi$ を $\varphi$ に、$\varphi$ を $\lnot\varphi$ にした式）
$(\lnot\varphi\to\lnot\varphi)\to\varphi$ ——3、4 から MP
$\lnot\varphi\to\lnot\varphi$ ——恒等式
$\varphi$ ——6、5 から MP
6 行目は恒等式の 5 行の導出をその場に挿入したものと考える。Bil03 Example 3.4（p. 13）は同じ式を演繹定理を使わずに導出している。

条件を外した反例

体系の条件を 1 つ外すと何が崩れるかを表にまとめる。各行の確かめ方は ex-hilbert-style-proof-system-conditions にある。

外す条件	反例	成り立たなくなること
公理が図式である（すべての実例が公理）	(A1)〜(A3) の実例のうち、命題変数 $p,q,r$ だけで書いた 3 つの式だけを公理にする	恒真式 $s\to s$ の導出（完全性）
(A3) がある	(A1)・(A2) と MP だけの体系	恒真式 $\lnot\lnot p\to p$ の導出（完全性）
否定の公理として (A3) を置く	(A3) の代わりに二重否定除去 $\lnot\lnot\varphi\to\varphi$ を置く	恒真式 $p\to\lnot\lnot p$ の導出（完全性）
推論規則が真理を保つ	MP に後件肯定「$\psi$ と $\varphi\to\psi$ から $\varphi$」を加える	健全性

性質

健全性と完全性

$\mathbf H_0$ は健全かつ完全である。すなわち、論理式の集合 $\Gamma$ と論理式 $\varphi$ について、$\Gamma\vdash_{\mathbf H_0}\varphi$ であることと、$\Gamma$ のすべての元を真にする付値がすべて $\varphi$ を真にすること（$\Gamma\models\varphi$）は同値である（Bil03 Theorem 4.1・4.12、pp. 15–16）。健全性の向きは、(A1)〜(A3) がどれも恒真式であり、MP が「真」を保つことから、導出の長さに関する帰納法で従う。これは一階論理の証明体系の記事の定理「健全性定理」と同じ論法である（(A1)〜(A3) が恒真式であることは同記事の補題「論理公理は妥当である」の証明の最初の段落）。完全性の向きは本記事では証明しない。命題論理のシーケント計算についての完全性は命題論理の記事の定理「健全性と完全性」で証明されている。

健全性から、導出できないことを示すには、前提を真にして結論を偽にする付値を 1 つ見つければよい。たとえば $\{q,\ p\to q\}\vdash_{\mathbf H_0}p$ ではない。$p$ を偽、$q$ を真にする付値が前提を真にし、$p$ を偽にするからである。後の lem-hilbert-style-proof-system-matrix は、この論法を「真理値が 2 つとは限らない表」に広げたものである。

公理系の違い

2 つの体系が同値であるとは、すべての $\Gamma,\varphi$ について $\Gamma\vdash_{S}\varphi\iff\Gamma\vdash_{S'}\varphi$ であることをいう。そのためには、一方の公理（の実例）がすべて他方で定理になり、規則も他方で導出できれば十分である。導出の中の公理の行を、他方の体系でのその公理の導出で置き換えればよいからである（推移性）。
まず $\mathbf H_0'$ で「矛盾からは何でも出る」ことを確かめる。

矛盾からの導出

$\mathbf H_0'$ で、任意の論理式 $\varphi,\chi$ について $\{\lnot\varphi,\ \varphi\}\vdash_{\mathbf H_0'}\chi$ である。

(A1) と (A3′) を 1 回ずつ使う

要点：(A1) で $\lnot\chi\to\lnot\varphi$ を作り、(A3′) で $\varphi\to\chi$ に裏返して MP を使う。

7 行の導出を開く

次の列が $\{\lnot\varphi,\varphi\}$ からの導出である。

$\lnot\varphi$ ——前提
$\lnot\varphi\to(\lnot\chi\to\lnot\varphi)$ ——(A1)
$\lnot\chi\to\lnot\varphi$ ——1、2 から MP
$(\lnot\chi\to\lnot\varphi)\to(\varphi\to\chi)$ ——(A3′) の実例（$\varphi$ を $\chi$ に、$\psi$ を $\varphi$ にした式）
$\varphi\to\chi$ ——3、4 から MP
$\varphi$ ——前提
$\chi$ ——6、5 から MP $\square$

3 つ目の公理を取り替えても同値

体系 $\mathbf H_0$ と $\mathbf H_0'$ は同値である。とくに、同じ論理式を定理にもつ。

互いの 3 つ目の公理を導出する

2 つの体系は (A1)・(A2) と MP を共有するので、$\mathbf H_0$ で (A3′) の実例がすべて定理になり、$\mathbf H_0'$ で (A3) の実例がすべて定理になることを示せばよい。
$\mathbf H_0$ で (A3′)：$\vdash_{\mathbf H_0}(\lnot\varphi\to\lnot\psi)\to(\psi\to\varphi)$ を示す。演繹定理を 2 回使えば、$\Gamma:=\{\lnot\varphi\to\lnot\psi,\ \psi\}$ から $\varphi$ を導出すればよい。

$(\lnot\varphi\to\lnot\psi)\to((\lnot\varphi\to\psi)\to\varphi)$ ——(A3) の実例（$\psi$ を $\varphi$ に、$\varphi$ を $\psi$ にした式）
$\lnot\varphi\to\lnot\psi$ ——前提
$(\lnot\varphi\to\psi)\to\varphi$ ——2、1 から MP
$\psi\to(\lnot\varphi\to\psi)$ ——(A1)
$\psi$ ——前提
$\lnot\varphi\to\psi$ ——5、4 から MP
$\varphi$ ——6、3 から MP
$\mathbf H_0'$ で (A3)：$\vdash_{\mathbf H_0'}(\lnot\psi\to\lnot\varphi)\to((\lnot\psi\to\varphi)\to\psi)$ を示す。演繹定理を 2 回使えば、$\Delta:=\{\lnot\psi\to\lnot\varphi,\ \lnot\psi\to\varphi\}$ から $\psi$ を導出すればよい。$\tau:=\psi\to\psi$ とおく。

$\Delta\cup\{\lnot\psi\}$ からは、MP で $\lnot\varphi$ と $\varphi$ が導出できる。lem-hilbert-style-proof-system-explosion と推移性により、$\Delta\cup\{\lnot\psi\}\vdash_{\mathbf H_0'}\lnot\tau$ である。
演繹定理により $\Delta\vdash_{\mathbf H_0'}\lnot\psi\to\lnot\tau$ である。
(A3′) の実例 $(\lnot\psi\to\lnot\tau)\to(\tau\to\psi)$ と MP で、$\Delta\vdash_{\mathbf H_0'}\tau\to\psi$ である。
$\tau=\psi\to\psi$ は恒等式なので $\vdash_{\mathbf H_0'}\tau$ であり、MP で $\Delta\vdash_{\mathbf H_0'}\psi$ である。
以上で、どちらの体系も他方の公理をすべて定理にもつ。$\Gamma\vdash_{\mathbf H_0}\varphi$ の導出の中の (A3) の実例の行を、その $\mathbf H_0'$ での導出で置き換えれば $\Gamma\vdash_{\mathbf H_0'}\varphi$ の導出になり、逆も同様である。$\square$

(A3′) を使った $\mathbf H_0'$ の証明では、「$\lnot\psi$ を仮定すると矛盾する」ことから $\psi$ を得るのに、恒等式 $\tau$ を経由する工夫が要った。(A3) は「$\lnot\psi$ から $\lnot\varphi$ と $\varphi$ の両方が出るなら $\psi$」という背理法の形をしているので、この工夫は不要である。このように、同値な体系でも個々の式の導出の長さや手間は違う。上の証明は、完全性（rem-hilbert-style-proof-system-completeness）を使わず、導出を直接つないで同値性を示している。完全性を使うなら、$\mathbf H_0'$ の公理 (A3′) が恒真式であることから $\mathbf H_0'$ の定理は $\mathbf H_0$ の定理でもあると分かるが、逆向きには $\mathbf H_0'$ についての別の議論が要る。

公理の独立性

公理図式 (A$k$) が体系の中で独立であるとは、(A$k$) を取り除いた体系で導出できない (A$k$) の実例があることをいう。独立でない公理は、取り除いても定理の集合が変わらない。
独立性を示すには、真理値の集合を 3 つ以上に増やした表を使う。

真理値の表と指定値

空でない有限集合 $V$、その部分集合 $D\subset V$（指定値）、写像 $n\colon V\to V$ と $i\colon V\times V\to V$ の組 $\mathfrak M=(V,D,n,i)$ を考える。命題変数への値の割り当て $w$ を、$w(\lnot\varphi):=n(w(\varphi))$、$w(\varphi\to\psi):=i(w(\varphi),w(\psi))$ で論理式全体に広げる。すべての $w$ で $w(\varphi)\in D$ となる論理式 $\varphi$ を、$\mathfrak M$ で 恒に指定値をとる という。

$V=\{\mathrm T,\mathrm F\}$、$D=\{\mathrm T\}$、$n,i$ を通常の真理値表とすれば、恒に指定値をとる式は恒真式である。この定義は OLT26 の Definition 45.5（行列、p. 673）の、$V$ を有限にし、結合子を $\lnot,\to$ に限った場合である。

表による非導出性

$\mathfrak M=(V,D,n,i)$ と、公理図式の集合 $\mathcal A$ について、次の 2 つを仮定する。

$\mathcal A$ の公理図式のすべての実例が、$\mathfrak M$ で恒に指定値をとる。
MP が指定値を保つ：$x\in D$ かつ $i(x,y)\in D$ ならば $y\in D$。
このとき、$\mathcal A$ と MP からなる体系の定理はすべて $\mathfrak M$ で恒に指定値をとる。

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

割り当て $w$ を任意に固定し、定理 $\varphi$ の導出 $\varphi_1,\dots,\varphi_m=\varphi$ の各行について $w(\varphi_j)\in D$ を $j$ に関する帰納法で示す。$\varphi_j$ が公理なら 1 による。$\varphi_j$ が $\varphi_k$ と $\varphi_l=(\varphi_k\to\varphi_j)$（$k,l< j$）から MP で得られたなら、帰納法の仮定により $w(\varphi_k)\in D$、$w(\varphi_l)=i(w(\varphi_k),w(\varphi_j))\in D$ なので、2 により $w(\varphi_j)\in D$ である。前提のない導出なので、ほかの場合はない。$\square$

公理図式の実例は、文字にどんな論理式を入れたものでもよいが、論理式の値は $V$ の元なので、1 を確かめるには「文字に $V$ の元を入れたときの値」を調べれば足りる。$V$ が有限なので、これは有限回の確認である。

H₀ の公理の独立性

$\mathbf H_0$ の 3 つの公理図式 (A1)・(A2)・(A3) は、どれも他の 2 つと MP から導出できない実例をもつ。具体的に、$p,q,r$ を異なる命題変数として、

$p\to(q\to p)$ は (A2)・(A3) と MP から導出できない。
$(p\to(q\to r))\to((p\to q)\to(p\to r))$ は (A1)・(A3) と MP から導出できない。
$(\lnot q\to\lnot p)\to((\lnot q\to p)\to q)$ は (A1)・(A2) と MP から導出できない。

証明には次の表を使う。値は $V=\{0,1,2\}$、指定値は $D=\{0\}$ である（$0$ が「真」、$2$ が「偽」の役をする）。$i(x,y)$ の表は行が $x$、列が $y$ である。

$i_1(x,y)$	$y=0$	$y=1$	$y=2$
$x=0$	$0$	$2$	$2$
$x=1$	$0$	$0$	$2$
$x=2$	$0$	$0$	$0$
$i_2(x,y)$	$y=0$	$y=1$	$y=2$
:--	:--:	:--:	:--:
$x=0$	$0$	$2$	$2$
$x=1$	$0$	$2$	$0$
$x=2$	$0$	$0$	$0$

否定はどちらも $n(0)=2$、$n(1)=n(2)=0$ とする。$\mathfrak M_1:=(V,D,n,i_1)$、$\mathfrak M_2:=(V,D,n,i_2)$ とおく。

表ごとに公理の値を調べる

$\mathfrak M_1$、$\mathfrak M_2$ に共通する次の性質を使う（$i$ は $i_1$ または $i_2$）。

(a) $i$ と $n$ の値は $0$ か $2$ である。
(b) $i(0,y)=0\iff y=0$ であり、$i(2,y)=0$ である。$n(x)=0\iff x\ne0$ である。
(c) $x,y\in\{0,2\}$ なら、$i(x,y)$ と $n(x)$ は $0$ を真、$2$ を偽とする通常の真理値表どおりである。すなわち $i(x,y)\ne0\iff(x=0$ かつ $y=2)$ である。
MP が指定値を保つこと：$x=0$ かつ $i(0,y)=0$ なら、(b) により $y=0$ である。
(A3) がどちらの表でも恒に指定値をとること：文字 $\varphi,\psi$ に値 $a,b$ を入れ、$P:=i(n(b),n(a))$、$R:=i(n(b),a)$、$Q:=i(R,b)$ とおく。(A3) の値は $i(P,Q)$ で、(a) により $P,Q,R\in\{0,2\}$ である。$i(P,Q)\ne0$ と仮定すると、(c) により $P=0$、$Q=2$ である。$R=2$ なら (b) により $Q=i(2,b)=0$ なので、$R=0$ であり、$Q=i(0,b)=2$ から $b\ne0$ である。(b) により $n(b)=0$ なので、$R=i(0,a)=0$ から $a=0$、したがって $n(a)=2$ となり、$P=i(0,2)=2$ となって $P=0$ に反する。よって (A3) の値はつねに $0$ である。
1（表 $\mathfrak M_1$）：(A2) が恒に指定値をとることを示す。文字 $\varphi,\psi,\chi$ に値 $a,b,c$ を入れ、$X:=i_1(a,i_1(b,c))$、$Y:=i_1(i_1(a,b),i_1(a,c))$ とおく。(A2) の値は $i_1(X,Y)$ で、$X,Y\in\{0,2\}$ である。これが $0$ でないなら (c) により $X=0$、$Y=2$ であり、さらに (c) により $i_1(a,b)=0$、$i_1(a,c)=2$ である。$i_1$ の表から、$i_1(a,c)=2$ は $a\ne2$、$c\ne0$、$(a,c)\ne(1,1)$ を意味し、$a\ne2$ のもとで $i_1(a,b)=0$ は「$b=0$、または $a=b=1$」を意味する。$b=0$ なら $i_1(b,c)=i_1(0,c)=2$（$c\ne0$）である。$a=b=1$ なら $c=2$ で、$i_1(b,c)=i_1(1,2)=2$ である。どちらでも $X=i_1(a,2)=2$（$a\ne2$）となり、$X=0$ に反する。よって (A2) の値はつねに $0$ である。一方、$p,q$ に $1,0$ を割り当てると、$p\to(q\to p)$ の値は $i_1(1,i_1(0,1))=i_1(1,2)=2\notin D$ である。lem-hilbert-style-proof-system-matrix により、この式は (A2)・(A3) と MP から導出できない。
2（表 $\mathfrak M_2$）：(A1) が恒に指定値をとることを示す。文字 $\varphi,\psi$ に値 $a,b$ を入れる。(A1) の値は $i_2(a,i_2(b,a))$ である。$a=0$ なら、$i_2$ の表の $y=0$ の列はすべて $0$ なので $i_2(b,0)=0$、値は $i_2(0,0)=0$ である。$a=2$ なら (b) により値は $0$ である。$a=1$ なら、$i_2(b,1)\in\{0,2\}$ であり、$i_2(1,y)$ は $y\ne1$ のとき $0$ なので、値は $0$ である。一方、$p,q,r$ に $1,0,1$ を割り当てると、$p\to(q\to r)$ の値は $i_2(1,i_2(0,1))=i_2(1,2)=0$、$p\to q$ の値は $i_2(1,0)=0$、$p\to r$ の値は $i_2(1,1)=2$、$(p\to q)\to(p\to r)$ の値は $i_2(0,2)=2$ で、全体の値は $i_2(0,2)=2\notin D$ である。lem-hilbert-style-proof-system-matrix により、この式は (A1)・(A3) と MP から導出できない。
3（2 値の表）：$V=\{\mathrm T,\mathrm F\}$、$D=\{\mathrm T\}$、$\to$ は通常の真理値表とし、否定を $n(x):=x$（何もしない）と解釈する。(A1)・(A2) は $\lnot$ を含まない恒真式なので恒に $\mathrm T$ をとり、MP は $\mathrm T$ を保つ。一方、$q$ に $\mathrm F$、$p$ に任意の値を割り当てると、$(\lnot q\to\lnot p)\to((\lnot q\to p)\to q)$ の値は $(\mathrm F\to p)\to((\mathrm F\to p)\to\mathrm F)=\mathrm T\to(\mathrm T\to\mathrm F)=\mathrm F$ である。lem-hilbert-style-proof-system-matrix により、この式は (A1)・(A2) と MP から導出できない。$\square$

3 つ目の証明が示すように、(A1)・(A2) は $\lnot$ について何も言っていないので、否定のふるまいを決めるのは (A3) だけである。1・2 では、$\mathfrak M_1$ と $\mathfrak M_2$ はどちらも値 $0,2$ の上では通常の真理値表と一致し、3 つ目の値 $1$ の扱いだけで (A1) または (A2) を壊している。$\mathfrak M_2$ では $i_2(1,1)=2$ なので恒等式 $p\to p$ も指定値をとらない。実際、恒等式の導出は (A2) を使う（一階論理の証明体系の記事の補題「恒等式の導出」）。

反例：表の各行の確認

「条件を外した反例」の表の各行を確かめる。1〜3 は lem-hilbert-style-proof-system-matrix の表を 2 値で作り、4 は付値を 1 つ示す。

各行の確認を開く

図式でない公理：命題変数 $p,q,r$ だけで書いた 3 つの式を公理とし MP だけを規則とする体系では、定理に現れる命題変数はすべて $p,q,r$ の中にある。公理ではそうであり、MP で $\varphi$ と $\varphi\to\psi$ から得た $\psi$ の命題変数は $\varphi\to\psi$ の命題変数に含まれるからである（導出の長さに関する帰納法）。よって恒真式 $s\to s$（$s$ は $p,q,r$ と異なる命題変数）は定理でない。
(A3) のない体系：2 値の表で否定をつねに $\mathrm T$ と解釈する（$n(x):=\mathrm T$）。(A1)・(A2) は恒に $\mathrm T$ をとり MP は $\mathrm T$ を保つが、$p$ に $\mathrm F$ を割り当てると $\lnot\lnot p\to p$ の値は $\mathrm T\to\mathrm F=\mathrm F$ である。lem-hilbert-style-proof-system-matrix により $\lnot\lnot p\to p$ は (A1)・(A2) と MP から導出できない。
(A3) の代わりに $\lnot\lnot\varphi\to\varphi$：2 値の表で否定をつねに $\mathrm F$ と解釈する（$n(x):=\mathrm F$）。$\lnot\lnot\varphi\to\varphi$ の値は $\mathrm F\to w(\varphi)=\mathrm T$ で恒に $\mathrm T$ をとり、(A1)・(A2) と MP も上と同じである。$p$ に $\mathrm T$ を割り当てると $p\to\lnot\lnot p$ の値は $\mathrm T\to\mathrm F=\mathrm F$ なので、lem-hilbert-style-proof-system-matrix によりこの恒真式は導出できない。二重否定除去だけでは否定の性質を捉えきれない。
後件肯定：この規則を加えると、前提 $q$ と $p\to q$ から 1 回で $p$ が得られ、$\{q,\ p\to q\}\vdash p$ となる。一方、$p$ を偽、$q$ を真にする付値は前提を真にして $p$ を偽にするので、$\{q,\ p\to q\}\models p$ ではない。