Título: On the formal unprovability of some provable properties of
                numbers 
        Palestrante: Giuseppe Longo
                     Laboratoire et Departement d'Informatique
                     CNRS et Ecole Normale Superieure
                     et CREA, Ecole Polytechnique (Paris)
 
        Resumo: In Arithmetic one can prove theorems by many tools, which 
                may go beyond the expressive power of Formal Number Theory, as
                ordinarely defined. The key issue is the essential
                incompleteness of I order induction as well as the limits of
                the distinction "theory/metatheory" in proofs. Prototype
                proofs, a rigourous notion in Type Theory, allow first to
                focus informally on the expressiveness of induction.  A close
                analysis can then be developped concerning the unprovability
                of various true propositons (normalization, some finite forms
                of theorems on trees, due to Friedman ...): the proofs of
                their truth help to single-out the (un-)formalizable, but
                perfectly accessible, fragments. 

                The reference paper for this would be (downloadable):

                Giuseppe Longo. On the proofs of some formally unprovable
                propositions and Prototype Proofs in Type Theory. Invited
                Lecture,Types for Proofs and Programs, Durham, (GB); Lecture
                Notes in Computer Science, vol 2277 (Callaghan et al. eds),
                pp. 160 - 180, Springer, 2002.