冬眠はしたいし、お水問題に気分暗澹だし、こんなときには「極大（無矛盾）セオリーというのはどういうことでしょうか」なんてコメントに過剰反応しちゃうぞ。
公理系と証明可能性
まず、論理式（formula、文とも呼ぶ）全体の集合をLだとします。Lの部分集合Aを公理系と呼ぶことにします。論理の構文論の文脈では、Aはまったく勝手な部分集合です。有限である必要もないし、A={}（空）でも、A=Lでもかまいません。
Lには推論（証明）のシステムが付いているとして、X⊆Lと、f∈Lに対して、「Xからfが証明できる」ときに、X |- f と書きます。記号「|-」は、論理式や証明系を外から眺めたメタな言明の語彙であることに注意してください。
セオリー
先に定義した公理系（Lの勝手な部分集合）をセオリーと呼ぶ人も多いのですが、僕は次の性質を持つときにセオリーと呼んだほうがいいと思っています。
- T⊆L がセオリーだとは、T |- f ならば f∈T
つまり、論理式の集合がセオリーだとは、証明に関して閉じていることです。Aが公理系だとして、Aを含む最小のセオリーを<A>と書くことにします。これは、<A>={f∈L | A |- f} として定義できます。言い換えれば、<A>は“公理系Aから導出される定理の全体”ですね。ちなみに、<A>という書き方は、閉包とか生成された部分系を表す一般的記法です。
極大（無矛盾）セオリー
さて、極大（無矛盾）セオリーの定義です。Tが極大（無矛盾）セオリーであるとは：
- Tはセオリーである。
- T≠L 。
- Tより真に大きなセオリーはL以外にない。
唐突でしょうが、「T≠L」のとき、Tは無矛盾というのです。「セオリーが矛盾する」の定義は「T = L」なのですよ。無矛盾セオリー（L以外のセオリー）しか相手にしないので、「無矛盾」をわざわざ付けないことも多いですね。（[追記 date="12-27"]「極大無矛盾」という形容詞の語源（とラショネール）は別にあったようです。http://d.hatena.ne.jp/m-hiyama/20051227/1135676094 を参照。[/追記]）
極大セオリーの性質
任意の無矛盾な公理系Aに対して、Aを含む極大セオリーが存在します。これを示すには、普通、ツォルンの補題を使ってしまいます。Lが具体的に与えられていれば、構成的に示すことができるケースもあります。
[追記 date="12-23"]
上の段落で、「無矛盾な」が抜けていました。Aが無矛盾とは、Aからfalseが証明されないことです。これは <A>≠L と同じことです。さらに言い換えれば、A⊆T、T≠LであるセオリーTがあるならAは無矛盾ですね。
[/追記]
証明系が古典論理に基づく標準的なシステムなら、極大セオリーTは次の性質を持ちます。
- 任意のf∈Lに対して、f∈T か ¬f∈T のどちらか一方が必ず成り立つ。
¬fはfの古典的否定です。もし、f∈T かつ ¬f∈T ならば、(f∧¬f)∈Tのはずです、これは証明系が fとgからf∧gを導くからですね。(f∧¬f)はfalseですから、false∈Tとなり、さらにfalseを仮定してどんな論理式でも導出できるんで、T = L となり無矛盾の仮定に反します。よって、「f∈T かつ ¬f∈T」（両方とも入っている）はあり得ません。
次に、fも¬fもTに入ってない状況を考えると、{f}∪TはTより真に大きな集合（公理系）です。T' = <{f}∪T> は、Tより真に大きなセオリーです。T'≠Lであることを示せれば、Tが極大であることに反して、両方とも入ってない可能性も排除できます。
Tがセオリーのとき、fも¬fもTに入ってないなら、T |- f でもないし T |- ¬f でもありません、セオリーの定義からそうなりますよね。「T |- ¬f じゃないならば、T'は無矛盾」は、当該の証明系において演繹定理が成り立ち、モダスポネンスが使えるなら示せます。詳細は論理の教科書内で探してみてください。
これでわかることは、極大セオリーが究極の決定能力を持つことです。「白黒つけろよ」の要求に完璧に応えてくれます。ってことは理想的／超越的な存在で実際にはありそうにない系ですよね。現実的なセオリーはここまで強くなくて、たくさんの極大セオリーの共通部分として表現されます。
最後に一言：極大セオリーが理想的概念であることは、（空間の）点が理想的概念であることと事情は同じです。
