Teoria de la demostració
La teoria de la demostració es una branca de la lògica matemàtica que tracta amb la estructura de les demostracions matemàtiques i la potència expresiva d'un determinat conjunt d'axiomes matemàtics.
Taula de continguts |
Tipus de demostracions [modifica]
Les demostracions matemàtiques que sovient es troven en els llibres estàn contenen raonaments expressats en un llengüatge informal. També la pràctica ordinària dels matemàtics es basa en intuicions que tracten de capturar l'essencia d'un conjunt d'objectes matemàtics (aquestes demostracions sovint requereixen creativitat i enginy per ser creades). En canvi hi ha un altre tipus de demostracions purament formals que consisteixen en la aplicació reiterada d'un conjunt d'axiomes i regles de deducció. Escriure una d'aquestes proves utilitzant un cert llenguatge formal és un exercici molt tediósi sovint dona lloc a una successió de proposicions en que la substància intuitiva i intel·ligible de l'assumpte és dificil d'entreveure (en contrapartida aquestes demostracions formals poden ser verificades mitjançant un ordinador). A la pràctica ordinaria de les matemàtiques les demostracions formals tenen un objectiu secondari, i els matemàtics creen nous teoremes sempre utilitzant demostraciosn creatives, intuitives i per tant informals. Per aquesta raó quan es publica un resultat matemàtic nou sovint es requereixen setmanes o mesos de verificació per part d'altres matemàtics professionals. En canvi una demostració formal pot ser revisada més fàcilment, només que en general no resulta fàcil crear una demostració formal si no és coneix una demostració informal i intuitiva a partir de la qual construir-la. Per aquesta raó les demostracions purament formals s'acostumen a construir amb l'ajut d'ordinadors i mètodes de demostracció de teoremes interactius i sempre amb un propòsit secundari diferent de entendre de manera comprensible els elements bàsics involucrats en una demostració.
La teoria de la demostració de fet s'ocupa de demostracions formals, o més específicament de les propietats dels sistemas deductius i algunes de les seves propietats metalògiques. Mentre que la qüestió de construir demostracions informals és un aspecte altament creatiu i fora de l'abast del funcionament algorísmic 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ó d'un problema obert acostuma a ser un problema difícil.
Demostracions formals [modifica]
Les demostracions formals consisteixen tècnicament en una successió finita de propocisions (o fòrmules ben formades) cadascuna de les quals és o bé un axioma o bé s'en dedueix a partir de algunes de les proposicions anteriors mitjançant una regla de deducció explícita.
Aquest procediment de deducció mitjançant regles de formació de fòrmules, axiomes i regles d'inferència és un enfoc sintàctic. Alternativament molts sistemes lògics poden ser tractats construint una interpretació semàntica dels mateixos mitjançant la teoria de models. Aquest enfoc busca que un teorema sigui una proposició que es dona en tots els models possibles d'una teoria (una única teoria en general admet més 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ó que es satisfà en tots les models es una proposició vàlida, els sistemes lògics estan construits de tal manera que tota proposició deduïble de la teoria sigue a més una proposició vàlida en tots els models de la teoria.
Historia de la teoria de la demostració [modifica]
El programa de Hilbert [modifica]
Històricament el sorgiment de la teoria de la demostració és remunta a la crisi fundacional de les matemàtiques a principis del segle XX. Diverses paradoxes sorgides en la teoria de conjunts i algunes informalitats usades comunment al càlcul infinitesimal, van convéncer alguns matemàtiques que era important fonamentar més rigurosament el punt de partida d'algunes branques de la matemàtica. Entre aquests matemàtics es trobava en David Hilbert i alguns dels seus col·laboradors. En resposta a la crisi fundacional, aquests matemàtics van proposar un enfoc que amb el temps s'anomenà el pograma de Hilbert.
Bàsicament aquest enfoc formalista consistia en axiomatitzar de manera explícita les diverses branques de la matemàtica mitjançant un conjunt d'axiomes explícits expressables en un llenguatge formal ben definit de tal manera que és pogués demostrar la consistència de les diverses parts de la matemàtica. Hilbert i altres matemàtics tenien confiança en que per qualsevol àrea de les matemàtiques seria possible construir un conjunt de regles que portéssin a demostrar en un nombre finit de passos si una proposició era una proposició vàlida. Tanmateix K. Gödel va poder demostrar el 1931 que aquest enfoc tenia limitacions, fins i tot per un sistema tan central en les matemàtiques como el de la artimètica dels nombres naturals.
Els teoremes d'incompletasa de Gödel [modifica]
El Hauptsatz de Gentzen [modifica]
El 1934 Gerhard Gentzen introduí una noció bàsica de la moderna teoria de la demostració.
Les jerarquies aritmètica i analítica [modifica]
Referències [modifica]
Bibliografia [modifica]
- Proof Theory: The first setp into impredicatibility. Berlín: Springer-Verlag, 2009, p. 17-42.
