Formalismo (matemática)
En fundamentos de las matemáticas, filosofía de las matemáticas y filosofía de la lógica, el formalismo matemático es una teoría que sostiene que las proposiciones de las matemáticas y la lógica pueden considerarse como declaraciones sobre las consecuencias de ciertas reglas de manipulación de símbolos o términos o cadena de caracteres.
Por ejemplo, la geometría euclidiana puede ser visto como un juego de lenguaje cuyo objetivo consiste en mover ciertas cadenas de símbolos (llamados axiomas) de acuerdo con un conjunto de reglas llamadas reglas de inferencia para generar nuevas cadenas. En este juego se puede demostrar o probar que el teorema de Pitágoras es válido porque la cadena que representa el teorema de Pitágoras se puede construir usando sólo las reglas establecidas.
De acuerdo con el formalismo, las "verdades" expresadas en la lógica y las matemáticas no son acerca de los números, series, o triángulos o cualquier otra materia específica — de hecho, no son "sobre" nada en absoluto. Son formas sintácticas cuyos contenidos o significados o referencias (ver Sobre el sentido y la referencia) no existen a menos que se les de una interpretación (o semántica).
En la actualidad algunos —siguiendo a Michael Resnik— clasifican el formalismo en "formalismo de juego". "Formalismo de términos" (aquel en el cual los términos (axiomas) solo se denotan a sí mismos y de ellos se deriva proposiciones, pero sin pronunciarse acerca de la realidad ontológica de los mismos; lo que se busca no es prueba de existencia, pero coherencia. etc.
A partir de la década de los 80 del siglo XX, algunos han propuesto que todo nuestro conocimiento matemático formal debe ser sistemáticamente codificados en formatos legibles por un ordenador, a fin de facilitar la comprobación o chequeo automatizadas de las demostraciones matemáticas; la Demostración automática de teoremas y el uso de Demostración interactiva de teoremas en el desarrollo de las teorías matemáticas y programas informáticos. Debido a su estrecha relación con la informática, esta idea también es atractiva a matemáticos logicistas; intuicionistas y constructivistas de la tradición de la "computabilidad" (ver también Proyecto Mizar, la biblioteca matemática que contiene la colección más grande del mundo de obras matemáticas estrictamente formalizadas y computarizadas.) (pero ver más abajo).
Se ha sugerido que la adopción del punto de vista formalista exime a los matemáticos de la necesidad de preocuparse por cuestiones de los “fundamentos de las matemáticas” y proceder como si estos asuntos hubieran sido resueltos o carecieran de interés matemático. Muchos agregan que, en la práctica, los sistemas axiomáticos que se estudian son sugeridos por las exigencias de la ciencia en cada caso particular.
Aun cuando la idea básica de la formalización de los términos lógico-matemáticos tiene una trayectoria bastante larga, y por lo menos en parte debido a la llamada crisis de los fundamentos de las matemáticas, hacia finales del siglo XIX comenzó a tomar arraigo la tesis que es posible definir las matemáticas como el resultado de la manipulación de símbolos de acuerdo a ciertas reglas. Por ejemplo, en 1898, se propuso que:
Generalmente se considera que el fundador del formalismo moderno es David Hilbert. Hacia fines del siglo XIX y comienzos del XX el interés de Hilbert era la construcción axiomática; consistente y completa de la totalidad de las matemáticas, seleccionando como punto de partida los números naturales y asumiendo que mediante el uso de axiomas se obvía la necesidad de definir los objetos básicos (op. cit) con el fin de lograr un sistema completo y consistente. (nótese que en lo anterior Hilbert considera el cálculo como Cálculo lógico, llevando a cabo inferencias (no necesaria o exclusivamente deductivas) a partir de una concepción axiomática de los números naturales, concepción que toma esos números como evidentes en la medida que solo se refieren a sí mismos.- ver Programa de Hilbert).
Sin embargo el optimismo en la "implementabilidad" del proyecto fue de corta duración, debido al teorema de incompletitud de Gödel, que demostró que cualquier sistema de axiomas que incluya los números naturales es ya sea incompleto o contradictorio.
A pesar de lo anterior, Alfred Tarski retomó el concepto, pero introduciendo la idea que el estatus (corrección, validez, etc) de una prueba o demostración es relativa a los axiomas elegidos para expresar la teoría en cuestión. Tarski comenzó -en la década del 30 del siglo XX- buscando redifinir ciertos conceptos semánticos (en particular, el de Verdad (ver aquí), con el fin último de construir un sistema formal axiomático que permitiera la reformulación de teoremas en el lenguaje de ese sistema, eliminando así los problemas. Es generalmente aceptado que en ese proyecto Tarski transformó radicalmente el sistema "metamatematico" de Hilbert, mostrando, entre otras cosas, que las consecuencias lógicas de un argumento siguen de ese argumento si y solo si cada modelo de las premisas es un modelo de las conclusiones. (lo anterior se puede resumir en lo que Jaakko Hintikka llama los "teoremas de inconsistencia y la imposibilidad", la proposición que conceptos tales como "verdad" no pueden ser usados en lenguajes de primer orden (digamos por ejemplo: el común y corriente) sin caer en inconsistencias. Esos conceptos solo pueden ser definidos y usados en un "metalenguaje". Eventualmente Tarski creyó que la manera de resolver el problema en matemáticas es basar la totalidad de las matemáticas en el álgebra.)
Uno de los estudiantes más conocidos de Hilbert fue John von Neumann quien, en 1931, buscó presentar el formalismo como una síntesis dialéctica de la tesis logicista y la antítesis intuicionista. Von Neumann promovió el uso de modelos matemáticos que, explícitamente, buscan ser coherentes con el conjunto de axiomas de la teoría, cualquiera sean esos axiomas (ver Teoría de juegos). Estos trabajos resultaron de mayor importancia para desarrollos científicos contemporáneos, desde la economía a la mecánica cuántica. (ver Postulados de la mecánica cuántica).
Rudolf Carnap confronta directamente el problema generado por los teoremas de Gödel, buscando resolverlo por medio del llamado "Principio de tolerancia": En lógica, no hay moral. Todo el mundo es libre de construir su propia lógica, es decir, su propia forma de lenguaje, como quiera. [énfasis de Carnap] . Carnap extiende esa tolerancia a las matemáticas: "La actitud tolerante aquí se sugiere es, en cuanto a los cálculos matemáticos especiales se refiere, la actitud que es tácitamente compartida por la mayoría de los matemáticos." Adicionalmente Carnap busca eliminar totalmente la relevancia del significado para las matemáticas. La corrección (nótese el término) de un teorema es decidida no en relación a consideraciones o algún conjunto de reglas "externas" sino en relación a las que se eligen para el sistema específico del cual el teorema se deriva, el único en el cual tiene sentido.
También de mayor importancia fue (es?) la contribución del grupo Bourbaki en favor de exigir rigor y promover el uso del método axiomático. A partir de esto, el formalismo llegó, de facto, a constituir la posición más aceptada entre los matemáticos hasta el último cuarto del siglo XX: "Los años setenta vieron decaer la tendencia formalista, representada por el grupo Bourbaki, seudónimo de varias generaciones de matemáticos franceses."
Sin embargo el formalismo todavía ejerce gran influencia, parte a través del "legado" de lo anterior pero también por medio de su importancia, quizás fundamental, en el desarrollo de la Informática, específicamente, los lenguajes de programación, a través del trabajo de Haskell Curry, generalmente considerado el fundador de la lógica combinatoria.
Aun cuando ni Bertrand Russell ni Alfred North Whitehead fueron realmente formalistas (sino más bien logicistas) la publicación, en 1910, por esos autores de Principia mathematica fue generalmente percibida como un gran avance en el intento de derivar los conocimientos matemáticos de la época a partir de un conjunto de principios o axiomas.
En filosofía de las matemáticas, el deductivismo, o a veces si-entoncismo (del inglés if-thenism), es una variante del formalismo que propone que el trabajo del matemático consiste en derivar proposiciones a partir de la asunción de que ciertas otras son correctas (si A, entonces B). Tradicionalmente se ha asumido que esas proposiciones básicas (o axiomas) son o deberían ser indudablemente correctas. Pero eso no es ni necesariamente correcto ni necesario. No es necesario porque la matemática no necesita fundaciones indudables, y no es necesariamente correcto porque, de hecho, la matemática trabaja perfectamente (especialmente en el área de las matemáticas aplicadas) sobre la base que los axiomas son presumiblemente correctos y presumiblemente coherentes y que las inferencias que siguen de esos presumibles axiomas son presumiblemente posibles (en el sentido que se puede crear un modelo matemático a partir de ellas).
Los deductivistas requieren que toda y cada prueba matemática sea una deducción. Ellos reconocen que no todas tales pruebas son estrictamente válidas (véase Validez (epistemología) y Validez (lógica)) pero consideran que toda prueba informal debe ser completable como deducción para ser considerada válida.
Por ejemplo, el deductivismo considera que el teorema de Pitágoras no es verdadero sin más, sino solo en relación a ciertos supuestos. Si a las cadenas se les asignan significados, de tal manera que los axiomas sean verdaderos y reglas de inferencia sean válidas, entonces se obtienen «conclusiones ciertas», tales como el teorema de Pitágoras. En este sentido, el formalismo no sigue siendo obligatoriamente un juego simbólico sin sentido. El matemático puede confiar, en cambio, que existe una interpretación de las cadenas de caracteres sugerida por ejemplo por la física o por otras ciencias naturales, tal que las reglas conduzcan a «afirmaciones verdaderas». Por lo tanto un matemático deductivista se puede mantener al margen tanto de la responsabilidad por la interpretación como de las dificultades ontológicas de los filósofos.
En 1967, Hilary Putnam revivió una idea de Bertrand Russell —el «si-entoncismo» (if-thenism)— e introdujo el deductivismo como una respuesta a algunos problemas con el logicismo en Principia Mathematica. Putnam propone considerar las matemáticas como el estudio de las consecuencias de los axiomas, usando teoría de modelos. En consecuencia interpreta las proposiciones matemáticas como refiriéndose a un posible modelo para esas proposiciones. A diferencia de la sugerencia logicista de Russell y otros, el deductivismo basa y transforma la matemática en una lógica con un sentido mucho más amplio que el sentido logicista. La lógica deductivista incluye, por ejemplo, la teoría de conjuntos necesaria para estudiar las consecuencias que siguen de axiomas. El logicismo podría ser solo una versión del deductivismo, usando una concepción más restrictiva de la lógica matemática.
Para que una teoría T cualquiera sea formalizable, esta requiere constituir un sistema axiomatizado
La constitución de un sistema axiomático (o axiomatización de una teoría) es la selección, para esa teoría, de un conjunto de proposiciones que serán consideradas como básicas (es decir, desde las cuales se puede, en principio, derivar el resto de las proposiciones que constituyen el cuerpo de la teoría) y evidentes o no demostrables (ver axioma)
Ejemplos de teorías axiomatizadas son: la geometría plana con los axiomas de Euclides, la aritmética (teoría de números) con los axiomas de Peano, la teoría de conjuntos con los axiomas de Zermelo-Fraenkel, la teoría de probabilidades con los axiomas de Kolmogórov, etc.
A partir de lo anterior, y restringiéndonos sólo a lógica de primer orden, se escoge un lenguaje L de primer orden apropiado para T. (específicamente un Lenguaje formalizado). El vocabulario para un lenguaje de primer orden formalizado consiste de cinco componentes o términos. Cuatro de ellos son siempre los mismos y no dependen de la teoría T. Estos primeros cuatro términos son:
Otros ejemplos: Entre los términos indefinidos de la aritmética, en la axiomatización de Peano, aparece cero, suma y multiplicación, y para ellos uno escoge como sus símbolos, 0, + y × respectivamente. La teoría de conjuntos más fácil de formalizar es, la de Fraenkel-Zermelo (FZ), por cuanto que esta teoría, no tiene sino un solo término indefinido, esto es, la relación de pertenencia que simbolizamos como "".
Puesto que los parámetros son los únicos símbolos en el vocabulario de un lenguaje de primer orden que dependen de la teoría previamente axiomatizada T, entonces, uno formaliza T simplemente escogiendo estos parámetros. Una vez hecha esta “selección”, la totalidad de la teoría T queda formalizada. Se puede ahora expresar en el lenguaje de primer orden resultante L, no sólo los axiomas, definiciones y teoremas de T, si no mucho más. Se puede expresar en ese lenguaje L todos los axiomas de la lógica clásica y desde luego, también toda la argumentación que uno usa en la prueba de los teoremas de la teoría T. Resumiendo, se puede ahora proseguir enteramente con L; es decir, “formalmente”.
En 1993/4 surgió el proyecto QED (principalmente bajo el impulso de Robert S. Boyer): la propuesta de creación de una base de datos informatizada de todo el conocimiento matemático, estrictamente formalizado y con todas las pruebas habiendo sido verificados de forma automática.
Para este proyecto se creó una “ lista de correo” en la internet y se organizaron dos conferencias: La primera tuvo lugar, en 1994, en el Laboratorio Nacional Argonney la segunda, en 1995, en Varsovia, organizada por el grupo Mizar.
Sin embargo, y a partir de 1996, el proyecto parece haber cesado sus actividades. En un artículo de 2007, Freek Wiedijk identifica dos razones para el fracaso del proyecto.:
Aun así se proponen regularmente proyectos del tipo QED, y la biblioteca Mizar ha logrado formalizar una gran parte de las matemáticas de pregrado. A partir de 2007, es la mayor tal biblioteca.