Reflections on Concrete Incompleteness
23
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe en t'inscrivant gratuitement
Découvre YouScribe en t'inscrivant gratuitement
23
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Niveau: Supérieur
Reflections on Concrete Incompleteness? Giuseppe Longo Laboratoire d'Informatique CNRS – Ecole Normale Superieure, Paris et Crea, Ecole Polytechnique Abstract. How do we prove true, but unprovable propositions? Godel produced a statement whose undecidability derives from its “ad hoc” construction. Concrete or mathematical incompleteness results, instead, are interesting unprovable statements of Formal Arithmetic. We point out where exactly lays the unprovability along the ordinary mathemat- ical proofs of two (very) interesting formally unprovable propositions, Kruskal-Friedman theorem on trees and Girard's Normalization Theo- rem in Type Theory. Their validity is based on robust cognitive perfor- mances, which ground mathematics on our relation to space and time, such as symmetries and order, or on the generality of Herbrands notion of prototype proof. Introduction: some history, some philosophy Suppose that you were asked to give the result of the sum of the first n integers. There exist many proofs of this simple fact (see [Nelsen93] for this and more examples), an immediate one (allegedly (re-)invented by Gauss at the age of 7 or so) is the following: 1 2 ... n n (n-1) ... 1 (n+1) (n+1) ... (n+1) which gives ?n1 i = n(n+ 1)/2.
Voir
Reflections on Concrete Incompleteness? Giuseppe Longo Laboratoire d'Informatique CNRS – Ecole Normale Superieure, Paris et Crea, Ecole Polytechnique Abstract. How do we prove true, but unprovable propositions? Godel produced a statement whose undecidability derives from its “ad hoc” construction. Concrete or mathematical incompleteness results, instead, are interesting unprovable statements of Formal Arithmetic. We point out where exactly lays the unprovability along the ordinary mathemat- ical proofs of two (very) interesting formally unprovable propositions, Kruskal-Friedman theorem on trees and Girard's Normalization Theo- rem in Type Theory. Their validity is based on robust cognitive perfor- mances, which ground mathematics on our relation to space and time, such as symmetries and order, or on the generality of Herbrands notion of prototype proof. Introduction: some history, some philosophy Suppose that you were asked to give the result of the sum of the first n integers. There exist many proofs of this simple fact (see [Nelsen93] for this and more examples), an immediate one (allegedly (re-)invented by Gauss at the age of 7 or so) is the following: 1 2 ... n n (n-1) ... 1 (n+1) (n+1) ... (n+1) which gives ?n1 i = n(n+ 1)/2.
- herbrand's prototype proofs
- cognitive perfor- mances
- prototype proof
- purely formal
- formal
- negative results
- must provide
- poincare
