Soy un estudiante graduado de matemáticas, no un estudiante de filosofía, así que tengan paciencia conmigo. Sin embargo, estoy interesado en investigar qué es exactamente lo que paso haciendo la mayor parte de mi semana.
Tal como se practica, la prueba matemática parece no ser una deducción formal explícita dentro de un sistema formal. En cambio, la prueba parece ser una especie de pensamiento crítico sobre cosas que parecen ser necesariamente ciertas. Los supuestos utilizados en este pensamiento pueden identificarse razonablemente, pero no se declaran explícitamente desde el principio.
Dado esto, ¿cuál es la naturaleza de las conclusiones matemáticas en la práctica? ¿Son "deducciones informales"? ¿Existe alguna ventaja epistemológica en formar explícitamente conclusiones matemáticas dentro de un sistema formal, en lugar de lo que se practica comúnmente (por ejemplo, probablemente no haya probado algo como el teorema fundamental del cálculo al rastrearlo hasta axiomas como ZFC, pero tal vez debería ser hecho)? Si es así, ¿por qué este procedimiento no es estándar en la comunidad matemática?
Espero que estas preguntas sean al menos relativamente claras, ¡y gracias de antemano por cualquier información!
Me parece que una prueba es, o al menos tiende a ser, algo que los matemáticos en el campo relevante sienten que podría formalizarse. La formalización implicaría declarar explícitamente aquellos pasos que de otro modo se aceptan implícitamente como válidos. El problema es que hacerlo probablemente oscurecería el resultado principal en una maraña de detalles, de modo que leer las pruebas desperdiciaría el tiempo de los lectores al obligarlos a leer resultados que ya han aceptado durante mucho tiempo. Esta es probablemente la razón por la que la formalización no es un "procedimiento estándar en la comunidad matemática".
Dicho esto, la formalización está ganando más atención debido al creciente interés en las pruebas asistidas por computadora; cf. esta publicación de Mike Shulman sobre la formalización informática . En particular, tenga en cuenta el comentario de Shulman sobre "un beneficio adicional de hacer matemáticas con un asistente de prueba (en lugar de formalizar las matemáticas que ya ha hecho en papel), que creo que es particularmente pronunciado para la teoría de tipos y la teoría de tipos de homotopía".
Es posible que su prueba no sea completamente formal, pero la expectativa es que al menos sea falsificable. Si fuera completamente formal, entonces no solo sería falsable, sino también verificable. Si alguien revisa su prueba y señala errores o agujeros, se espera que reconozca los errores y reconozca los agujeros o explique cómo se pueden llenar los agujeros.
Hay más expectativas tanto en usted como autor de la prueba como en su audiencia por la prueba. Si su audiencia simplemente no se da cuenta de su prueba, o si tiene mejores cosas que hacer, entonces lea y verifique su prueba, entonces su prueba aún no es una prueba matemática real. Pero si hay lectores y señalan errores o agujeros, entonces el autor debe tratar de responder adecuadamente. Los lectores notarán si no responde correctamente a las preguntas y objeciones. Para ellos, será como jugar al ajedrez contra un niño que aún no comprende completamente las reglas del juego. Es posible que intenten explicar las reglas, pero a menudo el resultado es que su prueba simplemente se ignora y ya no se considera una pieza matemática.
hipnótico
James Kingsbery