On the formal unprovability of some provable properties of numbers

 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.