Reflections on Concrete Incompleteness

-

English
23 Pages
Read an excerpt
Gain access to the library to view online
Learn more

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


Subjects

Informations

Published by
Reads 101
Language English
Report a problem
ReflectionsonConcreteIncompleteness?GiuseppeLongoLaboratoired’InformatiqueCNRSE´coleNormaleSupe´rieure,ParisetCrea,E´colePolytechniquehttp://www.di.ens.fr/users/longoAbstract.Howdoweprovetrue,butunprovablepropositions?Go¨delproducedastatementwhoseundecidabilityderivesfromits“adhoc”construction.Concreteormathematicalincompletenessresults,instead,areinterestingunprovablestatementsofFormalArithmetic.Wepointoutwhereexactlylaystheunprovabilityalongtheordinarymathemat-icalproofsoftwo(very)interestingformallyunprovablepropositions,Kruskal-FriedmantheoremontreesandGirard’sNormalizationTheo-reminTypeTheory.Theirvalidityisbasedonrobustcognitiveperfor-mances,whichgroundmathematicsonourrelationtospaceandtime,suchassymmetriesandorder,oronthegeneralityofHerbrandsnotionofprototypeproof.Introduction:somehistory,somephilosophySupposethatyouwereaskedtogivetheresultofthesumofthefirstnintegers.Thereexistmanyproofsofthissimplefact(see[Nelsen93]forthisandmoreexamples),animmediateone(allegedly(re-)inventedbyGaussattheageof7orso)isthefollowing:12...nn(n-1)...1(n+1)(n+1)...(n+1)whichgivesΣ1ni=n(n+1)/2.Clearly,theproofisnotbyinduction.Givenn,auniformargumentispro-posed,whichworksforanyintegern.FollowingHerbrand,wewillcallproto-typethiskindofproof.Ofcourse,oncetheformulaisknown,itisveryeasytoproveitbyinduction,aswell.But,onemustknowtheformula,or,moregener-ally,the“inductionload”.Anon-obviousissueinmathematics,asweallknow(atthisregards,wewilldiscussbelowthecaseoftheNormalizationTheoremsinTypeTheory).?InPhilosophiaMathematica,19(3):255-280,OxfordU.P.jounal,2011.ApreliminaryversionofthispaperwasanInvitedLecture“OntheproofsofsomeformallyunprovablepropositionsandPrototypeProofsinTypeTheory”attheconferenceonTypesforProofsandPrograms,Durham,(GB),publishedinLNCSvol.2277(Callaghanetal.eds),pp.160-180,Springer,2002.
Let’snowspeculateonthepossible“cognitive”pathwhich“bringsto”(andgivescertainty!)tothisproof.Thereadercansurelysee,inhismentalspaces,the“numberline”asadiscretesequence,thatisthewell-orderedsequenceofintegernumbers.Theyarethere,oneaftertheother,inincreasingorder:youmayseeitonastraightline,itmayoscillate,butitshouldbe,foryou,fromlefttoright(isn’tit?pleasecheck...andgiveupdoingmathematics,ifyoudonotseethenumberline;see[Dehaene98]forsomedataaboutit).Wheninventingaprooflikethis,onemustfirstseeorputtheorderedsequenceonpaperandthenhavethementalcourageto...reverseit,byamirrorsymmetry.Noinduction,justtheorderanditsinverse,asymmetry,andtheproofworksforanyn,aperfectlyrigorousproof.Considernowanon-emptysubsetinyournumberline.Youcansurely“see”thatthissethasaleastelement.Lookandsee:ifasetofintegernumbersonyournumberlinecontainsanelement,thereisaleastoneamongthefinitelymanyprecedingit,evenifyoumaynotknowwhichone.The“observation”imposesitselftoanypersonwithsomemathematicaltraining:itisthe(well-)orderingofthenumberline,asgeometricevidence,averyrobustone(seebelowformoreonthiscommuncognitiveperformanceinmathematics).Moreover,onedoesnotneedtoknowifandhowthesubseteventuallygoestoinfinity:ifithasonepointsomewhere(thesetisnotempty),thisisatsomefinitepointand,then,thereisasmalleronewhichistheleastofthe“given”subset.Intheconclusion,wewillcallthis,a“geometricjudgement”.Inthefewlinesabove,wehintedtoanunderstandingoftheorderingofnumberswithreferencetoamentalconstruction,inspace(ortime).Fregewouldhavecalledthisapproach“psychologism”(Herbart’sstyle,accordingtohis1884book).Poincare´insteadcouldbeareferenceforthisviewoncertaintyandmeaningofinductionasgroundedonintuition,possiblyofspace.InBrouwer’sfoundationalproposalaswell,themathematician’sintuitionofthesequenceofnaturalnumbers,whichfoundsMathematics,reliesonaphenomenalexperience;however,thisexperienceshouldbegroundedonthe“discretefallingapartoftime”,as“twoness”(“thefallingapartofalifemomentintotwodistinctthings,onewhichgiveswaytotheother,butisretainedbymemory”,[Brouwer48]).Thus,“Brouwer’snumberline”originatesfrom(adiscreteformof)phenomenaltimeandinductionderivesmeaningandcertaintyfromit.Intuitionoforderinginspaceortime,actuallyofboth,contributestoestab-lishthenumberline,asaninvariantoftheseactiveexperiences:formalinduc-tionfollowsfrom,itdoesn’tfoundthisintuition.ThisismyunderstandingofPoincare´’sandBrouwer’sphilosophy,bycombiningboththough,astheinvariantmaybeconstructedonlyonthebasisofmanyindependenthumanconstitutiveactivitiesinspaceandtime.Themanifoldedphenomenalexperiencesyieldtheindependence,asconceptualinvariant,ofthemathematicalstructure.Byrecentscientificevidence(see[Dehaene98],[LongoVia10]),weseemtouseextensively,inreasoningandcomputations,the“intuitive”numberline;theseneuropsycho-logicalinvestigationsareremarkablefacts,sincetheytakeusbeyondthe“intro-spection”thatthefoundingfathersusedastheonlywaytogroundmathematics