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