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

Contingut suprimit Contingut afegit
m Corregit: dona lloc a -> dóna lloc a
m Corregit: troven -> troben en
Línia 2:
 
== Tipus de demostracions ==
Les demostracions matemàtiques que sovient es troventroben 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 dóna 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 es 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 [[metalògica|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.