ドウセンの論文：一貫性の理解

ドウセンの論文で、一貫性をどう理解すべきかがやっと（少し）わかった気がする。

まず、素朴集合論に対する公理的集合論のように、公理的圏論（axiomatic category theory）あるいは形式的圏論（formal category theory）の文脈で考えないといけない。これは重要だ。

公理的圏論における公理系（その他諸々一式）で定義される概念を、圏のブランド（a brand of category）と呼ぼう（ドウセンの用語）。ブランドは正確に定義しにくいが、公理系のモデルである圏の圏（僕はレルムと呼んでいる）は、ウルトラ超越的な立場では外延として実在するから、ブランドの意味はレルムだと言ってもいい。ただし、レルムが純粋に外延なのに対して、ブランドはもっとイデアル（理念的）で、ブランドの実現として公理系がある、という雰囲気。

一貫性は、ブランドを実現する公理系に対する性質を述べている。論理との比較（比喩？）でまとめると次のようになる。

論理	公理的圏論
論理式	等式
健全性	健全性
充分性、(弱)完全性	完全性
(強)完全性	一貫性

もともと用語法が混乱しているが、充分性はadequacyのつもり。十分条件（sufficient condition）の「十分」と区別して「充分」とした。ちなみに、充足はsatisfyの訳語。

では、一貫性（コヒーレンス）は（強い意味の）完全性の同義語かというとニュアンスが違うのだ。まず、一貫性が扱う論理式（論理文）は等式系である。等式系は可換図式の表現で、実質は可換図式とも言える。Dが図式で、対応する等式系をEとすると、|- E ⇔ Comm(D) という感じ。図式のクラスDに対して、∀D∈D.[|- E(D) ⇔ Comm(D)] のようなメタな言明を問題にする。Comm(D)はモデル論の主張で、実際の圏のなかでの成立することを意味している。

一貫性のもう一つの特徴は、レルムに属する任意の圏を相手にするのではなくて、通常は自由圏と典型モデルを扱うこと。自由圏をうまく構成し、「等式系が自由圏で成立するなら、証明可能である」という命題（完全性の一形態）を述べる。レルム内の任意の圏が、典型圏と圏同値になる、という定理も必要だ。

自由圏をリンデンバウム代数として構成すれば、上の意味の完全性は当たり前になる。結局問題は、リンデンバウム代数の実際の構成法。それと、リンデンバウム代数＝自由圏よりさらに扱いやすい特定のモデル（典型モデルと呼ぼう）を構成して、充満関手G:F→M を構成すること。

Fがあるブランド（公理系、形式理論）のリンデンバウム代数＝自由圏なら、f = g in F ⇔ |- 'f = g' はFの作り方から当たり前。f = g in F ⇒ G(f) = G(g) in M も当然だが、これが典型モデルMに対する“あるブランドのセオリー”の健全性となる。通常、G(f)は、自由圏の射fの絵図表現となる。完全性が成り立つには、Mの射が必ずGの像となることが必要で、これはGの充満性の主張となっている。

Gが自由圏（特定の形式圏論＝ブランドのリンデンバウム代数）から典型モデルへの充満関手であることを示せば一貫性が従うが、より強く、典型モデルMが自由圏Fと圏同値（あるいは圏同型）であることまで示せることもある。シャムの定理はそのような例となっている。