Ahora que hemos generalizado los conceptos de estructura, fórmula elemental y prueba elemental vía el concepto de tipo, podemos enunciar en forma mucho mas general el Programa de Lógica Matemática para Reticulados Cuaterna dado al principio de este capítulo.
Programa de Lógica Matemática
adhocprefix(1)adhocsufix Dar un modelo matemático del concepto de fórmula elemental de tipo \(\tau\).
adhocprefix(2)adhocsufix Dar una definición matemática de cuando una fórmula elemental de tipo \(\tau\) es verdadera en una estructura de tipo \(\tau\) para una asignación dada de valores a las variables libres y a los nombres de elementos fijos de dicha fórmula elemental.
adhocprefix(3)adhocsufix (Plato gordo) Dar un modelo matemático del concepto de prueba elemental en una teoría elemental. A estos objetos matemáticos los llamaremos pruebas formales.
adhocprefix(4)adhocsufix (Sublime) Intentar probar matemáticamente que nuestro concepto de prueba formal es una correcta modelización matemática de la idea intuitiva de prueba elemental en una teoría elemental.
Como veremos, los cuatro puntos anteriores pueden ser hechos satisfactoriamente y constituyen el comienzo de la lógica matemática con cuantificadores. Cabe aclarar que la realización del cuarto punto es realmente sorprendente ya que es un caso de una prueba matemática rigurosa de un hecho que involucra un concepto intuitivo como lo es el de prueba elemental.
El punto (1) se resuelve en la sección siguiente y si bien produce interesantes conceptos y resultados matemáticos su resolución es rutinaria. El punto (2) es resuelto por Tarski en la Sección Modelo Matemático del Valor de Verdad de una Fórmula. El punto (3) por Fregue en la Sección Teorías de Primer Orden. El (4) es una consecuencia de dos importantes resultados, el Teorema de Corrección y el Teorema de Completitud de Godel.