リンデンバウム／タルスキー構成
骨格関係は、
DがCの外部骨格であることを次のように定義する。
- Dは骨格的圏。
- 埋め込み E:D→C がある。
- E(D) はCの内部骨格。
内部骨格と外部骨格の区別は微妙だが、一応区別しておく。
E:D→C が外部骨格の埋め込みのとき、P:C→D で、E*P = Id となるものを骨格射影と呼ぶ。EとPの組を、骨格EPペアと呼ぶ。
圏Cに対して、Cのワイヤーフレーム圏〈wireframe category〉Dを次のように定義する。
- |D| = |C|
- D(A, B) = {*} if C(A, B) が空でない
- D(A, B) = {} if C(A, B) が空
上記の定義で、Dはやせた箙〈thin quiver〉となる。単に箙なだけでなくて、前順序集合になる。前順序集合はやせた圏だから、Dも圏となる。
自明な射影 P:C→D が定義できて、Pは対象類上で恒等〈identity on objects〉な、充満関手である。Dはやせているが骨格的とは限らない。
Cのワイヤーフレーム圏をWF(C)と書く。WF:CAT→ThinCAT となる。WFは一種の脱圏化関手になっている。WF(C)は圏ではあるが、圏としての構造を一部捨てて、より簡単になっている。
WF(C)を（大きいかもしれない）前順序集合とみなして、順序集合化できる。こうして出来た順序集合は骨格的な圏なので、やせた圏の骨格化〈skeletonize〉と呼び、Skelと書く。
WF*Skel : CAT→SkelThinCAT をリンデンバウム／タルスキー構成〈Lindenbaum-Tarski construction〉と呼び、LTと書く。
集合と単射の圏をSetInjとする。カントール／ベルンシュタイン／シュレーダーの定理から、SetInjのリンデンバウム／タルスキー構成（の結果）LT(SetInj)は基数の圏と（圏同値）となる。
集合圏Setのリンデンバウム／タルスキー構成LT(Set)は二値ブール代数になる。
命題と証明からなる圏があるとき、そのリンデンバウム／タルスキー構成は、真理値〈truth value〉の圏となる。
参考：
- https://ncatlab.org/nlab/show/Lindenbaum-Tarski+algebra
- https://ncatlab.org/nlab/show/Heyting+algebra
デカルト閉圏CCCの僅かな拡張として、両付点〈dipointed〉CCCを定義する。
- Cはデカルト閉圏である。当然に終対象を持つ。
- Cは始対象を持つ。
終対象と始対象の両方を持つ圏が両付点圏であり、終対象と始対象が一致する圏が付点圏である。両付点圏で、終対象から始対象への射があれば、それは矛盾しているという。付点圏は矛盾している。
両付点CCCをDPCCCと略記する。DPCCCの始対象を⊥と書く。DPCCCでは、対象Aに対して、指数対象 ⊥A を作れるので、その対象を ¬A と書く。DPCCCでは、いちおう否定があるので、論理らしきことができる。原始論理と言っていいだろう。
やせたDPCCCは、ハイティング代数にはならないが、かなり近い構造になる。
