part of Logic implemented generically

examples/logic/LexTheory.gf

@@ -3,6 +3,9 @@ interface LexTheory = open Grammar in {
   oper
     assume_VS : VS ;
     case_N : N ;
+    contradiction_N : N ;
     have_V2 : V2 ;
+    hypothesis_N : N ;
+    ifthen_DConj : DConj ;
 
 }

examples/logic/LexTheoryEng.gf

@@ -2,6 +2,8 @@ instance LexTheoryEng of LexTheory = open GrammarEng,ParadigmsEng,IrregEng in {
   oper
     assume_VS = mkVS (regV "assume") ;
     case_N = regN "case" ;
+    contradiction_N = regN "contradiction" ;
     have_V2 = dirV2 have_V ;
-
+    hypothesis_N = mk2N "hypothesis" "hypotheses" ;
+    ifthen_DConj = {s1 = "if" ; s2 = "then" ; n = singular ; lock_DConj = <>} ;
 }

examples/logic/Logic.gf

@@ -0,0 +1,60 @@
+-- many-sorted predicate calculus
+-- AR 1999, revised 2001 and 2006
+
+abstract Logic = {
+
+cat 
+  Prop ;       -- proposition
+  Dom ;        -- domain of quantification
+  Elem Dom ;   -- individual element of a domain
+  Proof Prop ; -- proof of a proposition
+  Hypo Prop ;  -- hypothesis 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 ;
+ 
+  -- 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) -> 
+              (Hypo A -> Proof C) -> (Hypo B -> Proof C) -> Proof C ;
+  ImplI  : (A,B : Prop) -> (Hypo A -> Proof B) -> Proof (Impl A B) ;
+  ImplE  : (A,B : Prop) -> Proof (Impl A B) -> Proof A -> Proof B ;
+  NegI   : (A : Prop) -> (Hypo 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
+  Hypoth : (A : Prop) -> Hypo A -> Proof A ;
+
+  -- pronoun
+  Pron : (A : Dom) -> Elem A -> Elem A ;
+
+} ;

examples/logic/LogicEng.gf

@@ -0,0 +1,23 @@
+--# -path=.:mathematical:present:resource-1.0/api:prelude
+
+concrete LogicEng of Logic = LogicI with
+  (LexTheory = LexTheoryEng), 
+  (Prooftext = ProoftextEng),
+  (Grammar = GrammarEng), 
+  (Symbolic = SymbolicEng), 
+  (Symbol = SymbolEng), 
+  (Combinators = CombinatorsEng), 
+  (Constructors = ConstructorsEng), 
+  ;
+
+{-
+ImplI Abs Abs (\h -> DisjE Abs Abs Abs (DisjIr Abs Abs (Hypoth Abs h)) 
+(\x -> Hypoth Abs x) (\y -> Hypoth Abs y))
+
+assume that we have a contradiction . by the hypothesis we have a contradiction . 
+a fortiori we have a contradiction or we have a contradiction . 
+we have two cases. assume that we have a contradiction . 
+by the hypothesis we have a contradiction . assume that we have a contradiction . 
+by the hypothesis we have a contradiction . therefore we have a contradiction . 
+therefore if we have a contradiction then we have a contradiction .
+-}

examples/logic/LogicI.gf

@@ -0,0 +1,44 @@
+incomplete concrete LogicI of Logic = 
+  open 
+    LexTheory,
+    Prooftext, 
+    Grammar, 
+    Constructors, 
+    Combinators 
+  in {
+
+lincat 
+  Prop  = Prooftext.Prop ;
+  Proof = Prooftext.Proof ;
+  Dom   = Typ ;
+  Elem  = Object ;
+  Hypo  = Label ;
+  Text  = Section ;
+
+lin
+  Disj A B = coord or_Conj A B ;
+  Impl A B = coord ifthen_DConj A B ;
+
+  Abs = mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ;
+
+  DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ;
+  DisjIr A B b = proof b (proof afortiori (coord or_Conj A B)) ;
+
+  DisjE A B C c b1 b2 =
+    appendText
+      c 
+      (appendText
+        (appendText
+           (cases (mkNum n2)) 
+           (proofs 
+             (appendText (assumption A) b1)
+             (appendText (assumption B) b2)))
+        (proof therefore C)) ;
+
+  ImplI A B b = 
+    proof (assumption A) (appendText b (proof therefore (coord ifthen_DConj A B))) ;
+
+  Hypoth A h = proof hypothesis A ;
+
+
+}

examples/logic/Prooftext.gf

@@ -0,0 +1,79 @@
+interface Prooftext = open 
+  Grammar, 
+  LexTheory,
+  Symbolic,
+  Symbol, 
+  (C=ConstructX),
+  Constructors, 
+  Combinators 
+  in {
+
+oper
+  Chapter  = Text ;
+  Section  = Text ;
+  Sections = Text ;
+  Decl     = Text ;
+  Decls    = Text ;
+  Prop     = S ;
+  Branching= S ;
+  Proof    = Text ;
+  Proofs   = Text ;
+  Typ      = CN ;
+  Object   = NP ;
+  Label    = NP ;
+  Adverb   = PConj ;
+  Ref      = NP ;
+  Refs     = [NP] ;
+  Number   = Num ;
+
+  chapter : Label -> Sections -> Chapter 
+    = \title,jments -> 
+        appendText (mkText (mkPhr (mkUtt title)) TEmpty) jments ;
+
+  definition : Decls -> Object -> Object -> Section 
+    = \decl,a,b -> 
+        appendText decl (mkUtt (mkS (pred b a))) ;
+
+  assumption : Prop -> Decl 
+    = \p -> 
+        mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS p)))) TEmpty ;
+
+  declaration : Object -> Typ -> Decl
+    = \a,ty ->
+        mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS (mkS (pred ty a)))))) TEmpty ;
+
+  proof = overload {
+    proof : Prop -> Proof 
+      = \p -> mkText (mkPhr p) TEmpty ;
+    proof : Adverb -> Prop -> Proof
+      = \a,p -> mkText (mkPhr a (mkUtt p) NoVoc) TEmpty ;
+    proof : Decl -> Proof
+      = \d -> d ;
+    proof : Proof -> Proof -> Proof
+      = \p,q -> appendText p q ;
+    proof : Branching -> Proofs -> Proof
+      = \b,ps -> mkText (mkPhr b) ps
+    } ;
+
+  proofs : Proof -> Proof -> Proofs 
+    = appendText ;
+
+  cases : Num -> Branching 
+    = \nu -> 
+        mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet nu) case_N)) ;
+
+  by : Ref -> Adverb 
+    = \h -> mkAdv by8means_Prep h ;
+  therefore : Adverb
+    = therefore_PConj ;
+  afortiori : Adverb
+    = C.mkPConj ["a fortiori"] ;
+  hypothesis : Adverb
+    = mkAdv by8means_Prep (mkNP (mkDet DefArt) hypothesis_N) ;
+
+  ref : Label -> Ref
+    = \h -> h ;
+  refs : Refs -> Ref
+    = \rs -> mkNP and_Conj rs ;
+
+}

examples/logic/ProoftextEng.gf

@@ -0,0 +1,12 @@
+--# -path=.:mathematical:present:resource-1.0/api:prelude
+
+instance ProoftextEng of Prooftext = open 
+  LexTheoryEng, 
+  GrammarEng, 
+  SymbolicEng, 
+  SymbolEng, 
+  (C=ConstructX),
+  CombinatorsEng, 
+  ConstructorsEng in {
+  }
+  ;