Deduction Theorem

昨日のOSCではまっていた奴です。CCC やってたはずなんだが、その直前に置いてあって、短い割に良くわからない。簡単そうだし。

えーと、

　　a を仮定して、b → c が証明できたなら、(a ∧ b) → c が a の仮定抜きで証明できる

ですね。当たり前っぽいけど、b → c のどこで仮定を使っているかがわからない。b → c の証明は推論の積み重ねなので、それを解析する感じ。

Intorduction to Higher order Categorical Logic には Positive logic の場合の証明が載っていて、五つの場合があるとか書いてある。

その場合分けにそって、

　　a を仮定した b → c の証明 φ(x) つまり、φ : a → (b → c)

を分解していく感じらしい。で、φ(x) から (a ∧ b) → c の証明を返す関数 kx∈a を作れば良いんですが、ぜんぜんできなくて。

　　kx∈a : {a b c : Obj A } → ( x : Hom A ⊤ a ) → ( φ {a} x z ) → Hom A (a ∧ b) c

と

　　data　φ　{a : Obj A } ( x : Hom A ⊤ a ) : Set ( c₁　⊔　c₂ )

かと思ったんですが、まったくできず... そうだよね。これだと、分解していく式がない。、b → c　の形をした式みたいなのでないと。

結果的には、

　　data　φ　{a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁　⊔　c₂ )

　　kx∈a : {a b c : Obj A } → ( x : Hom A ⊤ a ) → {z : Hom A b c } → ( y　: φ {a} x z ) → Hom A (a ∧ b) c

でできました。

要するに、場合分けの関数を書く時には、

　 data 関数　入力 : 出力 → Set

という風に書けば良かったらしい。なるほど。

これで、ほぼ教科書の式通りに証明できました。

　　data　φ　{a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁　⊔　c₂ ) where
　　　 i : {b c : Obj A} {k : Hom A b c } → φ x k
　　　 ii : φ x {⊤} {a} x
　　　 iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x < f , g >
　　　 iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g )
　　　 v : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' }　(ψ : φ x f )　→ φ x ( f * )

　　kx∈a : {a b c : Obj A } → ( x : Hom A ⊤ a ) → {z : Hom A b c } → ( y　: φ {a} x z ) → Hom A (a ∧ b) c
　　kx∈a x {k} i = k ・ π'
　　kx∈a x ii = π
　　kx∈a x (iii ψ χ ) = < kx∈a x ψ　, kx∈a x χ　>
　　kx∈a x (iv ψ χ ) = kx∈a x ψ　・ < π , kx∈a x χ　>
　　kx∈a x (v ψ ) = ( kx∈a x ψ　・ α ) *

超短い。

教科書通りにできるのは、書いてる先生の頭が Agda だからだろうと思います。というか、Agda が圏論に合わせて作られているわけだな。