1) Motivation
      a) Traditional Logic: A success BUT ...
      b) first order logic - minimal so necessary
         claim: if 'contextualized' it is sufficient
         no longer outside the first order vision
           Logicians: Intuitionistic, Pi-1-1 ...
           AI: Model, Temporal, direct, RDF, ...
      c) Hilbert's Program
         Hilbert - Reductionist
         NEW - mutual recursions + model
              practical - build a mind? - heads are finite
      d) history - later 
         Building a program for recording proofs
         You can't expect a program if find a proof if you can't even tell it the proof JMC
         I tried this here is what I found
           Formalize
             Arithmetic
               Induction is a schema
             Set Theory 
               Early Axiomatizations
                 No finite set of axions (needs meta theaory immediately
               SO Godel-Berney (?)
                 Needed many sorts
                 BUT sets were Classes SO Wang Many Sorts were NOT usable
                 So see early FOL sort theory
             Mendleson
             Group Theory
               a subgroup is mot mentionable in the elementary theory of groups
               how do we describe jumping between ele ns non-ele theories
             Hand in math homework
               Intersection of Bounded nested closed intervals is not eembty
               ? why is the bondedness criteria necessary?
                  usually answered by giving a counter example 
                  NOT a the proof of the existence of a counterecanple 
                  SO mentioning elements of a model are necessary
                  so simulation structure
               Wilson' theorem
                 The usual proof uses the igeon hole problem
                    to solve ele arith problem
                    of course the IS an elementary proof (ever seen it?)
                 reasoning on the side
               What are disgrams used in Geometry Proofs.
             Wht 

           Needed many sorts
             and representations
           meeded context
           needed formal metatheory
           mukltiple contexts
                          
      e) Strategy: replace infinite notions with finite data structures