--- a/first-order.agda	Thu Aug 13 11:07:35 2020 +0900
+++ b/first-order.agda	Thu Aug 13 11:22:12 2020 +0900
@@ -43,6 +43,17 @@
      All    :  {x t : Term} → Var x → Statement t → Statement ( all x => t )
      Exist  :  {x t : Term} → Var x → Statement t → Statement ( ∃ x => t )
 
+  Model : ( {x : Term } → (px :  Pred x ) → Bool )
+       →  ( {p args : Term } → (px :  Pred p ) → Expr args  → Bool )
+       → {t : Term } → Statement t  → Bool
+  Model amap pmap (atom x) = amap x
+  Model amap pmap (predicate x x₁) = pmap x x₁
+  Model amap pmap (and s s₁) = Model amap pmap s  ∧ Model amap pmap s₁ 
+  Model amap pmap (or s s₁) = Model amap pmap s ∨ Model amap pmap s₁ 
+  Model amap pmap (not s) = Data.Bool.not (Model amap pmap s )
+  Model amap pmap (All x s) = {!!}
+  Model amap pmap (Exist x s) = {!!}
+
 data Kind : Set where
       pred : Kind
       const : Kind
@@ -73,27 +84,6 @@
       kall_ : (x y : Term ) → Kinds (all x => y ) conn
       kexit : (x y : Term ) → Kinds (∃ x => y ) conn
 
-kindOf : Term → Kind
-kindOf X = var
-kindOf Y = var
-kindOf Z = var
-kindOf a = const
-kindOf b = const
-kindOf c = const
-kindOf f = func
-kindOf g = func
-kindOf h = func
-kindOf p = pred
-kindOf q = pred
-kindOf r = pred
-kindOf (t ⟨ t₁ ⟩) = arg
-kindOf (t , t₁) = args
-kindOf (t /\ t₁) = conn
-kindOf (t \/ t₁) = conn
-kindOf (¬ t) = conn
-kindOf (all t => t₁) =  conn
-kindOf (∃ t => t₁) = conn
-
 Const : Term → Set
 Const x = Kinds x const
 
@@ -176,4 +166,4 @@
 ... | _ = nothing
 parse _ = nothing
 
-  ex2 = parse ex1
+ex2 = parse ex1