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.