### changeset 792:5bee48f7c126

deduction theorem using category
author Shinji KONO Sun, 21 Apr 2019 18:11:14 +0900 376c07159acf f37f11e1b871 deductive.agda 1 files changed, 35 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
```--- a/deductive.agda	Sun Apr 21 17:43:01 2019 +0900
+++ b/deductive.agda	Sun Apr 21 18:11:14 2019 +0900
@@ -1,41 +1,51 @@
-module deductive (Atom : Set) where
+open import Level
+open import Category
+module deductive {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where

-- Deduction Theorem

--- positive logic ( deductive system based on graph )
-
-data Obj : Set where
-   ⊤ : Obj
-   atom : Atom → Obj
-   _∧_ : Obj → Obj → Obj
-   _<=_ : Obj → Obj → Obj
+-- positive logic

-data Arrow  : Obj → Obj → Set where
-   hom : (a b : Obj) → Arrow a b
-   id : (a : Obj ) → Arrow a a
-   _・_ : {a b c : Obj } → Arrow b c → Arrow a b → Arrow a c
-   ○ : {a : Obj } → Arrow a ⊤
-   π : {a b : Obj } → Arrow ( a ∧ b ) a
-   π' : {a b : Obj } → Arrow ( a ∧ b ) b
-   <_,_> : {a b c : Obj } → Arrow c a → Arrow c b → Arrow c (a ∧ b)
-   ε : {a b : Obj } → Arrow ((a <= b) ∧ b ) a
-   _* : {a b c : Obj } → Arrow (c ∧ b ) a → Arrow c ( a <= b )
+record PositiveLogic {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
+     field
+         ⊤ : Obj A
+         ○ : (a : Obj A ) → Hom A a ⊤
+         _∧_ : Obj A → Obj A → Obj A
+         <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)
+         π : {a b : Obj A } → Hom A (a ∧ b) a
+         π' : {a b : Obj A } → Hom A (a ∧ b) b
+         _<=_ : (a b : Obj A ) → Obj A
+         _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b)
+         ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a
+
+postulate L :  PositiveLogic A
+
+⊤ = PositiveLogic.⊤ L
+○ = PositiveLogic.○ L
+_∧_  = PositiveLogic._∧_  L
+<_,_> = PositiveLogic.<_,_> L
+π = PositiveLogic.π L
+π' = PositiveLogic.π' L
+_<=_ = PositiveLogic._<=_ L
+_* = PositiveLogic._* L
+ε = PositiveLogic.ε L
+_・_ = _[_o_] A

-- every proof b →  c with assumption a has following forms

-data  φ  {a : Obj} ( x : Arrow ⊤ a ) : {b c : Obj} → Arrow b c → Set where
-   i : {b c : Obj} → φ x ( hom b c )
+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 } { f : Arrow b c' } { g : Arrow b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x < f , g >
-   iv : {b c d : Obj } { f : Arrow d c } { g : Arrow b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g )
-   v : {b c' c'' : Obj } { f : Arrow (b ∧ c') c'' }  (ψ : φ x f )  → φ x ( f * )
+   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 * )

-α : {a b c : Obj } → Arrow (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
+α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
α = < π  ・ π   , < π'  ・ π  , π'  > >

-- genetate (a ∧ b) → c proof from  proof b →  c with assumption a

-kx∈a : {a b c : Obj } → ( x : Arrow ⊤ a ) → {z : Arrow b c } → ( y  : φ {a} x z ) → Arrow (a ∧ b) 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
kx∈a x {k} i = k ・ π'
kx∈a x ii = π
kx∈a x (iii ψ χ ) = < kx∈a x ψ  , kx∈a x χ  >```