On the formal unprovability of some provable properties of numbers

In Arithmetic one can prove theorems by many tools, which may go beyond the expressive power of Formal Number Theory, as ordinarily 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 developed 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.