Giuseppe Longo

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.