# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1555836181 -32400
# Node ID 376c07159acf6a8e6d78944dd9ea66c5c9fa9495
# Parent  1e7319868d77c53c62c691fa6c4ea6c62ff6577c
deduction theorem

diff -r 1e7319868d77 -r 376c07159acf deductive.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/deductive.agda	Sun Apr 21 17:43:01 2019 +0900
@@ -0,0 +1,43 @@
+module deductive (Atom : Set) where
+
+-- Deduction Theorem
+
+-- positive logic ( deductive system based on graph ) 
+
+data Obj : Set where
+   ⊤ : Obj 
+   atom : Atom → Obj
+   _∧_ : Obj → Obj → Obj
+   _<=_ : Obj → Obj → Obj
+
+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 )
+
+-- 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 )
+   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 * )
+
+α : {a b c : Obj } → Arrow (( 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 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 ψ  ・ α ) *