証明の文脈問題とバックワード・リーズニングと偏極ダブル
A1, ..., Anを仮定（assume）してBを結論（conclude, entail, result, produce, show）する証明があるとき、その証明内で使っている暗黙の知識がある。これを証明の文脈とか環境と呼ぶ。
で、文脈とは正確には何か？ が大問題。
それと、トンネル論法（コンパクト有向シーケント計算／高次シーケント計算の動機 - 檜山正幸のキマイラ飼育記 メモ編参照）の合理化も問題だ。
これらを解決するために、
- 文脈の定式化としてコンピュータッド（＝指標＝生成系＝プレゼンテーション≒スケッチ）を使う。
- バックワード・リーズニングの定式化として圏の偏極ダブルを使う。
ΓをドクトリンDのコンピュータッドとする。ドクトリンについては、
ドクトリンが決まると、そのドクトリンに対するコンピュータッドと、コンピュータッドから生成される圏が定義される。Γに対するドクトリンDのもとでの生成された圏をΓ*とする。スターはクリーネスターの拡張だと思ってよい。実際に使うドクトリンは、CCC（デカルト閉圏）、DpCCC（両付点デカルト閉圏）DCCC（両デカルト閉圏）など。
実際には、特定のドクトリンに対するコンピュータッドの定義と作り方、クリーネスターオペレーターの具体的な構成は難しい。
文脈＝コンピュータッドとして、文脈Γのもとで、fがA1, ..., Anを仮定してBを結論する証明であることを次のように書く。
- Γ| f:A1, ..., An->B
矢印は、ハイフン＋不等号を使う。その意味は、
- fは、圏Γ*の射である。
コンピュータッドから生成された圏Γ*は、命題を対象として、証明を射とする圏である。文脈が違うということは、背景圏（＝文脈圏＝環境圏＝ambient＝environment）が違うので、射とその存在性が違ってくるのは当然。
次に、バックワード証明＝逆行証明は次の形に書く。
- Γ| g:B-<A1, ..., An
これは、直接的には、gが反対圏(Γ*)opの射であることを意味する。gのもとの圏での対応物をfrevと書いて、反転（reverse, reversal）と呼ぶ。次の２つは同じである。
- gは(Γ*)opの射である
- grevはΓ*の射である
これを反転原理〈principle of reversal〉と呼ぶことにする（当たり前のことだが）。
Cが単なる圏のとき、圏の直和 C + Cop は簡単に作れて、反転作用素revは不動点を持たない対合オペレーターとなる。しかし、CがドクトリンDに属するとき、同じドクトリンの圏で、CとCopを埋め込める圏を作るのは簡単ではない。それが出来たとして、偏極ダブルと呼ぶ。「偏極」より「極性付き」がいいかも知れない。
偏極ダブルが作れないとしても、CとCopを別々に考えて、そのあいだをrevで結ぶことはできる。revがあれば何とかなる。
次は推論規則の定式化。推論規則は圏論的オペレーターとして定義する。推論規則は次の形で書く。
- Γ | providing 条件 α:: f1 ... fn => g
ガンマは文脈、すなわち圏のコンピュータッド。fiは射、すなわち証明。したがって、推論規則は証明達から証明を作り出す。以下に例：
- Γ | comp:: f:P->Q, g:Q->R => (f;g):P->R
縦書きすると：
Γ | f:P->Q g:Q->R
======================[comp]
(f;g):P->R証明も縦書きすると：
Γ
P Q
---- ----
f↓ g↓
---- ----
Q R
======================[comp]
P
------
(f;g)↓
--------
Rあるいは、
Γ
P Q
---[f] ----[g]
Q R
======================[comp]
P
------[f]
Q
------[g]
Rあるいは、
Γ
P Q
Q by [f] R by [g]
=========================[comp]
P
Q by [f]
R by[g]ともかくも、書き方なんてどうでもいいのだが、この"どうでもよさ”がなかなか伝わらない。
