Arithmetic/make.ml

   1 prioritize_num();;
   2
   3 (* ------------------------------------------------------------------------- *)
   4 (* Some additional mathematical background.                                  *)
   5 (* ------------------------------------------------------------------------- *)
   6
   7 loadt "Library/rstc.ml";;
   8 loadt "Library/prime.ml";;
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* The basics of first order logic and our inference system.                 *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 loadt "Arithmetic/fol.ml";;
  15
  16 (* ------------------------------------------------------------------------- *)
  17 (* The incompleteness results.                                               *)
  18 (* ------------------------------------------------------------------------- *)
  19
  20 loadt "Arithmetic/definability.ml";;
  21 loadt "Arithmetic/tarski.ml";;
  22 loadt "Arithmetic/arithprov.ml";;
  23 loadt "Arithmetic/godel.ml";;
  24
  25 (* ------------------------------------------------------------------------- *)
  26 (* Sigma-1 completeness of Robinson arithmetic.                              *)
  27 (* ------------------------------------------------------------------------- *)
  28
  29 loadt "Arithmetic/derived.ml";;
  30 loadt "Arithmetic/sigmacomplete.ml";;