Teoria de la demostració
La teoria de la demostració és una branca de la lògica matemàtica que tracta amb l'estructura de les demostracions matemàtiques i la potència expressiva d'un determinat conjunt d'axiomes matemàtics.
Tipus de demostracions
[modifica]Les demostracions matemàtiques que sovint es troben en els llibres contenen raonaments expressats en un llenguatge informal. També la pràctica ordinària dels matemàtics es basa en intuïcions que tracten de capturar l'essència 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 l'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ós i sovint dona lloc a una successió de proposicions en què la substància intuïtiva i intel·ligible de l'assumpte és difícil d'entreveure (en contrapartida aquestes demostracions formals poden ser verificades mitjançant un ordinador). A la pràctica ordinària de les matemàtiques les demostracions formals tenen un objectiu secundari, i els matemàtics creen nous teoremes sempre utilitzant demostracions creatives, intuïtives 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 es coneix una demostració informal i intuïtiva 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 demostració de teoremes interactius i sempre amb un propòsit secundari diferent d'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 sistemes 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 proposicions (o fórmules ben formades) cadascuna de les quals és o bé un axioma o bé es dedueix a partir d'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 enfocament sintàctic. Alternativament molts sistemes lògics poden ser tractats construint una interpretació semàntica dels mateixos mitjançant la teoria de models. Aquest enfocament 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 els models és una proposició vàlida, els sistemes lògics estan construïts de tal manera que tota proposició deduïble de la teoria sigui a més una proposició vàlida en tots els models de la teoria.
Història de la teoria de la demostració
[modifica]El programa de Hilbert
[modifica]Històricament el sorgiment de la teoria de la demostració es 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 comunament 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 enfocament que amb el temps s'anomenà el programa de Hilbert.
Bàsicament aquest enfocament formalista consistia a 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 es 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 portessin 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 enfocament tenia limitacions, fins i tot per un sistema tan central en les matemàtiques como el de la aritmètica dels nombres naturals.
Els teoremes d'incompletesa de Gödel
[modifica]El teorema d'incompletesa de Gödel estableix que cap teoria consistent, amb un nombre finit d'axiomes recursivament enumerable (en un llenguatge almenys tan potent com l'aritmètica), pot incloure totes les proposicions veritables. No obstant això, l'aritmètica és una teoria completable si s'afegeix un conjunt d'axiomes infinit i no recursiu. En altres paraules el teorema de Gödel només estableix que si és un tipus de teoria aritmètica:
O equivalentment:
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]Vegeu també
[modifica]Bibliografia
[modifica]- Pohlers, Wolfram. Proof Theory: The first setp into impredicatibility. Berlín: Springer-Verlag, 2009, p. 17-42. ISBN 978-3-540-69319-2.