Ahora que hemos generalizado los conceptos de estructura, formula elemental y prueba elemental via el concepto de tipo, podemos enunciar en forma mucho mas general el programa de logica matematica para reticulados cuaterna dado al principio de este capitulo
Programa
adhocprefix(1)adhocsufix Dar un modelo matematico del concepto de formula elemental de tipo \(\tau\)
adhocprefix(2)adhocsufix Dar una definicion matematica de cuando una formula elemental de tipo \(\tau\) es verdadera en una estructura de tipo \(\tau\) para una asignacion dada de valores a las variables libres y a los nombres de elementos fijos de dicha formula elemental
adhocprefix(3)adhocsufix (Plato gordo) Dar un modelo matematico del concepto de prueba elemental en una teoria elemental. A estos objetos matematicos los llamaremos pruebas formales
adhocprefix(4)adhocsufix (Sublime) Intentar probar matematicamente que nuestro concepto de prueba formal es una correcta modelizacion matematica de la idea intuitiva de prueba elemental en una teoria elemental
Como veremos, los cuatro puntos anteriores pueden ser hechos satisfactoriamente y constituyen el comienzo de la logica matematica con cuantificadores. Cabe aclarar que la realizacion del cuarto punto es realmente sorprendente ya que es un caso de una prueba matematica rigurosa de un hecho que involucra un concepto intuitivo como lo es el de prueba elemental.
El punto (1) se resuelve en la seccion siguiente y si bien produce interesantes conceptos y resultados matematicos su resolucion es rutinaria. El punto (2) es resuelto por Tarski (Seccion [seccion modelo matematico del valor de verdad de una formula]). El punto (3) por Fregue (Seccion [seccion teorias de primer orden]). El (4) es una concecuencia de dos importantes resultados, el Teorema de Correccion y el Teorema de completitud de Godel.