Las primeras tienen el objetivo de mostrar rigurosamente un resultado matemático de manera clara, pero al mismo tiempo intuitiva e inteligible, las segundas de estas demostraciones son como una especie de esquemas de alto-nivel escritos en lenguaje formal, que en principio, pueden permitir a un experto o un lógico construir una demostración puramente formal del mismo resultado, dado el suficiente tiempo y paciencia.
Para la mayoría de los matemáticos, escribir una demostración completamente formal es un gasto de tiempo innecesario como para ser práctica común.
Es significativo, que estas demostraciones puramente formales basadas en la manipulación de signos pueden ser verificadas automáticamente, también por ordenador.
Una demostración informal en un artículo matemático, por el contrario, requiere semanas de revisión por pares para ser verificada, y frecuentemente puede contener errores que pasen inadvertidos incluso para matemáticos profesionales en temas de investigación suficientemente complejos.
Por el contrario el desarrollo de demostraciones informales es un terreno altamente creativo y si bien existen familias enteras de esquemas de demostración en diferentes áreas, son un ejercicio básicamente humano en el que no existen algoritmos generales para construir demostraciones.
A principios de ese siglo, y como reacción a la explosión del conocimiento matemático, comenzaron esfuerzos para proporcionar al creciente cuerpo de conocimientos un fundamento formal firme.
Entre los problemas de fundamentación por ejemplo estaba el uso de los "infinitesimales"[1] que vagamente relacionados con algo "infinitamente pequeño" (lo cual era una noción demasiado imprecisa).
La eliminiación de los infinitesimales mediante el uso de límites significó un gran progreso para establecer las matemáticas existentes sobre un fundamento más firme y claro.
Estos "objetos" fueron denominados por Cantor en alemán como Mengen y el término se tradujo como 'conjunto' en español.
La posibilidad de formar conjuntos sin restricciones, producía ciertas contradicciones o antinomias.
sería una contradicción, ya que por construcción se tendría:
Hermann Weyl en su artículo "Über die neue Grundlagenkrise der Mathematik"[2] apuntó que la circularidad de las definiciones causaban paradojas y antinomias también en la teoría de conjuntos que se usaba en análisis matemático.
Hilbert y muchos otros matemáticos tenían confianza en que este programa tendría éxito para cualquier área de las matemáticas y siempre sería posible construir un conjunto de reglas que permitieran demostrar en un número finito de pasos si una proposición era una proposición válida (Entscheidungsproblem).
Sin embargo, K. Gödel pudo demostrar en 1931 que este enfoque tenía limitaciones esenciales, incluso en un sistema tan central para las matemáticas como era la aritmética de los números naturales.
Sin embargo, la aritmética es una teoría completable añadiendo un conjunto de axiomas infinito y no recursivo.
En otras palabras el teorema de Gödel solo establece que si