X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fexamples%2Fexp_math%2FL.hln;h=28f3bff2399b454d33190efce93339f85bc1a063;hb=4c157ac5c58f34fffc98289c2d2e71032d584a83;hp=fbcf44adf5b933cc0a484f733a5f12099aa3aa07;hpb=28430d599505ac26b51e4887e5196d9b380c898a;p=helm.git

diff --git a/helm/software/lambda-delta/examples/exp_math/L.hln b/helm/software/lambda-delta/examples/exp_math/L.hln
index fbcf44adf..28f3bff23 100644
--- a/helm/software/lambda-delta/examples/exp_math/L.hln
+++ b/helm/software/lambda-delta/examples/exp_math/L.hln
@@ -1,8 +1,8 @@
-\graph Z3
+\require preamble
 
-\sorts Prop, Set, Term
+\* Intuitionistic Predicate Logic with Equality *\
 
-\open syntax \* [1] 2.1. *\
+\open elements \* [1] 2.1. 2.2. *\
 
    \decl "logical false" False: *Prop
 
@@ -10,34 +10,31 @@
 
    \decl "logical disjunction" Or: *Prop => *Prop -> *Prop
 
-   \decl "logical implication" Imp: *Prop => *Prop -> *Prop
+\* implication and non-dependent abstraction are isomorphic *\
+   \def "logical implication" 
+      Imp = [p:*Prop, q:*Prop] p -> q : *Prop => *Prop -> *Prop
 
-   \decl "logical comprehension" All: [~:*Set->*Prop] *Prop
+   \decl "logical comprehension" All: (*Obj -> *Prop) -> *Prop
 
-   \decl "logical existence" Ex: [~:*Set->*Prop] *Prop
+   \decl "logical existence" Ex: (*Obj -> *Prop) -> *Prop
 
-   \decl "syntactical identity" Id: *Set => *Set -> *Prop
-
-   \decl "rule application" App: *Set => *Set => *Set -> *Prop
-
-   \decl "classification predicate" Cl: *Set -> *Prop
-
-   \decl "classification membership" Eta: *Set => *Set -> *Prop
-
-   \decl "object-to-term-coercion" T: *Set -> *Term
-
-   \decl "term application" At: *Term => *Term -> *Term
-
-   \decl "term-object equivalence" E: *Term => *Set -> *Prop
+   \decl "syntactical identity" Id: *Obj => *Obj -> *Prop
 
 \close
 
-\open non_logical_axioms
+\open abbreviations \* [1] 2.3. *\
+
+   \def "logical negation" 
+      Not = [p:*Prop] p -> False : *Prop -> *Prop
 
-   \ax e_refl: [x:*Set] E(T(x), x)
+   \def "logical equivalence"
+      Iff = [p:*Prop, q:*Prop] And(p -> q, q -> p) : *Prop => *Prop -> *Prop
 
-   \ax e_at_in: [f:*Set][x:*Set][y:*Set] App(f,x,y) -> E(At(T(f), T(x)), y) 
+   \def "logical strict existence"
+      EX = [p:*Obj->*Prop] Ex([x:*Obj] And(p(x), [y:*Obj] p(y) -> Id(x, y)))
+         : (*Obj -> *Prop) -> *Prop
 
-   \ax e_at_out: [f:*Set][x:*Set][y:*Set] E(At(T(f), T(x)), y) -> App(f,x,y) 
+   \def "negated syntactical identity"
+      NId = [x:*Obj, y:*Obj] Not(Id(x, y)) : *Obj => *Obj -> *Prop
 
 \close