|
Logic & Semantics |
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.