Redacción de pruebas "semiformales

Question

Me interesan mucho las pruebas. He tomado un curso de pregrado llamado "Lógica y Teoría de Conjuntos", que me pareció muy interesante, pero al final insatisfactorio. Mi mayor decepción tiene que ver con el lenguaje en el que se expresan las pruebas. se expresan las pruebas. Me parece que tenemos todos los símbolos necesarios para expresar una prueba en "matemática pura". Es decir, que sólo usamos símbolos y unas pocas palabras especializadas (iff, let, ...). Y sin embargo, la mayoría de las pruebas que he visto son muros de texto en inglés, interpolados con símbolos matemáticos.

Cuando leo una prueba compleja, me veo en la necesidad de transcribirla en puros símbolos puros antes de tener alguna posibilidad de entenderla. He hablado con un profesor sobre esto, y me informó de que mis pruebas de "matemáticas puras" se en realidad se consideraban informales, ¡y no pruebas propiamente dichas! Parecía escéptico que alguien prefiriera los símbolos al inglés.

He buscado más información en Wikipedia y Google, y veo que hay hay algo que se llama una "Prueba Formal" (aunque he oído este término se utiliza en otras situaciones, por lo que no estoy muy seguro de que significa lo que creo que significa) que utiliza un ordenador para verificar una prueba escrita en una programación especial especial. Por fascinante que sea, parece estar un paso más allá de lo que busco. estoy buscando.

¿Existe un método conocido para escribir y compartir pruebas matemáticas? que sólo utilice símbolos matemáticos y no sea un lenguaje de lenguaje de programación? Y si no es así, ¿por qué se considera "tabú" o "informal"?

Gracias,

--jc

EDITAR: Supongo que esto resultó no ser una pregunta real? Extraño, lo he comprobado, definitivamente termina en un signo de interrogación. Gracias a todos por la ayuda, los consejos y los enlaces. Agradezco vuestras aportaciones.

Answer 1

N. G. de Bruijn es conocido, entre otras cosas, por su trabajo en la Automath proyecto. Automath era un lenguaje formal para escribir demostraciones que influyó mucho en muchos de los lenguajes utilizados hoy en día para la demostración matemática asistida por ordenador (como Coq y Mizar). Sin embargo, de Bruijn también dedicó algún tiempo a desarrollar un sistema de demostración "semiformal", que denominó "Mathematical Vernacular" (MV):

• N.G. de Bruijn, The Mathematical Vernacular, un lenguaje matemático con conjuntos tipificados

He aquí algunas explicaciones extraídas de la introducción:

1.2. La palabra "vernácula" significa la lengua nativa del pueblo, en contraste con la lengua oficial o literaria (antiguamente en contraste con el latín de la iglesia). En combinación con la palabra "matemático", se entiende por vernáculo la mezcla muy precisa de palabras y fórmulas que utilizan los matemáticos en sus mejores momentos, mientras que por lenguaje matemático "oficial" se entiende algún sistema formal que sólo utiliza fórmulas. [...]

1.4. A mucha gente le gusta pensar que lo que realmente importa en matemáticas es un sistema formal (que suele incluir el cálculo de predicados y la teoría de conjuntos de Zermelo-Fraenkel), y que todo lo demás es palabrería informal. acerca de ese sistema. Sin embargo, los sistemas formales actuales no describen adecuadamente cómo piensa la gente en realidad y, además, no se ajustan del todo a los objetivos que tenemos en educación matemática. Por eso resulta atractivo intentar introducir una parte sustancial de la lengua vernácula matemática en el sistema formal. Incluso se puede intentar descartar por completo el sistema formal, haciendo que la lengua vernácula sea tan precisa que sus reglas lingüísticas sean suficientemente sólidas como base para las matemáticas. [...]

1.6. La idea de desarrollar MV surgió del deseo de disponer de una etapa intermedia intermedio entre la presentación matemática ordinaria, por un lado, y la presentación totalmente codificada en sistemas tipo Automath, por otro. Se puede pensar que los textos de MV son escritos por un matemático que entiende completamente el tema, y la traducción a Automath por alguien que sólo conoce los lenguajes implicados. [...]

1.13. Se podría pensar en la verificación directa por máquina de libros escritos en MV, pero esto no será en absoluto tan "trivial" como en Automath. La verificación de libros en MV puede requerir bastante inteligencia artificial. En primer lugar, MV nos permite omitir partes de las pruebas, al menos mientras no se supriman definiciones.

Encontrará un ejemplo de "libro MV" en la sección 18 (por desgracia, es un poco difícil de maquetar aquí...).

Answer 2

Creo que Funmath puede ser exactamente lo que busca.