Formalisme matemàtic

En fonaments de les matemàtiques, filosofia de les matemàtiques i filosofia de la llògica, el formalisme matemàtic és una teoria que sosté que les proposicions de les matemàtiques i la llògica poden considerar-se com a declaracions sobre les conseqüències de certes regles de manipulació de símbols o térmens o cadena de caràcters.

Per eixemple, la geometria euclidiana pot ser vist com un joc de llenguage l'objectiu del qual consistix en moure certes cadenes de símbols (cridats axioma) d'acort en un conjunt de regles anomenades regles d'inferència per a generar noves cadenes. En este joc es pot demostrar o provar que el teorema de Pitágoras és vàlit perque la cadena que representa la teorema de Pitágoras es pot construir usant només les regles establides.

D'acort en el formalisme, les "veritats" expressades en la llògica i les matemàtiques no són sobre els números, séries, o triànguls o qualsevol atra matèria específica — de fet, no són "sobre" res en absolut. Són formes sintàctiques els continguts de les quals o significats o referèncias (vore Sobre el sentit i la referència) no existixen a menos que se'ls done una interpretació (o semàntica).

En l'actualitat alguns —seguint a Michael Resnik— classifiquen el formalisme en "formalisme de joc". "Formalisme de térmens" (aquell en el qual els térmens (axioma) solament es denoten a sí mateixos i d'ells es deriva proposicions, pero sense pronunciar-se sobre la realitat ontològica dels mateixos; lo que es busca no és prova d'existència, pero coherència. etc.

A partir de la década dels 80 de el XX, alguns han propost que tot el nostre coneiximent matemàtic formal deu ser sistemàticament codificats en formats llegibles per un ordenador, a fi de facilitar la comprovació o chequeo automatizado de les demostracions matemàtiques; la Demostració automàtica de teoremes i l'us de Demostració interactiva de teoremes en el desenroll de les teories matemàtiques i programes informàtics. Per la seua estreta relació en l'informàtica, esta idea també és atractiva a matemàtics logicistas; intuicionistas i constructivista de la tradició de la "computabilidad" (vore també Proyecte Mizar, la biblioteca matemàtica que conté la colecció més gran del món d'obres matemàtiques estrictament formalisades i computarizadas.) (pero vore més avall).

S'ha sugerit que l'adopció del punt de vista formalista eximix als matemàtics de la necessitat de preocupar-se per qüestions dels “fonaments de les matemàtiques” i procedir com si estos assunts hagueren segut resolts o cariren d'interés matemàtic. Molts agreguen que, en la pràctica, els sistemes axiomàtics que s'estudien són sugerits per les exigències de la ciència en cada cas particular.

Història i evolució del concepte

Aun cuando l'idea bàsica de la formalisació dels térmens llògic-matemàtics té una trayectòria prou llarga, i per lo manco en part per l'anomenada crisis dels fonaments de les matemàtiques, cap a finals de el XIX va començar a prendre arraïlada la tesis que és possible definir les matemàtiques com el resultat de la manipulació de símbols d'acort a certes regles. Per eixemple, en 1898, es va propondre que:

«En la concepció formalista l'aritmètica és un joc en signes que es diuen buits, en la qual cosa es vol dir que no tenen un atre contingut (en el joc de càlcul) que el que se'ls assigna en relació al seu comportament baix certes regles de combinació (regles del joc). El jugador d'escacs fa un us similar de les seues peces ... Per supost que hi ha diferències importants entre l'escacs i l'aritmètica. Les regles de l'escacs són arbitràries, mentres que el sistema de regles de l'aritmètica és tal que els números poden ser referits a varietats [conjunts] de l'intuïció per mig de axioma simples i en això nos proporcionen importants contribucions en el coneiximent de la naturalea.»

Johannes Thomae (1840-1921)

Generalment es considera que el fundador del formalisme modern és David Hilbert. Cap a fins de el XIX i començos de el XX l'interés de Hilbert era la construcció axiomàtica; consistent i completa de la totalitat de les matemàtiques, seleccionant com a punt de partida els número natural i assumint que per mig de l'us d'axiomas es obvía la necessitat de definir els objectes bàsics (op. cit) en la finalitat de conseguir un sistema complet i consistent. (note's que en lo anterior Hilbert considera el càlcul com Càlcul llògic, portant a terme inferència (no necessària o exclusivament deductivas) a partir d'una concepció axiomàtica dels número natural, concepció que pren eixos números com a evidents en la mida que solament es referixen a sí mateixos.- vore Programa de Hilbert).

No obstant l'optimisme en la "implementabilidad" del proyecte va ser de curta duració, pel teorema de incompletitud de Gödel, que va demostrar que qualsevol sistema de axioma que incloga els número natural és ya siga incomplet o contradictori.

A pesar de lo anterior, Alfred Tarski va reprendre el concepte, pero introduint l'idea que l'estatus (correcció, validea, etc) d'una prova o demostració és relativa als axioma elegits per a expressar la teoria en qüestió. Tarski va començar -en la década del 30 de el XX- buscant redifinir certs conceptes semàntics (en particular, el de Veritat (vore ací), en el fi últim de construir un sistema formal axiomàtic que permetera la reformulación de teoremes en el llenguage d'eixe sistema, eliminant aixina els problemes. És generalment acceptat que en eixe proyecte Tarski va transformar radicalment el sistema "metamatemático" de Hilbert, mostrant, entre atres coses, que les conseqüències llògiques d'un argument seguixen d'eixe argument si i solament si cada model de les premisses és un model de les conclusions. (lo anterior es pot resumir en lo que Jaakko Hintikka crida els "teoremes de inconsistencia i l'impossibilitat", la proposició que conceptes tals com "veritat" no poden ser usats en llenguages de primer orde (digam per eixemple: el comú i corrent) sense caure en inconsistencias. Eixos conceptes solament poden ser definits i usats en un "metallenguage". Eventualment Tarski va creure que la manera de resoldre el problema en matemàtiques és basar la totalitat de les matemàtiques en l'àlgebra.)

Un dels estudiants més coneguts de Hilbert va ser John von Neumann qui, en 1931, va buscar presentar el formalisme com una síntesis dialèctica de la tesis logicista i l'antítesis intuicionista. Von Neumann va promoure l'us de models matemàtics que, explícitament, busquen ser coherents en el conjunt de axioma de la teoria, qualsevol siguen eixos axioma (vore Teoria de jocs). Estos treballs varen resultar de major importància per a desenrolls científics contemporàneus, des de l'economia a la mecànica quàntica. (vore Postulats de la mecànica quàntica).

Rudolf Carnap confronta directament el problema generat per les teoremes de Gödel, buscant resoldre-ho per mig del cridat "Principi de tolerància": En llògica, no hi ha moral. Tot lo món és lliure de construir la seua pròpia llògica, és dir, la seua pròpia forma de llenguage, com vullga. [émfasis de Carnap] . Carnap estén eixa tolerància a les matemàtiques: "L'actitut tolerant ací se sugerix és, sobre els càlculs matemàtics especials es referix, l'actitut que és tácitamente compartida per la majoria dels matemàtics." Adicionalment Carnap busca eliminar totalment la rellevància del significat per a les matemàtiques. La correcció (note's el terme) d'una teorema és decidida no en relació en consideracions o algun conjunt de regles "externes" sino en relació en les que s'elegixen per al sistema específic del com la teorema es deriva, l'únic en el qual té sentit.

També de major importància va ser (és?) la contribució del grup Bourbaki en favor d'exigir rigor i promoure l'us del método axiomàtic. A partir d'açò, el formalisme va aplegar, de facto, a constituir la posició més acceptada entre els matemàtics fins a l'últim quarto de el XX: "Els anys setanta varen vore decaure la tendència formalista, representada pel grup Bourbaki, seudònim de vàries generacions de matemàtics francesos."

No obstant el formalisme encara eixercix gran influència, part a través de el "llegat" de lo anterior pero també per mig de la seua importància, potser fonamental, en el desenroll de l'Informàtica, específicament, els llenguages de programació, a través del treball d'Haskell Curry, generalment considerat el fundador de la llògica combinatòria.

Aun cuando ni Bertrand Russell ni Alfred North Whitehead varen ser realment formalistes (sino més be logicistas) la publicació, en 1910, per eixos autors de Principia mathematica va ser generalment percebuda com un gran alvanç en l'intent de derivar els coneiximents matemàtics de l'época a partir d'un conjunt de principis o axioma.

Procés de formalisació

Per a que una teoria T qualsevol siga formalizable, esta requerix constituir un sistema axiomatizado

La constitució d'un sistema axiomàtic (o axiomatización d'una teoria) és la selecció, per a eixa teoria, d'un conjunt de proposicions que seran considerades com a bàsiques (és dir, des de les quals es pot, en principi, derivar el restant de les proposicions que constituïxen el cos de la teoria) i evidents o no demostradores (vore axioma)

Eixemples de teories axiomatizadas són: la geometria plana en els axioma de Euclides, l'aritmètica (teoria de números) en els axioma de Peano, la teoria de conjunts en els axioma de Zermelo-Fraenkel, la teoria de provabilitats en els axioma de Kolmogórov, etc.

A partir de lo anterior, i restringint-nos només a llògica de primer orde, es tria un llenguage L de primer orde apropiat per a T. (específicament un Llenguage formalisat). El vocabulari per a un llenguage de primer orde formalisat consistix de cinc components o térmens. Quatre d'ells són sempre els mateixos i no depenen de la teoria T. Estos primers quatre térmens són:

1. Una llista enumerable de variables: El seu número pot ser infinit, pero de cardinal igual a $\mathrm{\aleph }0$, el cardinal dels número natural.
2. Els símbols per a les conectivas: (¬) per a la negació, (∧) per a la conjunció, (∨) per a la disjunció (o inclusivo), (→) per a l'implicació i (↔) per a l'equivalència o doble implicació. Estes conectivas són realment les mateixes del nostre llenguage usual.
3. El signe per a l'igualtat matemàtica (=) imprescindible en la notació matemàtica.
4. Els Quantificadorés: ( ∀ ) universal i ( ∃ ) l'existencial.
5. Els térmens (o paràmetros) indefinits (o "primitius"). Ya que T és, ara, una teoria axiomatizada, T du implícita o explícitament, certs «térmens indefinits» extres als anteriors — a voltes també denominats elements primitius — als que generalment se'ls assigna sengles símbols. Estos símbols, un per cada terme indefinit de la teoria T, usualment es denominen paràmetros del llenguage de primer orde L. Este conjunt de símbols correspon al quint terme del vocabulari del nostre llenguage L per a la teoria T. Per eixemple, entre els térmens indefinits de la geometria plana de Euclides, apareix punt, recta, interestancia, incidència, etc. i per a cada u d'ells usem símbols apropiats per a completar el vocabulari del llenguage de primer orde L.

Atres eixemples: Entre els térmens indefinits de l'aritmètica, en la axiomatización de Peano, apareix zero, suma i multiplicació, i per a ells un tria com els seus símbols, 0, + i × respectivament. La teoria de conjunts més fàcil de formalisar és, la de Fraenkel-Zermelo (FZ), por cuanto que esta teoria, no té sino un sol terme indefinit, açò és, la relació de pertinença que simbolisem com "$\in$".

ya que els paràmetros són els únics símbols en el vocabulari d'un llenguage de primer orde que depenen de la teoria prèviament axiomatizada T, llavors, un formalisa T simplement triant estos paràmetros. Una volta feta esta “selecció”, la totalitat de la teoria T queda formalisada. Es pot ara expressar en el llenguage de primer orde resultant L, no només els axioma, definicions i teoremes de T, si no molt més. Es pot expressar en eixe llenguage L tots els axioma de la llògica clàssica i des de després, també tota l'argumentació que un usa en la prova de les teoremes de la teoria T. Resumint, es pot ara proseguir enterament en L; és dir, “formalment”.

Vore també

• David Hilbert
• Llògica matemàtica
• Teoria de categories
• Teoria de conjunts
• Teoria de la demostració
• Teoria de models
• Metamatemática
• Método formal
• Método hipotètic-deductivo
• Teoria de tipos
• Teoremes de incompletitud de Gödel

Bibliografia

• Ruiz Z; Angel: 26.3 El formalisme
• Ledesma Pereña, Nicasio: La Matemàtica Moderna: Entre el formalisme modificat de Cavaillès i el platonisme estructural de Lautman.
• Corry; Leo: David Hilbert and the Axiomatization of Physics (1894-1905)
• Weir, Alan: Formalism in the Philosophy of Mathematics en Stanford Encyclopedia of Philosophy (en Idioma anglés)
• Weir; Alan: A Neo-Formalist Approach to Mathematical Truth (en Idioma anglés)