無矛盾性

同義語：無矛盾consistency極大無矛盾理論極大無矛盾集合

概要

前提知識: 一階論理の証明体系, 一階述語論理, Gödelの完全性定理

数学の理論が「矛盾している」とは、その公理からある主張とその否定がどちらも証明できることである。矛盾した理論ではどんな主張も証明できてしまうので、何も区別できなくなる。無矛盾性（consistency）は、この事態が起こらないという性質で、公理系に最初に求められる条件である。
無矛盾性は証明体系の言葉で定義される構文的な性質であり、モデルの存在という意味の側の性質とは定義の上では別物である。しかし一階述語論理では、健全性定理と Gödelの完全性定理によって、文の集合が無矛盾であることとモデルをもつことは同値になる（thm-cons-models）。この記事では、無矛盾性の定義と同値な言い換え、証明可能性との関係、極大無矛盾集合（Lindenbaum の補題）を証明し、例と反例で使い方を示す。

定義

以下、一階言語 $L$ を固定し、証明体系としては一階論理の証明体系の記事の体系 $\mathbf H$ を使う。$\mathbf H$ の基本の記号は $\lnot,\to,\forall,=$ で、論理公理は公理図式 (A1)〜(A8) の実例の全称化、推論規則は前件肯定（MP）だけである。$\Gamma\vdash\varphi$ は論理式の集合 $\Gamma$ から論理式 $\varphi$ が $\mathbf H$ で導出できることを表す。$\mathbf H$ の公理のうち、以下で直接使うのは次の 2 つである。

(A1) $\alpha\to(\beta\to\alpha)$
(A3) $(\lnot\beta\to\lnot\alpha)\to((\lnot\beta\to\alpha)\to\beta)$

無矛盾性

$L$ の論理式の集合 $\Gamma$ が 矛盾する（inconsistent）とは、ある論理式 $\varphi$ について
$$ \Gamma\vdash\varphi\quad\text{かつ}\quad\Gamma\vdash\lnot\varphi $$
が成り立つことをいう。矛盾しないとき、$\Gamma$ は 無矛盾（consistent）であるという。
無矛盾な $\Gamma$ で、$\Gamma$ を真に含む $L$ の論理式の集合がどれも矛盾するものを 極大無矛盾（maximally consistent）という。

文の集合を理論とよぶときは、理論が無矛盾であるともいう。定義は証明体系 $\vdash$ に依存しているが、文の集合については、健全かつ完全な体系であればどれを使っても同じ概念になる（thm-cons-models の後の段落）。

直感

公理系を「世界の性質を書き並べたもの」と見ると、無矛盾性は「書いたことが互いにぶつからない」ことである。ぶつかれば、そこから何でも導けてしまい（lem-cons-explosion）、公理系は何の情報ももたなくなる。一方、ぶつからないかどうかを証明の側だけで確かめるのは一般に難しい。導出は無限にありうるからである。そこで、公理をすべて満たす具体的な構造（モデル）を 1 つ作れば、健全性によって無矛盾性が保証される。逆に、無矛盾ならモデルが必ず作れるというのが完全性定理の内容である。

基本性質

矛盾からは何でも導ける

矛盾からの導出

任意の論理式 $\varphi,\chi$ について $\{\varphi,\lnot\varphi\}\vdash\chi$ である。

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

$\lnot\varphi$ ——前提
$\lnot\varphi\to(\lnot\chi\to\lnot\varphi)$ ——(A1)
$\lnot\chi\to\lnot\varphi$ ——1、2 から MP
$\varphi$ ——前提
$\varphi\to(\lnot\chi\to\varphi)$ ——(A1)
$\lnot\chi\to\varphi$ ——4、5 から MP
$(\lnot\chi\to\lnot\varphi)\to((\lnot\chi\to\varphi)\to\chi)$ ——(A3) で $\beta$ を $\chi$、$\alpha$ を $\varphi$ にした実例
$(\lnot\chi\to\varphi)\to\chi$ ——3、7 から MP
$\chi$ ——6、8 から MP $\square$

これは 爆発律（ex falso quodlibet）ともよばれる。この補題から、矛盾の定義はいくつかの同値な形に言い換えられる。

矛盾の言い換え

論理式の集合 $\Gamma$ について、次の 3 つは同値である。

$\Gamma$ は矛盾する。
すべての論理式 $\chi$ について $\Gamma\vdash\chi$ である。
$\Gamma$ のある有限部分集合 $\Gamma_0$ が矛盾する。
とくに、$\Gamma$ が無矛盾であることは、$\Gamma$ から導出できない論理式が 1 つでもあることと同値であり、$\Gamma$ のすべての有限部分集合が無矛盾であることとも同値である。

以下、一階論理の証明体系の記事の命題「導出可能性の基本性質」の 1〜4（反射性・単調性・有限性・推移性）を使う。
1 ⇒ 2：$\Gamma\vdash\varphi$、$\Gamma\vdash\lnot\varphi$ とする。lem-cons-explosion により $\{\varphi,\lnot\varphi\}\vdash\chi$ なので、推移性により $\Gamma\vdash\chi$ である。
2 ⇒ 1：論理式 $\varphi$ を 1 つとれば、2 により $\Gamma\vdash\varphi$ かつ $\Gamma\vdash\lnot\varphi$ である。
1 ⇒ 3：$\Gamma\vdash\varphi$ と $\Gamma\vdash\lnot\varphi$ の導出をそれぞれ 1 つとる。有限性により、それぞれの導出で前提として使われる $\Gamma$ の元は有限個である。その全体を $\Gamma_0$ とすれば、$\Gamma_0$ は有限で $\Gamma_0\vdash\varphi$、$\Gamma_0\vdash\lnot\varphi$ である。
3 ⇒ 1：$\Gamma_0\subset\Gamma$ なので、単調性により $\Gamma_0$ からの導出はそのまま $\Gamma$ からの導出である。$\square$

3 の性質を、無矛盾性の 有限性（finite character）という。導出が有限の列であることから来る性質で、後の Lindenbaum の補題の証明で本質的に使う。

証明できることと無矛盾性

証明可能性と無矛盾性

論理式の集合 $\Gamma$ と論理式 $\varphi$ について、次が成り立つ。

$\Gamma\vdash\varphi$ であることと、$\Gamma\cup\{\lnot\varphi\}$ が矛盾することは同値である。
$\Gamma\vdash\lnot\varphi$ であることと、$\Gamma\cup\{\varphi\}$ が矛盾することは同値である。
$\Gamma$ が無矛盾ならば、$\Gamma\cup\{\varphi\}$ と $\Gamma\cup\{\lnot\varphi\}$ の少なくとも一方は無矛盾である。

1：$\Gamma\vdash\varphi$ なら、単調性により $\Gamma\cup\{\lnot\varphi\}\vdash\varphi$ であり、反射性により $\Gamma\cup\{\lnot\varphi\}\vdash\lnot\varphi$ なので矛盾する。逆に $\Gamma\cup\{\lnot\varphi\}$ が矛盾するとする。prop-cons-equivalents の 2 により $\Gamma\cup\{\lnot\varphi\}\vdash\varphi$ であり、また $\Gamma\cup\{\lnot\varphi\}\vdash\lnot\varphi$ である。一階論理の証明体系の記事の定理「一階論理の演繹定理」により
$$ \Gamma\vdash\lnot\varphi\to\varphi,\qquad\Gamma\vdash\lnot\varphi\to\lnot\varphi $$
である。(A3) で $\alpha,\beta$ をともに $\varphi$ にした実例 $(\lnot\varphi\to\lnot\varphi)\to((\lnot\varphi\to\varphi)\to\varphi)$ と MP を 2 回使えば $\Gamma\vdash\varphi$ を得る。
2：$\Gamma\vdash\lnot\varphi$ なら、1 の前半と同じ理由で $\Gamma\cup\{\varphi\}$ は矛盾する。逆に $\Gamma\cup\{\varphi\}$ が矛盾するとする。$\{\lnot\lnot\varphi\}\vdash\varphi$ である（下の注意）。したがって、$\Gamma\cup\{\varphi\}$ から導出できる論理式は、推移性により $\Gamma\cup\{\lnot\lnot\varphi\}$ からも導出できる。prop-cons-equivalents の 2 により $\Gamma\cup\{\varphi\}$ からはすべての論理式が導出できるので、$\Gamma\cup\{\lnot\lnot\varphi\}$ からもすべての論理式が導出でき、これは矛盾する。1 を論理式 $\lnot\varphi$ に当てはめれば $\Gamma\vdash\lnot\varphi$ である。
3：$\Gamma\cup\{\varphi\}$ と $\Gamma\cup\{\lnot\varphi\}$ がともに矛盾するなら、2 により $\Gamma\vdash\lnot\varphi$、1 により $\Gamma\vdash\varphi$ であり、$\Gamma$ は矛盾する。$\square$

2 の証明で使った $\{\lnot\lnot\varphi\}\vdash\varphi$ は、Hilbert流の証明体系の記事の例「二重否定の除去」の導出による。そこでの体系 $\mathbf H_0$ の公理 (A1)〜(A3) は $\mathbf H$ の (A1)〜(A3) と同じ形なので、命題変数を一階の論理式に置き換えた同じ列が $\mathbf H$ での導出になる。
1 は「$\varphi$ を証明するには、$\lnot\varphi$ を仮定して矛盾を導けばよい」という背理法の形式化であり、3 は「無矛盾な公理系には、どんな主張か、その否定のどちらかを公理として付け加えてよい」ことを述べている。

無矛盾性とモデル

モデルをもてば無矛盾

$L$ 構造 $\mathcal M$ と割り当て $s$ で、$\Gamma$ のすべての元を $\mathcal M\models\gamma[s]$ と満たすものがあれば、$\Gamma$ は無矛盾である。とくに、モデルをもつ文の集合は無矛盾である。

$\Gamma\vdash\varphi$ かつ $\Gamma\vdash\lnot\varphi$ となる $\varphi$ があったとする。一階論理の証明体系の記事の定理「健全性定理」により $\Gamma\models\varphi$ かつ $\Gamma\models\lnot\varphi$ であり、$\mathcal M,s$ は $\Gamma$ を満たすので $\mathcal M\models\varphi[s]$ かつ $\mathcal M\models\lnot\varphi[s]$ となる。$\lnot$ の充足の定義により、これは起こらない。$\square$

逆向きは完全性定理の言い換えである。

無矛盾性とモデルの存在

文の集合 $\Gamma$ について、$\Gamma$ が無矛盾であることと、$\Gamma$ がモデルをもつことは同値である。

モデルをもてば無矛盾であることは thm-cons-sound である。逆に、無矛盾な文の集合がモデルをもつことは、Gödelの完全性定理の記事の定理「Gödelの完全性定理」と、同記事の命題「完全性とモデル存在」（完全性定理と「無矛盾な文集合はモデルをもつ」の同値性）による。$\mathbf H$ は健全かつ完全な体系なので、この命題が当てはまる。$\square$

可算言語の場合、無矛盾な文の集合から実際にモデルを組み立てる議論は Gödelの完全性定理の記事の補題「モデル存在定理（可算言語）」にある。
thm-cons-models の右辺はモデルの存在で、証明体系に言及していない。したがって、文の集合については、健全かつ完全などの体系で無矛盾性を定義しても同じ集合が無矛盾になる。たとえばシーケント計算では、$\Gamma$ が矛盾することを「$\Gamma$ のある有限部分集合 $\Gamma_0$ について、右辺が空のシーケント $\Gamma_0\Rightarrow$ が導出できること」と定義するのが普通である（Zac25 Definition 10.12、p. 176）。この定義は体系 $\mathbf H$ による定義と見た目が違うが、どちらの体系も健全かつ完全なので、文の集合については同じ概念を定める。

極大無矛盾集合

Lindenbaum の補題

（選択公理を仮定する。）無矛盾な論理式の集合 $\Gamma$ は、ある極大無矛盾集合 $\Delta\supset\Gamma$ に含まれる。

$\Gamma$ を含む無矛盾な $L$ の論理式の集合の全体を $\mathcal P$ とし、包含関係で順序を入れる。$\Gamma\in\mathcal P$ なので $\mathcal P$ は空でない。
空の鎖は $\Gamma$ を上界にもつ。$\mathcal P$ の空でない鎖 $\mathcal C$ をとり、$U:=\bigcup\mathcal C$ とおく。$U$ が無矛盾であることを示す。$U$ が矛盾するなら、prop-cons-equivalents の 3 により有限部分集合 $U_0=\{\gamma_1,\dots,\gamma_n\}\subset U$ が矛盾する。各 $\gamma_i$ はある $C_i\in\mathcal C$ に属し、$\mathcal C$ は鎖なので $C_1,\dots,C_n$ のうち最大のもの $C$ がある（$n=0$ なら $\mathcal C$ の任意の元を $C$ とする）。$U_0\subset C$ なので、単調性により $C$ も矛盾し、$C\in\mathcal P$ に反する。よって $U$ は無矛盾で、$\Gamma\subset U$ だから $U\in\mathcal P$ は $\mathcal C$ の上界である。
Zornの補題により $\mathcal P$ は極大元 $\Delta$ をもつ。$\Delta$ を真に含む論理式の集合 $\Delta'$ が無矛盾なら、$\Gamma\subset\Delta'$ なので $\Delta'\in\mathcal P$ となり、$\Delta$ の極大性に反する。よって $\Delta$ は極大無矛盾である。$\square$

言語 $L$ が可算なら、論理式を $\varphi_0,\varphi_1,\dots$ と並べ、prop-cons-provability の 3 を使って $\varphi_n$ か $\lnot\varphi_n$ を順に付け加えていけば、Zorn の補題を使わずに極大無矛盾集合が得られる。Gödelの完全性定理の記事の補題「モデル存在定理（可算言語）」の証明はこの形をとっており、Zac25 Lemma 12.8（pp. 237–238）も同じ構成である。

極大無矛盾集合の性質

$\Delta$ を極大無矛盾集合とする。論理式 $\varphi,\psi$ について次が成り立つ。

$\Delta\vdash\varphi$ ならば $\varphi\in\Delta$ である。
$\varphi$ と $\lnot\varphi$ のうち、ちょうど一方が $\Delta$ に属する。
$(\varphi\to\psi)\in\Delta$ であることと、「$\varphi\notin\Delta$ または $\psi\in\Delta$」は同値である。

1：$\Delta\cup\{\varphi\}$ が矛盾するなら、prop-cons-provability の 2 により $\Delta\vdash\lnot\varphi$ であり、$\Delta\vdash\varphi$ と合わせて $\Delta$ が矛盾する。よって $\Delta\cup\{\varphi\}$ は無矛盾で、極大性から $\varphi\in\Delta$ である。
2：両方が属すれば $\Delta$ は矛盾する。prop-cons-provability の 3 により $\Delta\cup\{\varphi\}$ か $\Delta\cup\{\lnot\varphi\}$ が無矛盾で、極大性からそれは $\Delta$ に等しい。よって少なくとも一方が属する。
3：$(\varphi\to\psi)\in\Delta$ かつ $\varphi\in\Delta$ なら、MP により $\Delta\vdash\psi$ で、1 により $\psi\in\Delta$ である。逆に $\psi\in\Delta$ なら、(A1) の実例 $\psi\to(\varphi\to\psi)$ と MP で $\Delta\vdash\varphi\to\psi$ である。$\varphi\notin\Delta$ なら 2 により $\lnot\varphi\in\Delta$ である。lem-cons-explosion により $\{\lnot\varphi,\varphi\}\vdash\psi$ なので、演繹定理により $\{\lnot\varphi\}\vdash\varphi\to\psi$ であり、単調性から $\Delta\vdash\varphi\to\psi$ である。どちらの場合も 1 により $(\varphi\to\psi)\in\Delta$ である。$\square$

文だけを考える場合も同じである。文の集合 $\Delta$ が無矛盾で、$\Delta$ を真に含む文の集合がどれも矛盾するとき、$\Delta$ を 極大無矛盾理論 という（論理式の集合としては極大とは限らない）。thm-cons-lindenbaum と prop-cons-maximal の証明は、論理式の集合を文の集合に、論理式 $\varphi,\psi$ を文に読み替えてもそのまま通る。したがって、無矛盾な文の集合はある極大無矛盾理論に含まれ、極大無矛盾理論は文 $\varphi,\psi$ について prop-cons-maximal の 1〜3 を満たす。
2 と 3 は、$\Delta$ に属することを「真」と読めば、$\lnot$ と $\to$ が真理値表どおりに振る舞うことを述べている。完全性定理の証明は、この真理値の割り振りを量化記号まで含めて実現する構造を作るものである。文だけからなる無矛盾な理論で、どの文についてもそれ自身かその否定が導出できるものは完全な理論の記事で扱う。

例

群の公理系

言語 $\{e,\cdot,{}^{-1}\}$ で群の公理（結合法則、単位元、逆元の 3 つの文）を書いた集合 $T_{\mathrm{grp}}$ は無矛盾である。1 元の集合 $\{e\}$ に演算を $e\cdot e=e$、$e^{-1}=e$ と入れた自明な群がモデルであり、thm-cons-sound が使えるからである。可換性の文を加えても、その否定を加えても無矛盾である。前者は自明な群、後者は 3 次の対称群 $S_3$ がモデルになる。これは、$T_{\mathrm{grp}}$ から可換性も非可換性も導出できないことを意味する（prop-cons-provability の 1、2）。

3 つそろうと矛盾する集合

$P,Q$ を 1 変数の述語記号、$c$ を定数記号とし、$\Gamma:=\{P(c),\ P(c)\to Q(c),\ \lnot Q(c)\}$ とおく。$\Gamma$ は矛盾する。$P(c)$ と $P(c)\to Q(c)$ から MP で $\Gamma\vdash Q(c)$ であり、$\lnot Q(c)\in\Gamma$ だからである。一方、$\Gamma$ から 1 つを除いた 3 つの 2 元集合はどれも無矛盾である。台集合 $\{0\}$、$c=0$ の構造で、$P,Q$ の解釈を $(\{0\},\{0\})$、$(\emptyset,\emptyset)$、$(\{0\},\emptyset)$ とすれば、それぞれ $\lnot Q(c)$、$P(c)$、$P(c)\to Q(c)$ を除いた集合のモデルになる。矛盾は 1 つの公理だけを見ても分からず、公理の組み合わせから生じる。

素朴な内包公理

言語 $\{\in\}$ で、各論理式 $\varphi(x)$（$y$ を自由変数にもたない）について文
$$ \exists y\,\forall x\,(x\in y\leftrightarrow\varphi(x)) $$
（「$\varphi$ を満たすものの集まりは集合である」）を公理とする理論は矛盾する。$\varphi(x)$ を $\lnot\,x\in x$ にした公理のモデル $\mathcal M$ があったとすると、ある $b\in M$ が「すべての $a\in M$ について $a\in^{\mathcal M}b\iff a\notin^{\mathcal M}a$」を満たす。$a=b$ とおくと $b\in^{\mathcal M}b\iff b\notin^{\mathcal M}b$ となり、これは起こらない。したがってこの 1 つの公理はモデルをもたず、thm-cons-models により矛盾する。これは Russell のパラドックスを一階の理論の言葉で述べたものである。

Peano 算術

一階の Peano 算術 $\mathsf{PA}$ の公理はすべて自然数の構造 $(\mathbb N,0,S,+,\cdot)$ で真なので、thm-cons-sound により $\mathsf{PA}$ は無矛盾である。ただしこの議論は、集合 $\mathbb N$ とその上の真偽を扱える集合論の中で行っている。$\mathsf{PA}$ の無矛盾性を表す算術の文 $\mathrm{Con}_{\mathsf{PA}}$ は、$\mathsf{PA}$ が無矛盾である限り $\mathsf{PA}$ から導出できない（Gödel の第 2 不完全性定理。OLT26 Theorem 37.8、p. 588。この記事では証明しない）。理論の無矛盾性を示すには、その理論より強い何らかの道具が要る。

集合論のように、無矛盾性を示すモデルを手近に作れない理論については、ある理論が無矛盾ならば別の理論も無矛盾である、という 相対的な無矛盾性 が調べられる。たとえば ZF が無矛盾ならば ZFC も無矛盾である（Kun80 Chapter V, Corollary 2.14、p. 162。一般連続体仮説を加えた形は Chapter VI, Corollary 4.9、p. 175）。

反例：条件を外すと成り立たない

外す条件	反例	成り立たなくなること
thm-cons-lindenbaum の「$\Gamma$ が無矛盾」	$\Gamma=\{P(c),\lnot P(c)\}$	極大無矛盾集合への拡大の存在
thm-cons-sound の「体系が健全」	$\mathbf H$ に公理 $\exists x\,P(x)\to\forall x\,P(x)$ を加えた体系 $\mathbf H'$ と $\Gamma=\{P(c),\lnot P(d)\}$	モデルをもてば無矛盾
thm-cons-models の「体系が完全」	公理も推論規則ももたない体系と $\Gamma=\{\forall x\,P(x),\lnot P(c)\}$	無矛盾ならモデルをもつ
prop-cons-maximal の「極大」	無矛盾な $\Delta=\{P(c)\}$ と $\varphi=Q(c)$	$\varphi$ か $\lnot\varphi$ が $\Delta$ に属する

反例の確かめ

1 行目：$\Gamma$ は矛盾するので、$\Gamma$ を含む集合はすべて矛盾し（単調性）、無矛盾な拡大は 1 つもない。
2 行目：$\Gamma$ は、台集合 $\{0,1\}$、$c=0$、$d=1$、$P=\{0\}$ の構造をモデルにもつ。$\exists x\,P(x)$ は $\lnot\forall x\,\lnot P(x)$ の略記で、$\{P(c)\}\models\exists x\,P(x)$ なので、$\mathbf H$ の完全性（Gödelの完全性定理）により $\{P(c)\}\vdash\exists x\,P(x)$ であり、$\mathbf H'$ でも同じ導出が使える。新しい公理と MP で $\forall x\,P(x)$、(A4) の実例 $\forall x\,P(x)\to P(d)$ と MP で $P(d)$ が $\Gamma$ から $\mathbf H'$ で導出でき、$\lnot P(d)\in\Gamma$ なので $\Gamma$ は $\mathbf H'$ で矛盾する。新しい公理は上の構造で偽なので、$\mathbf H'$ は健全でない。
3 行目：公理も規則もない体系では、導出の各行は前提でなければならないので、$\Gamma\vdash\varphi$ は $\varphi\in\Gamma$ と同値である。$\Gamma$ には $P(c)$ も $\lnot\forall x\,P(x)$ も属さないので、$\Gamma$ はこの体系で無矛盾である。しかし $\forall x\,P(x)$ を満たす構造では $P(c)$ が真なので、$\Gamma$ はモデルをもたない。この体系は健全だが完全でない（Gödelの完全性定理の記事の演習「健全だが完全でない証明体系」）。
4 行目：台集合 $\{0\}$、$c=0$、$P=\{0\}$ の構造で $Q$ を $\{0\}$ と解釈しても $\emptyset$ と解釈しても $\Delta$ のモデルになるので、thm-cons-sound により $\Delta\cup\{Q(c)\}$ と $\Delta\cup\{\lnot Q(c)\}$ はどちらも無矛盾である。とくに $\Delta$ はどちらも含まないので極大でなく、2 の結論は成り立たない。

補足

ω無矛盾という条件

算術の理論 $T$ が ω無矛盾（ω-consistent）であるとは、どの論理式 $\varphi(x)$ についても、すべての自然数 $n$ で $T\vdash\lnot\varphi(\overline n)$ でありながら $T\vdash\exists x\,\varphi(x)$ となることはない、という条件である（$\overline n$ は $n$ を表す項。OLT26 §36.3, Definition 36.2、p. 574）。$T$ が矛盾すれば何でも導出できるので、ω無矛盾な理論は無矛盾である。逆は成り立たない。$\mathsf{PA}$ が無矛盾なら $\mathsf{PA}\cup\{\lnot\mathrm{Con}_{\mathsf{PA}}\}$ は無矛盾だが、この理論は「矛盾の導出の番号 $x$ がある」という存在文を導出する一方で、各自然数 $n$ について「$n$ は矛盾の導出の番号でない」ことも導出する（OLT26 §26.1、p. 393）。Gödel の最初の不完全性の結果はこの仮定のもとで述べられ、その後まもなく通常の無矛盾性の仮定に弱められた（同書 §36.3、p. 574）。

「証明できない」と「否定が証明できる」

prop-cons-provability の 1 により、$\Gamma\nvdash\varphi$ は「$\Gamma\cup\{\lnot\varphi\}$ が無矛盾」と同値であり、「$\Gamma\vdash\lnot\varphi$」とは違う。$\Gamma\nvdash\varphi$ かつ $\Gamma\nvdash\lnot\varphi$ となる $\varphi$ は、$\Gamma\cup\{\varphi\}$ と $\Gamma\cup\{\lnot\varphi\}$ がどちらも無矛盾な $\varphi$ であり、$\Gamma$ から独立であるという。ex-cons-group の可換性は群の公理系から独立である。