Formalización

Este término es característico de la lógica y de la filosofía de la ciencia contemporáneas. Con «formalización de una teoría» se entiende el procedimiento mediante el cual se construye un sistema meramente sintáctico de símbolos S, regido por algunos axiomas (y eventualmente, por reglas operativas de formación y derivación de las fórmulas) de los cuales, según las reglas sintácticas del sistema mismo, se hacen derivar fórmulas que resulten transformaciones tautológicas del grupo de axiomas. Este sistema sintáctico puro, S, constituye una forma de una determinada teoría T (por ejemplo, de la aritmética de los números enteros, de la teoría de los conjuntos o del cálculo lógico elemental), cuando T resulta ser una interpretación verdadera, y posiblemente L-verdadera, de S. En general todas las teorías fundamentales de las matemáticas puras contemporáneas han recibido formalización; pero sigue aún sin resolverse del todo el problema de la formalización de la lógica y, en general, de los metalenguajes empleados para la formalización por las propias teorías matemáticas. Entre otras cosas, una de las mayores dificultades de tal formalización de segundo grado es la dada por un conocido teorema (el de Gödel) por el cual una teoría formalizada no puede contener la prueba de la propia no-contradicción.