Prueba no verificable

En la filosofía de las matemáticas , una demostración no verificable es aquella que se considera inviable para un matemático humano y, por lo tanto, de validez controvertida . El término fue acuñado por Thomas Tymoczko en 1979 en una crítica a la demostración asistida por computadora del teorema de los cuatro colores de Kenneth Appel y Wolfgang Haken , y desde entonces se ha aplicado a otros argumentos, principalmente aquellos con una excesiva división de casos o con partes procesadas por un programa informático difícil de verificar. La verificabilidad sigue siendo una consideración importante en las matemáticas computacionales .

Tymoczko argumentó que tres criterios determinan si un argumento es una demostración matemática:

• La capacidad de persuasión , que se refiere a la habilidad de la prueba para convencer a un probador racional de su conclusión;
• La verificabilidad , que se refiere a la accesibilidad de la prueba para su verificación por parte de los miembros de la comunidad matemática humana; y
• Formalizabilidad , que se refiere a que la prueba recurre únicamente a relaciones lógicas entre conceptos para fundamentar su argumento. ^{[ 1 ]}

En opinión de Tymoczko, la prueba de Appel-Haken no superó el criterio de verificabilidad al, según argumentó, sustituir la deducción por el experimento :

Si aceptamos el Teorema de los Cuatro Colores como tal, nos comprometemos a cambiar el significado de "teorema" o, más concretamente, el del concepto subyacente de "demostración". El uso de ordenadores en matemáticas, como en el Teorema de los Cuatro Colores, introduce experimentos empíricos. Independientemente de si consideramos o no que el Teorema de los Cuatro Colores está demostrado, debemos admitir que la demostración actual no es una demostración tradicional, ni una deducción a priori de una afirmación a partir de premisas. Es una demostración tradicional con una laguna, o vacío, que se llena con los resultados de un experimento bien concebido.

Sin posibilidad de ser examinada, una demostración puede cumplir su primer propósito de convencer al lector de su resultado y, sin embargo, fracasar en su segundo propósito de esclarecer al lector por qué ese resultado es verdadero; puede desempeñar el papel de una observación en lugar de un argumento. ^{[ 2 ] [ 3 ]}

Esta distinción es importante porque significa que las demostraciones no revisables exponen las matemáticas a un potencial de error mucho mayor. Especialmente en el caso de que la no revisabilidad se deba al uso de un programa informático (que puede contener errores ), sobre todo cuando dicho programa no está publicado, la credibilidad puede verse afectada como resultado. ^{[ 3 ]} Como escribió Tymoczko:

Supongamos que una supercomputadora se pusiera a trabajar en la consistencia de la aritmética de Peano y arrojara una prueba de inconsistencia , una prueba tan larga y compleja que ningún matemático podría comprenderla más allá de los términos más generales. ¿Podríamos tener la suficiente confianza en las computadoras como para aceptar este resultado, o diríamos que la evidencia empírica de su fiabilidad es insuficiente?

Sin embargo, la opinión de Tymoczko es refutada por argumentos que sostienen que las pruebas difíciles de analizar no son necesariamente tan inválidas como las pruebas imposibles de analizar.

Paul Teller afirmó que la comprensibilidad era una cuestión de grado y dependía del lector, no algo inherente a una demostración. Así como las demostraciones no se rechazan cuando los estudiantes tienen dificultades para comprenderlas, argumenta Teller, tampoco deberían rechazarse (aunque puedan ser criticadas) simplemente porque a los matemáticos profesionales les resulte difícil seguir el argumento. ^{[ 4 ] [ 3 ]} (Teller discrepó de la valoración de Tymoczko de que «[El Teorema de los Cuatro Colores] no ha sido comprobado por matemáticos paso a paso, como se han comprobado todas las demás demostraciones. De hecho, no puede comprobarse de esa manera.»)

Un argumento en la misma línea es que la división de casos es un método de prueba aceptado, y la prueba de Appel-Haken es solo un ejemplo extremo de división de casos. ^{[ 2 ]}

Por otro lado, la afirmación de Tymoczko de que las demostraciones deben ser al menos susceptibles de revisión y que los errores en demostraciones difíciles de revisar tienen menos probabilidades de ser detectados no suele ser cuestionada; en cambio, se han sugerido métodos para mejorar la revisabilidad, especialmente de las demostraciones asistidas por computadora. Entre las primeras sugerencias se encontraba la de la paralelización: la tarea de verificación podría dividirse entre varios lectores, cada uno de los cuales podría revisar una parte de la demostración. ^{[ 5 ]} Pero la práctica moderna, popularizada por Flyspeck , consiste en presentar las partes dudosas de una demostración en un formalismo restringido y luego verificarlas con un verificador de demostraciones que también está disponible para su revisión. De hecho, la demostración de Appel-Haken se ha verificado de esta manera. ^{[ 6 ]}

Sin embargo, la verificación automatizada aún no ha tenido una adopción generalizada. ^{[ 7 ]}