Reflections on Concrete Incompleteness

Giuseppe Longo

Description

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.

• herbrand's prototype proofs


• cognitive perfor- mances


• prototype proof


• purely formal


• formal


• negative results


• must provide


• poincare

Sujets

• École polytechnique
• Formal
• Negative result
• Poincaré

Informations

• Publié par: chaeh
• Nombre de lectures: 101
• Langue: English

Extrait

ReflectionsonConcreteIncompleteness ? GiuseppeLongo Laboratoired’Informatique CNRS–E ´ coleNormaleSupe´rieure,Paris etCrea,E ´ colePolytechnique http://www.di.ens.fr/users/longo Abstract.Howdoweprovetrue,butunprovablepropositions?Go¨del producedastatementwhoseundecidabilityderivesfromits“adhoc” construction.Concreteormathematicalincompletenessresults,instead, areinterestingunprovablestatementsofFormalArithmetic.Wepoint outwhereexactlylaystheunprovabilityalongtheordinarymathemat- icalproofsoftwo(very)interestingformallyunprovablepropositions, Kruskal-FriedmantheoremontreesandGirard’sNormalizationTheo- reminTypeTheory.Theirvalidityisbasedonrobustcognitiveperfor- mances,whichgroundmathematicsonourrelationtospaceandtime, suchassymmetriesandorder,oronthegeneralityofHerbrandsnotion ofprototypeproof. Introduction:somehistory,somephilosophy Supposethatyouwereaskedtogivetheresultofthesumofthefirstnintegers. Thereexistmanyproofsofthissimplefact(see[Nelsen93]forthisandmore examples),animmediateone(allegedly(re-)inventedbyGaussattheageof7 orso)isthefollowing: 12...n n(n-1)...1 (n+1)(n+1)...(n+1) whichgivesΣ 1 n i=n(n+1)/2. Clearly,theproofisnotbyinduction.Givenn,auniformargumentispro- posed,whichworksforanyintegern.FollowingHerbrand,wewillcallproto- typethiskindofproof.Ofcourse,oncetheformulaisknown,itisveryeasyto proveitbyinduction,aswell.But,onemustknowtheformula,or,moregener- ally,the“inductionload”.Anon-obviousissueinmathematics,asweallknow (atthisregards,wewilldiscussbelowthecaseoftheNormalizationTheorems inTypeTheory). ? InPhilosophiaMathematica,19(3):255-280,OxfordU.P.jounal,2011. ApreliminaryversionofthispaperwasanInvitedLecture“Ontheproofsofsome formallyunprovablepropositionsandPrototypeProofsinTypeTheory”atthe conferenceonTypesforProofsandPrograms,Durham,(GB),publishedin LNCSvol.2277(Callaghanetal.eds),pp.160-180,Springer,2002.

Let’snowspeculateonthepossible“cognitive”pathwhich“bringsto”(and givescertainty!)tothisproof.Thereadercansurelysee,inhismentalspaces, the“numberline”asadiscretesequence,thatisthewell-orderedsequenceof integernumbers.Theyarethere,oneaftertheother,inincreasingorder:you mayseeitonastraightline,itmayoscillate,butitshouldbe,foryou,fromleft toright(isn’tit?pleasecheck...andgiveupdoingmathematics,ifyoudonot seethenumberline;see[Dehaene98]forsomedataaboutit).Wheninventinga prooflikethis,onemustfirstseeorputtheorderedsequenceonpaperandthen havethementalcourageto...reverseit,byamirrorsymmetry.Noinduction, justtheorderanditsinverse,asymmetry,andtheproofworksforanyn,a perfectlyrigorousproof. Considernowanon-emptysubsetinyournumberline.Youcansurely“see” thatthissethasaleastelement.Lookandsee:ifasetofintegernumbersonyour numberlinecontainsanelement,thereisaleastoneamongthefinitelymany precedingit,evenifyoumaynotknowwhichone.The“observation”imposes itselftoanypersonwithsomemathematicaltraining:itisthe(well-)orderingof thenumberline,asgeometricevidence,averyrobustone(seebelowformore onthiscommuncognitiveperformanceinmathematics).Moreover,onedoesnot needtoknowifandhowthesubseteventuallygoestoinfinity:ifithasonepoint somewhere(thesetisnotempty),thisisatsomefinitepointand,then,thereis asmalleronewhichistheleastofthe“given”subset.Intheconclusion,wewill callthis,a“geometricjudgement”. Inthefewlinesabove,wehintedtoanunderstandingoftheorderingof numberswithreferencetoamentalconstruction,inspace(ortime).Fregewould havecalledthisapproach“psychologism”(Herbart’sstyle,accordingtohis1884 book).Poincare´insteadcouldbeareferenceforthisviewoncertaintyand meaningofinductionasgroundedonintuition,possiblyofspace.InBrouwer’s foundationalproposalaswell,themathematician’sintuitionofthesequenceof naturalnumbers,whichfoundsMathematics,reliesonaphenomenalexperience; however,thisexperienceshouldbegroundedonthe“discretefallingapartof time”,as“twoness”(“thefallingapartofalifemomentintotwodistinctthings, onewhichgiveswaytotheother,butisretainedbymemory”,[Brouwer48]). Thus,“Brouwer’snumberline”originatesfrom(adiscreteformof)phenomenal timeandinductionderivesmeaningandcertaintyfromit. Intuitionoforderinginspaceortime,actuallyofboth,contributestoestab- lishthenumberline,asaninvariantoftheseactiveexperiences:formalinduc- tionfollowsfrom,itdoesn’tfoundthisintuition.Thisismyunderstandingof Poincare´’sandBrouwer’sphilosophy,bycombiningboththough,astheinvariant maybeconstructedonlyonthebasisofmanyindependenthumanconstitutive activitiesinspaceandtime.Themanifoldedphenomenalexperiencesyieldthe independence,asconceptualinvariant,ofthemathematicalstructure.Byrecent scientificevidence(see[Dehaene98],[LongoVia10]),weseemtouseextensively, inreasoningandcomputations,the“intuitive”numberline;theseneuropsycho- logicalinvestigationsareremarkablefacts,sincetheytakeusbeyondthe“intro- spection”thatthefoundingfathersusedastheonlywaytogroundmathematics