Teoria de la demostració: diferència entre les revisions

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 quequè 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ó.