Teoria de la demostració

La teoria de la demostració o teoria de la prova és una branca de la llògica matemàtica que tracta a les demostracions com objectes matemàtics, facilitant el seu anàlisis per mig de tècniques matemàtiques. Les demostracions solen presentar-se com estructures de senyes inductivamente definides que es construïxen d'acort en els axiomas i regles d'inferència dels sistemes llògics. En este sentit, la teoria de la demostració s'ocupa de la sintaxis, en contrast en la teoria de models, que tracta en la semàntica. Junt en la teoria de models, la teoria de conjunts axiomàtica i la teoria de la computabilidad, la teoria de la demostració és un dels «quatre pilars» dels fonaments de les matemàtiques.^{cita requerida}

Demostracions formals i informals

Dins de la teoria de la demostració és molt important distinguir entre les demostracions «informals» trobades en la pràctica quotidiana dels matemàtics i en els llibres comuns sobre matemàtiques, de les demostracions purament «formals» de la teoria de la demostració formal. Les primeres tenen l'objectiu de mostrar rigorosament un resultat matemàtic de manera clara, pero al mateix temps intuïtiva i inteligible, les segones d'estes demostracions són com una espècie d'esquemes d'alt-nivell escrits en llenguage formal, que en principi, poden permetre a un expert o un llògic construir una demostració purament formal del mateix resultat, donat el suficient temps i paciència. Per a la majoria dels matemàtics, escriure una demostració completament formal és una despesa de temps innecessari com per a ser pràctica comuna.

Les demostracions formals poden ser construïdes en ajuda d'ordenadors per mig de métodos de demostració de teoremes interactives o atres tècniques. És significatiu, que estes demostracions purament formals basades en la manipulació de signes poden ser verificades automàticament, també per ordenador. Verificar una demostració purament formal és simple, mentres que trobar demostracions és generalment molt més difícil. Una demostració informal en un artícul matemàtic, pel contrari, requerix semanes de revisió per parells per a ser verificada, i freqüentment pot contindre errors que passen inadvertits inclús per a matemàtics professionals en temes d'investigació suficientment complexos.

La teoria de la demostració formal s'ocupa de les propietats dels sistemes deductivos, la seua complexitat, el poder expressiu de dits sistemes i està íntimament conectada a la llògica matemàtica, la teoria de models i la fundamentación de les matemàtiques. Pel contrari el desenroll de demostracions informals és un terreny altament creatiu i si be existixen famílies sanceres d'esquemes de demostració en diferents àrees, són un eixercici bàsicament humà en el que no existixen algoritmes generals per a construir demostracions.

Història de la teoria de la demostració formal

Orígens

La teoria de la demostració formal va començar en la crisis sobre els fonaments de les matemàtiques de les primeres décades de el XX. A principis d'eixe sigle, i com a reacció a l'explosió del coneiximent matemàtic, varen començar esforços per a proporcionar al creixent cos de coneiximents un fonament formal ferm. Si be en les aplicacions de les matemàtiques esta fundamentación no era important, en atres àrees de la matemàtica, com la filosofia de la matemàtica s'estava fent necessària una clarificació dels conceptes fonamentals, ya que estaven apareixent problemes llògics com els identificats per B. Russell i A. N. Whitehead en el treball de Gottlob Frege i atres persones que havien tractat de fonamentar sólidamente les matemàtiques.

Entre els problemes de fundamentación per eixemple estava l'us dels "infinitesimals" que vagament relacionats en alguna cosa "infinitament menut" (la qual cosa era una noció massa imprecisa). L'eliminació dels infinitesimals per mig de l'us de llímits va significar un gran progrés per a establir les matemàtiques existents sobre un fonament més ferm i clar. Un atre problema sense fonamentar era lo "infinitament gran". Les investigacions sobre unicitat de representació de Georg Cantor varen forçar a este matemàtic a desenrollar una nova teoria de lo infinitament gran. Un dels punts centrals de la teoria de Cantor era la possibilitat de considerar inclús una colecció no finita d'objectes i formar un "objecte matemàtic" en esta colecció. Estos "objectes" varen ser denominats per Cantor en alemà com Mengen i el terme es va traduir com a 'conjunt' en espanyol. Per això Cantor va denominar a la seua teoria Mengenlehre que és l'orige de la teoria de conjunts. La possibilitat de formar conjunts sense restriccions, produïa certes contradiccions o antinomias. Un eixemple notable d'estes antinomias és la paradoxa de Russell sobre el conjunt de conjunts que no són membres de sí mateixos. Aixina si es poguera definir el conjunt:

seria una contradicció, ya que per construcció es tindria:

Estes paradoxes i provablement també el fet aparentment paradòxic de que l'axioma d'elecció oferia la possibilitat de que qualsevol conjunt poguera ser un conjunt ben ordenat, varen crear la sensació d'incertitut entre la comunitat matemàtica. Hermann Weyl en el seu artícul "Über die neue Grundlagenkrise der Mathematik" va apuntar que la circularidad de les definicions causaven paradoxes i antinomias també en la teoria de conjunts que s'usava en anàlisis matemàtic. Este matemàtic va introduir el terme "nova crisis de fonaments" en la discussió de l'época. En el seu llibre Dones Kontinuum ya havia propost desenrollar matemàtiques lliures de definicions circulares.

El programa de Hilbert

Artícul principal → Programa de Hilbert.

Les diverses paradoxas sorgides en la teoria de conjunts i els problemes de fundamentación del concepte d'infinit, varen dur a l'anomenada crisis fundacional de les matemàtiques a principis de el XX. Front a este debat entre els matemàtics, David Hilbert i alguns dels seus colaboradors varen considerar elaborar un programa de formalisació complet, per a demostrar la consistència de numeroses branques de la matemàtica. Esta proposta de formalisació es va conéixer com a programa de Hilbert.

Este enfocament formaliste pretenia axiomatizar de manera explícita els supòsits usats en diverses branques de les matemàtiques per mig d'un conjunt de axioma expressables en un llenguage formal ben definit i de manera que es poguera provar la consistència de les matemàtiques aixina formalisades. Hilbert i molts atres matemàtics tenien confiança en que este programa tindria èxit per a qualsevol àrea de les matemàtiques i sempre seria possible construir un conjunt de regles que permeteren demostrar en un número finit de passos si una proposició era una proposició vàlida (Entscheidungsproblem). No obstant, K. Gödel va poder demostrar en 1931 que este enfocament tenia llimitacions essencials, inclús en un sistema tan central per a les matemàtiques com era l'aritmètica dels número natural.

Les teoremes de incompletitud de Gödel

AP El teorema de incompletitud de Gödel establix que cap teoria consistent, en un número finit de axioma recursivamente enumerable (en un llenguage per lo manco tan potent com l'aritmètica), pot incloure totes les proposicions veritateres. No obstant, l'aritmètica és una teoria completable afegint un conjunt de axioma infinit i no recursivo. En atres paraules la teorema de Gödel solament establix que si $T(𝒜)$ és un tipo de teoria aritmètica:

O equivalentemente:

El Hauptsatz de Gentzen

En 1934 Gerhard Gentzen va introduir les nocions bàsiques que varen dur al desenroll de la moderna teoria de la demostració.

Referències

Bibliografia

• (2009) Proof Theory: The first step into impredicatibility, Berlín: Springer-Verlag, pp. 17-42. ISBN 978-3-540-69319-2.