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

La cuestión se vuelve interesante cuando se interpreta como una pregunta técnica sobre hasta qué punto podemos tener un lenguaje semiformal intermedio entre las pruebas verdaderamente formales, que son en gran medida ilegibles para los humanos, y las pruebas informales utilizadas por los matemáticos profesionales.

De hecho, se han realizado trabajos realmente interesantes sobre este tema. En particular, el Sistema de prueba Naproche pone en práctica esta idea de lenguaje semiformal. Véase también este artículo que describe el sistema y prueba el ejemplos de interfaz web ).

La idea de Naproche (para la comprobación de pruebas en lenguaje natural) es centrarse precisamente en el nivel de detalle de las pruebas que existe entre las pruebas totalmente formales que pueden comprobarse por ordenador y las pruebas totalmente en lenguaje natural utilizadas por los humanos. Cuando se utiliza Naproche, se crean pruebas en un lenguaje natural controlado, un lenguaje semi-formal que parece natural, mientras que el sistema convierte la prueba semi-formal en una prueba completamente formal que no se ve y que es comprobada por uno de los comprobadores de pruebas formales estándar.

El efecto es que, utilizando el lenguaje semiformal, uno guía a Naproche hacia una demostración formal que luego puede verificarse. Así, se obtiene el valor de la prueba formal verificada, sin necesidad de considerar nunca explícitamente el objeto de la prueba formal.

Además, como la sintaxis del lenguaje natural controlado utiliza formalismos TeX, las pruebas semiformales y los teoremas pueden componerse automáticamente de forma atractiva.

Animo a todo el mundo a que pruebe el ejemplos de interfaz web que incluye pruebas semiformales de Naproche (pero totalmente verificadas) de resultados elementales en teoría de grupos, teoría de conjuntos y una parte del texto de Landau.

Aquí tiene un ejemplo de texto naproche, y también puede consultar el salida pdf aquí . Este texto introducido textualmente da como resultado objeto de prueba formal que se verifica como correcta. (El pdf y el objeto de comprobación son archivos temporales, pero pueden generarse haciendo clic en "crear pdf" o "Comprobación lógica" en la interfaz web).

Axiom. 
There is no $y$ such that $y \\in \\emptyset$.

Axiom.
For all $x$ it is not the case that $x \\in x$.

Define $x$ to be transitive if and only if 
for all $u$, $v$, if $u \\in v$ and $v \\in x$ 
then $u\\in x$. Define $x$ to be an ordinal 
if and only if $x$ is transitive and for all 
$y$, if $y \\in x$ then $y$ is transitive.

Theorem.
$\\emptyset$ is an ordinal.

Proof.
Consider $u \\in v$ and $v \\in \\emptyset$. 
Then there is an $x$ such that $x \\in \\emptyset$. 
Contradiction. Thus $\\emptyset$ is transitive.
Consider $y \\in \\emptyset$. Then there is an 
$x$ such that $x \\in \\emptyset$. Contradiction.
Thus for all $y$, if $y \\in \\emptyset$ then $y$ 
is transitive. Hence $\\emptyset$ is an ordinal.
Qed.

Theorem.
For all $x$, $y$, if $x \\in y$ and $y$ is an 
ordinal then $x$ is an ordinal.

Proof.
Suppose $x \\in y$ and $y$ is an ordinal. Then 
for all $v$, if $v \\in y$ then $v$ is transitive. 
Hence $x$ is transitive. Assume that $u \\in x$. 
Then $u \\in y$, i.e. $u$ is transitive. Thus $x$ 
is an ordinal.
Qed.

Theorem: There is no $x$ such that for all $u$, 
$u \\in x$ iff $u$ is an ordinal.

Proof.
Assume for a contradiction that there is an $x$ 
such that for all $u$, $u \\in x$ iff $u$ is an ordinal.
Lemma: $x$ is an ordinal.
Proof:
Let $u \\in v$ and $v \\in x$. Then $v$ is an ordinal, 
i.e. $u$ is an ordinal, i.e. $u \\in x$. Thus $x$ is 
transitive. Let $v \\in x$. Then $v$ is an ordinal, 
i.e. $v$ is transitive. Thus $x$ is an ordinal. Qed.

Then $x \\in x$. Contradiction. Qed.

Answer 2

Una "prueba" es en realidad un meme, un organismo constituido no por células sino por pensamientos. Vive en la cabeza de la gente, a veces muta y a menudo (por desgracia) muere. En colonias, suelen vivir más tiempo y reproducirse con mayor eficacia. La ``prueba'' que escribimos es el órgano sexual de estos memes matemáticos: su único propósito es facilitar la reproducción desde la cabeza del autor a la tuya.

Ahora tu cabeza es diferente a la mía, y nuestras cabezas son diferentes a la de Milnor. Es completamente apropiado (e incluso esperado) que las necesidades reproductivas sean distintas en estas circunstancias diferentes. No se trata de encontrar el nivel de detalle "adecuado", sino de que sirva para fines diferentes. En última instancia, tú sabrás mejor que nadie lo que necesita tu cerebro y, al igual que el resto de nosotros, tendrás que trabajar para convertir lo que lees en lo que necesitas.

Answer 3

Quizás este artículo sea relevante:

Thomas Hales, Prueba formal , Avisos de la AMS 55 Número 11 (2008) pp 1370-1380. ( pdf )

Y otra cosa: Las "pruebas estructuradas" de Lamport:

Leslie Lamport, Cómo redactar una prueba (1995) ( abstracto )

Answer 4

Te sugiero que eches un vistazo a la página de Freek Wiedijk:

http://www.cs.ru.nl/~freek/

Él es un montón de papeles sobre diferentes formalizaciones. También, algunas charlas sobre 'proof sketches'. La teoría de conjuntos no es la única formalización.

Fíjate también en la luz HOL:

http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html

Esta lógica formal, pero no teoría de conjuntos, es cálculo lambda tipado. Puede inspirarte para otras formas de formalización que la teoría de conjuntos.

Lucas

Answer 5

(He publicado esto accidentalmente como respuesta a otra pregunta. No presté atención)

En este artículo en Notices of the AMS tenemos un extracto de Paul Halmos:

Mis consejos sobre el uso de las palabras pueden ser resumirse así. (1) Evite los términos técnicos, y especialmente la creación de otros nuevos posibles. (2) Piense detenidamente en los nuevos que debe crear; consulte a Roget; y hágalos lo más apropiados posible. (3) Utilice los antiguos correctamente y con coherencia, pero con un mínimo pedantería molesta. [...]

Todo lo dicho sobre las palabras, se aplica, mutatis mutatis mutandis, a las unidades aún más pequeñas de la matemática, los símbolos matemáticos. La mejor notación es la ausencia de notación. el uso de un complicado aparato alfabético, evítelo. Una buena actitud ante la preparación de exposición matemática escrita es fingir que se hablada. Imagina que estás explicando el tema tema a un amigo en un largo paseo por el bosque, sin sin papel; recurra al simbolismo sólo cuando sea realmente necesario. cuando sea realmente necesario.