Founding the newly structured GF2.0 cvs archive.

1 files changed, 82 insertions, 0 deletions

diff --git a/grammars/logic/Logic.gf b/grammars/logic/Logic.gf
new file mode 100644
index 000000000..334592946
--- /dev/null
+++ b/grammars/logic/Logic.gf
@@ -0,0 +1,82 @@
+-- many-sorted predicate calculus
+-- AR 1999, revised 2001
+
+abstract Logic = {
+
+flags startcat=Prop ; -- this is what you want to parse
+
+cat 
+  Prop ;       -- proposition
+  Dom ;        -- domain of quantification
+  Elem Dom ;   -- individual element of a domain
+  Proof Prop ; -- proof of a proposition
+  Text ;       -- theorem with proof etc. 
+
+fun 
+  -- texts
+  Statement : Prop -> Text ;
+  ThmWithProof : (A : Prop) -> Proof A -> Text ;
+  ThmWithTrivialProof : (A : Prop) -> Proof A -> Text ;
+
+  -- logically complex propositions
+  Disj : (A,B : Prop) -> Prop ;
+  Conj : (A,B : Prop) -> Prop ;
+  Impl : (A,B : Prop) -> Prop ;
+  Abs  : Prop ;
+  Neg  : Prop -> Prop ;
+
+  Univ  : (A : Dom) -> (Elem A -> Prop) -> Prop ;
+  Exist : (A : Dom) -> (Elem A -> Prop) -> Prop ;
+
+  -- progressive implication à la type theory
+  ImplP : (A : Prop) -> (Proof A -> Prop) -> Prop ;
+
+  -- inference rules
+  ConjI  : (A,B : Prop) -> Proof A -> Proof B -> Proof (Conj A B) ;
+  ConjEl : (A,B : Prop) -> Proof (Conj A B) -> Proof A ;
+  ConjEr : (A,B : Prop) -> Proof (Conj A B) -> Proof B ;
+  DisjIl : (A,B : Prop) -> Proof A -> Proof (Disj A B) ;
+  DisjIr : (A,B : Prop) -> Proof B -> Proof (Disj A B) ;
+  DisjE  : (A,B,C : Prop) -> Proof (Disj A B) -> 
+              (Proof A -> Proof C) -> (Proof B -> Proof C) -> Proof C ;
+  ImplI  : (A,B : Prop) -> (Proof A -> Proof B) -> Proof (Impl A B) ;
+  ImplE  : (A,B : Prop) -> Proof (Impl A B) -> Proof A -> Proof B ;
+  NegI   : (A : Prop) -> (Proof A -> Proof Abs) -> Proof (Neg A) ;
+  NegE   : (A : Prop) -> Proof (Neg A) -> Proof A -> Proof Abs ;
+  AbsE   : (C : Prop) -> Proof Abs -> Proof C ;
+
+  UnivI  : (A : Dom) -> (B : Elem A -> Prop) -> 
+              ((x : Elem A) -> Proof (B x)) -> Proof (Univ A B) ;
+  UnivE  : (A : Dom) -> (B : Elem A -> Prop) -> 
+              Proof (Univ A B) -> (a : Elem A) -> Proof (B a) ;
+  ExistI : (A : Dom) -> (B : Elem A -> Prop) -> 
+              (a : Elem A) -> Proof (B a) -> Proof (Exist A B) ;
+  ExistE : (A : Dom) -> (B : Elem A -> Prop) -> (C : Prop) -> 
+              Proof (Exist A B) -> ((x : Elem A) -> Proof (B x) -> Proof C) -> 
+              Proof C ;
+
+  -- use a hypothesis
+  Hypo : (A : Prop) -> Proof A -> Proof A ;
+
+  -- pronoun
+  Pron : (A : Dom) -> Elem A -> Elem A ;
+
+data
+  Proof = ConjI | DisjIl | DisjIr ;
+
+def 
+  -- proof normalization
+  ConjEl _ _ (ConjI _ _ a _) = a ;
+  ConjEr _ _ (ConjI _ _ _ b) = b ;
+  DisjE _ _ _ (DisjIl _ _ a) d _ = d a ;
+  DisjE _ _ _ (DisjIr _ _ b) _ e = e b ;
+  ImplE _ _ (ImplI _ _ b) a = b a ;
+  NegE _ (NegI _ b) a = b a ;
+  UnivE _ _ (UnivI _ _ b) a = b a ;
+  ExistE _ _ _ (ExistI _ _ a b) d = d a b ;
+
+  -- Hypo and Pron are identities
+  Hypo _ a = a ;
+  Pron _ a = a ;
+
+} ;