b"\n_START_ARTICLE_\nTeoria de la demostraci\xc3\xb3\n_START_PARAGRAPH_\nLa teoria de la demostraci\xc3\xb3 \xc3\xa9s una branca de la l\xc3\xb2gica matem\xc3\xa0tica que tracta amb l'estructura de les demostracions matem\xc3\xa0tiques i la pot\xc3\xa8ncia expressiva d'un determinat conjunt d'axiomes matem\xc3\xa0tics.\n_START_SECTION_\nTipus de demostracions\n_START_PARAGRAPH_\nLes demostracions matem\xc3\xa0tiques que sovint es troben en els llibres contenen raonaments expressats en un llenguatge informal. Tamb\xc3\xa9 la pr\xc3\xa0ctica ordin\xc3\xa0ria dels matem\xc3\xa0tics es basa en intu\xc3\xafcions que tracten de capturar l'ess\xc3\xa8ncia d'un conjunt d'objectes matem\xc3\xa0tics (aquestes demostracions sovint requereixen creativitat i enginy per ser creades). En canvi hi ha un altre tipus de demostracions purament formals que consisteixen en l'aplicaci\xc3\xb3 reiterada d'un conjunt d'axiomes i regles de deducci\xc3\xb3. Escriure una d'aquestes proves utilitzant un cert llenguatge formal \xc3\xa9s un exercici molt tedi\xc3\xb3s i sovint d\xc3\xb3na lloc a una successi\xc3\xb3 de proposicions en qu\xc3\xa8 la subst\xc3\xa0ncia intu\xc3\xaftiva i intel\xc2\xb7ligible de l'assumpte \xc3\xa9s dif\xc3\xadcil d'entreveure (en contrapartida aquestes demostracions formals poden ser verificades mitjan\xc3\xa7ant un ordinador). A la pr\xc3\xa0ctica ordin\xc3\xa0ria de les matem\xc3\xa0tiques les demostracions formals tenen un objectiu secundari, i els matem\xc3\xa0tics creen nous teoremes sempre utilitzant demostracions creatives, intu\xc3\xaftives i per tant informals. Per aquesta ra\xc3\xb3 quan es publica un resultat matem\xc3\xa0tic nou sovint es requereixen setmanes o mesos de verificaci\xc3\xb3 per part d'altres matem\xc3\xa0tics professionals. En canvi una demostraci\xc3\xb3 formal pot ser revisada m\xc3\xa9s f\xc3\xa0cilment, nom\xc3\xa9s que en general no resulta f\xc3\xa0cil crear una demostraci\xc3\xb3 formal si no es coneix una demostraci\xc3\xb3 informal i intu\xc3\xaftiva a partir de la qual construir-la. Per aquesta ra\xc3\xb3 les demostracions purament formals s'acostumen a construir amb l'ajut d'ordinadors i m\xc3\xa8todes de demostraci\xc3\xb3 de teoremes interactius i sempre amb un prop\xc3\xb2sit secundari diferent d'entendre de manera comprensible els elements b\xc3\xa0sics involucrats en una demostraci\xc3\xb3._NEWLINE_La teoria de la demostraci\xc3\xb3 de fet s'ocupa de demostracions formals, o m\xc3\xa9s espec\xc3\xadficament de les propietats dels sistemes deductius i algunes de les seves propietats metal\xc3\xb2giques. Mentre que la q\xc3\xbcesti\xc3\xb3 de construir demostracions informals \xc3\xa9s un aspecte altament creatiu i fora de l'abast del funcionament algor\xc3\xadsmic dels ordinadors actuals. De fet no hi ha algorismes generals per construir demostracions informals, tot i que existeixen esquemes generals per a molts tipus de problemes, en general construir una demostraci\xc3\xb3 d'un problema obert acostuma a ser un problema dif\xc3\xadcil.\n_START_SECTION_\nDemostracions formals\n_START_PARAGRAPH_\nLes demostracions formals consisteixen t\xc3\xa8cnicament en una successi\xc3\xb3 finita de proposicions (o f\xc3\xb3rmules ben formades) cadascuna de les quals \xc3\xa9s o b\xc3\xa9 un axioma o b\xc3\xa9 es dedueix a partir d'algunes de les proposicions anteriors mitjan\xc3\xa7ant una regla de deducci\xc3\xb3 expl\xc3\xadcita._NEWLINE_Aquest procediment de deducci\xc3\xb3 mitjan\xc3\xa7ant regles de formaci\xc3\xb3 de f\xc3\xb3rmules, axiomes i regles d'infer\xc3\xa8ncia \xc3\xa9s un enfocament sint\xc3\xa0ctic. Alternativament molts sistemes l\xc3\xb2gics poden ser tractats construint una interpretaci\xc3\xb3 sem\xc3\xa0ntica dels mateixos mitjan\xc3\xa7ant la teoria de models. Aquest enfocament busca que un teorema sigui una proposici\xc3\xb3 que es d\xc3\xb3na en tots els models possibles d'una teoria (una \xc3\xbanica teoria en general admet m\xc3\xa9s d'un model, aquests coincideixen en els aspectes centrals definits a la teoria i difereixen en aspectes secundaris no tractats per la teoria). Una proposici\xc3\xb3 que es satisf\xc3\xa0 en tots els models \xc3\xa9s una proposici\xc3\xb3 v\xc3\xa0lida, els sistemes l\xc3\xb2gics estan constru\xc3\xafts de tal manera que tota proposici\xc3\xb3 dedu\xc3\xafble de la teoria sigui a m\xc3\xa9s una proposici\xc3\xb3 v\xc3\xa0lida en tots els models de la teoria.\n_START_SECTION_\nEl programa de Hilbert\n_START_PARAGRAPH_\nHist\xc3\xb2ricament el sorgiment de la teoria de la demostraci\xc3\xb3 es remunta a la crisi fundacional de les matem\xc3\xa0tiques a principis del segle XX. Diverses paradoxes sorgides en la teoria de conjunts i algunes informalitats usades comunament al c\xc3\xa0lcul infinitesimal, van conv\xc3\xa8ncer alguns matem\xc3\xa0tiques que era important fonamentar m\xc3\xa9s rigurosament el punt de partida d'algunes branques de la matem\xc3\xa0tica. Entre aquests matem\xc3\xa0tics es trobava en David Hilbert i alguns dels seus col\xc2\xb7laboradors. En resposta a la crisi fundacional, aquests matem\xc3\xa0tics van proposar un enfocament que amb el temps s'anomen\xc3\xa0 el programa de Hilbert._NEWLINE_B\xc3\xa0sicament aquest enfocament formalista consistia a axiomatitzar de manera expl\xc3\xadcita les diverses branques de la matem\xc3\xa0tica mitjan\xc3\xa7ant un conjunt d'axiomes expl\xc3\xadcits expressables en un llenguatge formal ben definit de tal manera que es pogu\xc3\xa9s demostrar la consist\xc3\xa8ncia de les diverses parts de la matem\xc3\xa0tica. Hilbert i altres matem\xc3\xa0tics tenien confian\xc3\xa7a en que per qualsevol \xc3\xa0rea de les matem\xc3\xa0tiques seria possible construir un conjunt de regles que portessin a demostrar en un nombre finit de passos si una proposici\xc3\xb3 era una proposici\xc3\xb3 v\xc3\xa0lida. Tanmateix K. G\xc3\xb6del va poder demostrar el 1931 que aquest enfocament tenia limitacions, fins i tot per un sistema tan central en les matem\xc3\xa0tiques como el de la artim\xc3\xa8tica dels nombres naturals.\n_START_SECTION_\nEl Hauptsatz de Gentzen\n_START_PARAGRAPH_\nEl 1934 Gerhard Gentzen introdu\xc3\xad una noci\xc3\xb3 b\xc3\xa0sica de la moderna teoria de la demostraci\xc3\xb3."