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

Contingut suprimit Contingut afegit
m Corregit: la aplicació -> l'aplicació reiterada
Línia 2:
 
== Tipus de demostracions ==
Les demostracions matemàtiques que sovientsovint es troben en els llibres estàn contenen raonaments expressats en un llengüatgellenguatge informal. També la pràctica ordinària dels matemàtics es basa en intuicionsintuïcions que tracten de capturar l'essenciaessè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ósitediós i sovint dóna lloc a una successió de proposicions en que la substància intuitivaintuïtiva i intel·ligible de l'assumpte és dificildifícil d'entreveure (en contrapartida aquestes demostracions formals poden ser verificades mitjançant un ordinador). A la pràctica ordinariaordinària de les matemàtiques les demostracions formals tenen un objectiu secondarisecundari, i els matemàtics creen nous teoremes sempre utilitzant demostraciosndemostracions creatives, intuitivesintuï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 intuitivaintuï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 demostracciódemostració de teoremes interactius i sempre amb un propòsit secundari diferent de 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 sistemassistemes 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.
 
=== Demostracions formals ===
Les demostracions formals consisteixen tècnicament en una successió finita de propocisionsproposicions (o fòrmulesfórmules ben formades) cadascuna de les quals és o bé un axioma o bé s'enes dedueix a partir de d'algunes de les proposicions anteriors mitjançant una [[regla d'inferència|regla de deducció]] explícita.
 
Aquest procediment de deducció mitjançant regles de formació de fòrmulesfó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 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 les models es una proposició vàlida, els sistemes lògics estan construitsconstruïts de tal manera que tota proposició deduïble de la teoria siguesigui a més una proposició vàlida en tots els models de la teoria.
 
<!-- Proofs are typically presented as inductively-defined [[data structures]] such as plain lists, boxed lists, or trees, which are constructed according to the [[axiom]]s and [[rule of inference|rules of inference]] of the logical system. As such, proof theory is [[syntax (logic)|syntactic]] in nature, in contrast to [[model theory]], which is [[Formal semantics (logic)|semantic]] in nature. Together with [[model theory]], [[axiomatic set theory]], and [[recursion theory]], proof theory is one of the so-called ''four pillars'' of the [[foundations of mathematics]].<ref name=wang>E.g., Wang (1981), pp. 3–4, and Barwise (1978).</ref>