定理記述 2

定理記述 - 檜山正幸のキマイラ飼育記 メモ編の続き。

少し変える。

theorem 定理の名前
 import モジュール1, モジュール2
 for 宣言1, 宣言2
 given 命題1, 命題2
 ensures 命題
 begin
   証明
 end
end

proofという語は避けた。

圏論	論理
始対象	False
終対象	True
対象	proposition
射	theorem
オペレーター	procedure

圏論	基本構成素	複合体
対象	predicate	proposition
射	axiom	theorem
オペレーター	rule	procedure

圏論	論理
対象に作用するオペレーター	connective
対象を移動するオペレーター	quantifier
射に作用するオペレーター	procedure

1. constant（特殊なconnective）: True, False
2. connective: ∧, ∨, ⊃, ¬
3. quantifier: ∀, ∃
4. term: インデックス圏のベースの射＝ベース射
5. rule: カリー化、デカルトペアリング、デカルト余ペアリング

構成法

1. propositionを作るには、prediateに対してconnective（constant含む）を使う。
2. さらに、quantifierを作用させてpropositionを作る。
3. termでpropositionの舞台を移動する。
4. axiomをもとに、定理結合、手煎りたプリング、procedure適用などでtheoremを作る。
5. ruleをもとに、手続き結合と手続きタプリングなどでprocedureを作る。

ベース圏と各ベース対象（domain of discourse＝議論領域＝論域）ごとの命題・定理（証明）圏をハッキリと意識する必要がある。

インデックス付き圏のベース圏（インデクシング圏）は論域の圏から指標（型文脈）の圏に拡張して、各指標の上に乗っかる命題と定理（＝証明）の圏を論理圏と呼ぶことにしよう。

指標Σの論理圏をLogic[Σ]とする。|Logic[Σ]| = Sen[Σ] としてインスティチューションと関係が付く。充足関係を |Mod[Σ]|×Sen[Σ]→{true, false} から拡張して、Mod[Σ]×Logic[Σ]→Ω としたい。Ωは、Logic[1]から作った真理値の圏。