Teoria de la demostració

De Viquipèdia
Dreceres ràpides: navegació, cerca

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 expresiva d'un determinat conjunt d'axiomes matemàtics.

Tipus de demostracions[modifica | modifica el codi]

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 dóna lloc a una successió de proposicions en que 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 | modifica el codi]

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 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 dóna 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 é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 | modifica el codi]

El programa de Hilbert[modifica | modifica el codi]

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 enfoc que amb el temps s'anomenà el pograma de Hilbert.

Bàsicament aquest enfoc 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 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 | modifica el codi]

El Hauptsatz de Gentzen[modifica | modifica el codi]

El 1934 Gerhard Gentzen introduí una noció bàsica de la moderna teoria de la demostració.

Les jerarquies aritmètica i analítica[modifica | modifica el codi]

Referències[modifica | modifica el codi]

Bibliografia[modifica | modifica el codi]

  • Pohlers, Wolfram. Proof Theory: The first setp into impredicatibility. Berlín: Springer-Verlag, 2009, p. 17-42. ISBN 978-3-540-69319-2.