X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fexamples%2Fexp_math%2FT0.hln;fp=helm%2Fsoftware%2Flambda-delta%2Fexamples%2Fexp_math%2FT0.hln;h=0000000000000000000000000000000000000000;hb=95872555aaa040a22ad2d93cb1278f79e20da70c;hp=8321246c649a413a74e7a8401b24c7c8c39a611a;hpb=4025c3f5b36025380dcad84bb7a97045d08652f6;p=helm.git

diff --git a/helm/software/lambda-delta/examples/exp_math/T0.hln b/helm/software/lambda-delta/examples/exp_math/T0.hln
deleted file mode 100644
index 8321246c6..000000000
--- a/helm/software/lambda-delta/examples/exp_math/T0.hln
+++ /dev/null
@@ -1,88 +0,0 @@
-\require L
-
-\* Feferman's system T0 *\
-
-\open elements \* [1] 2.1. 2.2. 2.4. *\
-
-   \decl "rule application" App: *Obj => *Obj => *Obj -> *Prop
-
-   \decl "classification predicate" Cl: *Obj -> *Prop
-
-   \decl "classification membership" Eta: *Obj => *Obj -> *Prop
-
-\* we must make an explicit coercion from *Obj to *Term *\
-   \decl "object-to-term-coercion" T: *Obj -> *Term
-
-   \decl "term application" At: *Term => *Term -> *Term
-
-   \decl "term-object equivalence" E: *Term => *Obj -> *Prop
-
-\close
-
-\open logical_abbreviations \* [1] 2.3. 2.5. *\
-
-   \def "logical comprehension restricted to classifications"
-      CAll = [q:*Obj->*Prop] [x:*Obj] Cl(x) -> q(x)      
-           : (*Obj -> *Prop) -> *Prop
-
-   \def "logical existence restricted to classifications"
-      CEx = [q:*Obj->*Prop] Ex([x:*Obj] And(Cl(x), q(x)))      
-          : (*Obj -> *Prop) -> *Prop
-
-   \def "logical comprehension restricted to a classification"
-      EAll = [a:*Obj, q:*Obj->*Prop] [x:*Obj] Eta(x, a) -> q(x)      
-           : *Obj => (*Obj -> *Prop) -> *Prop
-
-   \def "logical existence restricted to a classification"
-      EEx = [a:*Obj, q:*Obj->*Prop] Ex([x:*Obj] And(Eta(x, a), q(x)))      
-          : *Obj => (*Obj -> *Prop) -> *Prop
-
-\close
-
-\open non_logical_abbreviations \* [1] 2.4. 2.7 *\
-
-   \def "object application"
-      OAt = [f:*Obj, x:*Obj] At(T(f), T(x)) : *Obj => *Obj -> *Term
-
-   \def "convergence of a term to an object"
-      Conv = [t:*Term] EX([y:*Obj] E(t, y)) : *Term -> *Prop
-
-   \def "term-term equivalence"
-      Eq = [t1:*Term, t2:*Term] [y:*Obj] Iff(E(t1, y), E(t2, y))
-         : *Term => *Term -> *Prop
-
-   \def "classification membership of a term"
-      TEta = [t:*Term, a:*Obj] EEx(a, [y:*Obj] E(t, y))
-           : *Term => *Obj -> *Prop
-
-   \def "operation (rule with inhabited domain)"
-      Op = [f:*Obj] Ex([x:*Obj] Conv(OAt(f, x))) : *Obj -> *Prop
-
-   \def "classification inclusion"
-      ESub = [a1:*Obj, a2:*Obj] EAll(a1, [x:*Obj] Eta(x, a2))
-           : *Obj => *Obj -> *Prop
-
-    \def "classification morphism"
-      ETo = [f:*Obj, a:*Obj, b:*Obj] EAll(a, [x:*Obj] TEta(OAt(f, x), b))
-          : *Obj => *Obj => *Obj -> *Prop
-
-\close
-
-\open non_logical_axioms \* [1] 2.4. 3.2 *\
-
-\* we axiomatize E because *Term is not inductively generated *\
-   \ax e_refl: [y:*Obj] E(T(y), y)
-
-   \ax e_at_in: [t1:*Term][t2:*Term][f:*Obj][x:*Obj][y:*Obj] 
-                E(t1, f) -> E(t2, x) -> App(f, x, y) -> E(At(t1, t2), y) 
-\*
-   \ax e_at_out: [f:*Obj][x:*Obj][y:*Obj] E(At(T(f), T(x)), y) -> App(f,x,y) 
-*\
-   \ax "I (i)" id_dec: [x:*Obj][y:*Obj] Or(Id(x, y), NId(x, y))
-   
-   \ax "I (ii)" at_mono: [f:*Obj][x:*Obj][y1:*Obj][y2:*Obj]
-                         E(OAt(f, x), y1) -> E(OAt(f, x), y2) -> Id(y1, y2)
-
-   \ax "I (iii)" eta_cl: [x:*Obj][a:*Obj] Eta(x, a) -> Cl(a)
-
-\close