極大と無矛盾は冗長表現ではなかった
辞書的に使っている『情報科学における論理』を調べてみたら、「極大無矛盾」の定義に関して、僕が誤解していたようだ。（誤解していたのではなくて、用語法が2種類以上あるのかもしれない。）
まず、矛盾（無矛盾）の用法を並べる：
- 公理系Aが矛盾する：A|- false
- 公理系Aが矛盾する：A|- f かつ A|- ¬f
- セオリーTが矛盾する：T = L （Lはすべての論理式）
- セオリーTが矛盾する：false∈T
- 公理系or証明系が矛盾する：{証明可能論理式}∩{反証可能論理式}≠空
- 論理式の集合Aが矛盾する：Aはモデルを持たない。
1番目と2番目は、false≡f∧¬f なら区別する必要はない、単に言い方の違いに過ぎない。3番目と4番目も「false∈T ⇒ T = L（Lは全体）」のもとで同じこと。5番目は、2番目を外延的表現で言い換えたもの。最後の矛盾概念は異質で、モデル論的な概念（構文論／証明論だけでは定義不可能な概念）。
さて、A、B⊆Lがあるとき、対(A, B)が無矛盾、またはAがBに対して無矛盾であることを次のように定義する（この定義は、『情報科学における論理』のものと少し違う。）
- 任意のb∈Bに対して、A |- b ではない。(Bのどんな論理式もAから証明できない。）
まず、「A |- b でない（bはAから証明できない）」ならば、「<A> |- b ではない」となるので、Aは、必要があればセオリーに拡張（またはセオリーと仮定）しても問題はない。
B={¬f | f∈A}（BはAに属する式の否定の全体）とすれば、AがBに対して無矛盾なら「f∈A ならば、A |- ¬f ではない」となる。これから、「f∈A かつ A |- ¬f」となるfの存在を否定できる。よって、特にAがセオリーなら普通の（肯定／否定が共に証明できることはない、という）意味で無矛盾となる。
B={false}とすれば、セオリーAがBに対して無矛盾なことはfalse!∈Aと同じことで、これもセオリーAが無矛盾であることの表現になっている。
今度は、B={f | f!∈A}と置く（!は否定）。このケースでは、「f!∈A ならば、A |- f ではない」となり、単にAがセオリーであること（の対偶）になる。
AがBに対して無矛盾であり、A∪B = L （Lは全体）のとき、無矛盾な対(A, B)は極大と呼ぶ。セオリーAとその補集合の対は極大無矛盾な対となる。セオリーAとAの論理式の否定を集めたBが極大無矛盾になるとは限らない。これが極大になるとき、Aは構文論的に完全（決定性を持つ）で、これまた通常の意味でAは極大。
AcはAの補集合、A¬をAの否定を集めた集合と約束して、以上をまとめると：
- Aは任意、(A、Ac)が無矛盾 ⇔ Aがセオリー
- Aはセオリー、(A、A¬)が無矛盾 ⇔ A|-fかつA|-¬fでないので、Aは無矛盾セオリー
- Aはセオリー、(A、{false})が無矛盾 ⇔ false !∈A で、Aは無矛盾セオリー
- Aはセオリー、(A、A¬)が極大無矛盾 ⇔ Aは決定性を持ち、通常の意味で極大。
セオリーAのBに相対的な無矛盾性は、Bの取り方で色々な概念を導けるといえる。(A, B)が極大無矛盾のとき、A∩Bは空（そうでないと無矛盾にならない）であり、対の極大性はAが決定性を持つ（構文的完全である）ことと同じである。
[追記]
「AがBに対して無矛盾」を形式的に書けば ∀b. b∈B→¬(A |- b)。あるいは、書き換えて ∀b. ¬(b∈B)∨¬(A |- b)。
BがL（全体）のときはb∈Bが常にtrueだから、∀b. false∨¬(A |- b)、∀b. ¬(A |- b) となる。つまり、「Aが全体に対して無矛盾」のときは「Aは何も証明できない」。つまりはAが空であることを意味する。
Bが空の時はb∈Bが常にfalseだから、∀b. true∨¬(A |- b)。つまり、「Aが空に対して無矛盾」は恒真である。いかなるAも空に対しては無矛盾。
[/追記]
「飽和」（saturate）という言葉もあったようが気がするが、正確な定義は憶えてないなぁ。極大と同じだったような気もするが、構成的なんだっけ？ 今はあんまり使わないのかな、飽和ってのは。
