Este artículo Del New York Times es un obituario de el recientemente fallecido Dr. Voevodsky. Explicó que él estaba profundamente involucrado en el desarrollo de equipo de prueba de verificación, y para ello "se ha cambiado el significado del signo igual" y "reformulado las matemáticas desde su fundación".
Como el artículo está dirigido a un público general, no entra en detalles.
Alguien puede explicar el significado de estas dos citas del New York Times?
(Creo que están relacionados)
El cambio de paradigma aquí — que no se originan con Voevodsky — es que la equivalencia es generalmente más importante de la noción de igualdad. Hay una peculiaridad que hace que el logro el cambio difícil: la equivalencia es a menudo más complejo que un simple sí/no propuesta.
Por ejemplo, en teoría de grupos, es mucho más importante hablar acerca de si los dos grupos son isomorfos que si son iguales. De hecho, es bastante raro para hacer el último.
Como un ejemplo de la complejidad añadida, consideran que el primer teorema de isomorfismo de grupos. La principal conclusión que se dice a menudo como
Si $\varphi : G \to H$ es un grupo homomorphism, a continuación, $G/\ker(\varphi)$ es isomorfo a $\mathrm{im}(\varphi)$
pero eso es sólo parte de lo que dice: la primera isomorfismo no es el mero hecho de decir "hay un isomorfismo", pero que la función específica $\overline{x} \mapsto \varphi(x)$ se dice isomorfismo. (donde $\overline{x}$ denota la clase de congruencia de $x$)
Hablar de "cambiar el significado del signo igual" es, en mi opinión, un tanto hiperbólica. Realmente, es sólo describir el hecho de que si usted tiene una manera de razonar y calcular de una manera en que la equivalencia es realmente el principal concepto, es útil para cambiar el símbolo "=" para indicar la equivalencia. (y si usted realmente necesita la noción de igualdad, para encontrar alguna otra forma de expresarlo)
Una gran respuesta debe mencionar homotopy tipo de teoría y/o la univalence axioma. También debe murmuró algo sobre el desarrollo de la $\infty$-categoría de la teoría y la búsqueda interna de idiomas, y también acerca de la semántica de los tipos de identidad en intensional tipo de teoría. Yo no soy lo suficientemente ambicioso para intentar escribir una gran respuesta, así que sólo voy a mencionar los términos aquí para dar sugerencias para seguir leyendo.
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
