No estoy seguro de entender completamente sus preguntas, pero intentaré una respuesta sesgada por los resultados formales recientes en Proof Theory y mi punto de vista de un científico informático. Entonces, no será una respuesta muy "filosófica" en el sentido de que no confío completamente en referencias filosóficas.

Tenga en cuenta que la naturaleza de la prueba no está del todo clara y todavía es algo que buscamos. De hecho, tenemos varias respuestas para eso.

¿Crees que nosotros, como humanos en general, usamos ciertas estrategias de prueba para probar cosas?

Hacia una formalización de la prueba . Los matemáticos ya hacían demostraciones mucho antes de que apareciera la lógica formal. Alrededor de los siglos XIX y XX se establecieron muchos sistemas de prueba de acuerdo con nuestra concepción de la prueba.

• Frege con su Begriffsschrift partió de la concepción de la Lógica aportada por Aristóteles y los estoicos.

• Hilbert hizo un sistema donde el modus ponens era la única regla y tratamos de derivar pruebas de axiomas ya establecidos

• Más interesante: Gentzen primero hizo un sistema basado en el uso de la lógica en métodos matemáticos llamado Deducción Natural (porque reproduce el uso empírico de la lógica por parte de los humanos). Al probar cosas, introducimos conectores y los eliminamos más tarde:

  • de A y B podemos reducir A /\ B (definición de "y")
  • de A /\ B podemos deducir A o B (uso de "y")

Con tal sistema podemos restringir el espacio de pruebas dentro de la introducción y eliminación de un conjunto finito de conectivos.

Entonces sí, usamos ciertas estrategias para probar cosas . Otras preguntas:

• ¿De dónde vienen estas reglas?
• ¿Es la lógica más que eso?
• ¿Por qué usamos estas reglas y no otras?

Las dos primeras preguntas se pueden responder, la última puede ser una pregunta de psicología o biología (de hecho, hay literatura al respecto).

Si lo anterior es cierto, significa que hay ciertas estrategias que debemos seguir, ¿dónde crees que entra la creatividad?

Un fino análisis de la lógica . Volviendo a Gentzen, observó que las deducciones del sistema de Deducción Natural podrían reducirse/simplificarse: cuando introducimos un conectivo y lo eliminamos inmediatamente después, estamos haciendo una "desviación" que no es necesaria.

No pudo probar eso, por lo que creó otro sistema llamado Sequent Calculus . Ese sistema no se basaba en el estudio del uso de la prueba sino en un análisis de la deducción natural y la lógica. El Cálculo Secuente analiza la estructura profunda de la lógica y sus simetrías según una dualidad hipótesis/conclusión más que introducción/eliminación o definición/uso.

El último sistema fue lo suficientemente adecuado para hacer explícito el concepto de "desviación": se llama regla de corte y ahí es donde entra la creatividad (pero él no lo sabía).

La creatividad y el uso de lemas . La regla de corte se expresa de la siguiente manera: de Γ ⊢ Δ,A (izquierda = conjunción de hipótesis, derecha = disyunción de conclusiones, las letras griegas son múltiples conjuntos de fórmulas) y Σ,A ⊢ Π podemos deducir Γ,Σ ⊢ Π, Δ. Al leer la regla en sentido inverso, significa que si queremos probar Γ,Σ ⊢ Π,Δ (que es lo que quieras) puedes introducir una A arbitraria siempre que A pueda probarse con alguna hipótesis Γ que tengas y que dando A y eventualmente alguna otra hipótesis Σ que tienes, puedes probar lo que querías.

La regla de corte es en realidad el uso del lema en matemáticas. Cuando quieras probar algo, prueba un lema A y úsalo.

Siguiendo su objetivo, Gentzen demostró que el uso de la regla de corte (que representa las desviaciones ahora llamadas "cortes") podría eliminarse. Significa que podemos probar cosas sin lemas y solo con pura aplicación de reglas lógicas. Solo un problema: reducir una prueba con cortes puede conducir a una explosión de complejidad con pruebas de gran tamaño (a veces de un tamaño absurdo).

Un ejemplo concreto de cortes . Digamos que quieres probar que 5+3 es lo mismo que 3+5. Puede usar "aplicación pura de reglas" que conducen al resultado de 8 en ambos lados O usar creatividad/un lema/la regla de corte: demostramos que la suma es conmutativa (para todo n y m, n+m = m+n ) y que la conmutatividad de la suma prueba lo que queremos.

Hacemos un desvío que no es necesario sino más creativo, más útil, más interesante...

¿En qué se diferencia probar cosas en matemáticas del mundo real? [...] En otras palabras, para probar q en la vida real, podemos encontrar fácilmente p que resulte en q y no es muy desafiante. Sin embargo, ¿qué hace que esto sea un desafío en matemáticas?

Hum... No estoy seguro de entender eso. En su ejemplo, la razón puede ser que el espacio de búsqueda es finito cuando en matemáticas puede ser infinito . Pero no es algo general si en el "mundo real" incluye resultados sobre física, por ejemplo.

Epílogo: Hacia la estructura profunda de la lógica

El origen de las reglas . En el siglo XX, lógicos e informáticos descubrieron algo sorprendente llamado isomorfismo de Curry-Howard . Se afirma que :

• La demostración de algunos sistemas lógicos en realidad corresponde exactamente a los programas de computadora de algún sistema (La Deducción Natural Intuicionista corresponde al Cálculo Lambda).

• Para los sistemas correspondientes, la fórmula demostrada por una prueba puede verse como el tipo del programa correspondiente.

• La eliminación de recortes puede verse como la ejecución de programas

No hay mucha literatura al respecto, pero creo que la correspondencia le da un estado "natural" a las reglas lógicas que provienen del concepto natural de "computación".

Este paradigma interpreta las reglas lógicas como construcciones de programas: la implicación lógica se ve como una función en un lenguaje de programación, la conjunción como un par, la disyunción como un tipo de suma/tipo algebraico ...

Un análisis aún más fino de la lógica . Recientemente, lógicos como Jean-Yves Girard intentaron profundizar aún más en el análisis de la lógica: en la mayoría de los sistemas de prueba tenemos una regla para "duplicar" y "borrar fórmula". Por ejemplo, dando A ⊢ A, sigue siendo válido lo siguiente: A,A ⊢ A. Y dando A,A ⊢ A tenemos A ⊢ A que sigue siendo válido. ¿Qué pasa si eliminamos estas reglas y vemos pruebas como reacciones químicas donde consumimos fórmulas? Condujo a la Lógica Lineal que finalmente reintroduce la infinitud/la estaticidad de la verdad con los nuevos operadores !A y ?A.

La Lógica Lineal finalmente condujo a un nuevo estado dinámico e interactivo para las pruebas que todavía se está investigando en la actualidad. Ese nuevo enfoque se basa completamente en el concepto de eliminación de cortes, que ahora se considera interacción , una idea central de la investigación actual en Teoría de la prueba.

Hacia una lógica totalmente interna . Como dijiste, el problema de los axiomas y el teorema puede ser problemático. En lógica confiamos demasiado en un mundo externo. Los lógicos intentaron hacer una lógica interna llamada Lúdica que también se encuentra actualmente bajo investigación. Los lúdicos tienen un concepto de pruebas "parciales" donde dos pruebas parciales interactúan juntas, una tratando de probar una fórmula A y la otra la negación dual y solo una gana.

La negación Las investigaciones recientes en Teoría de la Prueba interactúan mucho con la informática y tienden a dar un tratamiento preferencial a la lógica explicada por la computación.

Una pregunta bastante controvertida es: ¿qué pasa con los sistemas lógicos donde el teorema de eliminación de cortes (los cortes pueden eliminarse) no se cumple y que no tiene ningún sistema correspondiente en Ciencias de la Computación? ¿Son realmente "válidos"?

Algunos sistemas en "lógicas filosóficas" no disfrutan del teorema de eliminación de corte, pero es otro debate.

Resumen

• Una prueba puede verse como un programa de algún sistema de programación en Ciencias de la Computación

• La informática y la regla de corte dan direcciones realmente interesantes

• La regla de corte y el procedimiento de eliminación de corte pueden ser el núcleo de la lógica.

• Sin considerar el uso de la lógica por parte de los humanos, podemos estudiar la estructura formal de la lógica aún más profunda y finamente.

• Los resultados formales en Ciencias de la Computación, Teoría de Pruebas y Matemáticas deberían interactuar más con los filósofos: las ideas filosóficas son desconocidas para la mayoría de los primeros y la computación y los detalles técnicos para los segundos.

Esta es una pregunta muy amplia; pero tal vez al centrarnos en el contraste que sugiere entre las pruebas legales y matemáticas, podemos reducirlo un poco. Como mínimo, esto puede darle algunas ideas sobre dónde podría comenzar su búsqueda. Así que tú dices:

“En la vida real, si queremos probar que alguien es inocente, simplemente buscamos un grupo de testigos de confianza para que testifiquen que alguien es inocente. En otras palabras, para probar q en la vida real, podemos encontrar fácilmente p que resulte en q y no es muy difícil. Sin embargo, ¿qué hace que esto sea un desafío en matemáticas?

Tres breves advertencias. (i) Continuaré usando 'prueba' tanto para lo matemático como para lo legal, aunque probablemente sería mejor usar dos palabras diferentes. (ii) Con cuidado de no caer en lo psicológico, al preguntar por qué nos resultan más fáciles las pruebas legales y si tenemos estrategias cognitivas para abordar las pruebas. (iii) No estoy seguro de por qué dice que las pruebas legales son más fáciles que las matemáticas: hay pruebas simples en matemáticas y pruebas duras en la ley.

Ahora, si está señalando el hecho de que las pruebas legales, pero no las pruebas matemáticas, se basan en evidencia empírica, podría analizar la distinción A Priori vs A Posteriori . Los "Fundamentos de la aritmética" de Frege pueden ser un buen lugar para comenzar. (Tenga en cuenta que algunos argumentan que el conocimiento matemático se puede derivar de la evidencia empírica: por ejemplo, la conjetura de Goldbach posiblemente esté respaldada por las computadoras que la están verificando. Alexander Paseau ha escrito sobre esto).

Si se pregunta más en particular sobre el estado epistémico de los testimonios de los testigos, puede consultar la literatura sobre Conocimiento por testimonio . (Tenga en cuenta que el conocimiento matemático de muchas personas probablemente proviene del testimonio: sé que 2+2=4 porque mi mamá/maestros me lo dijeron, no porque lo demostré).

Dado que habla de p 'que da como resultado' q , también puede consultar la literatura sobre pruebas/razonamiento deductivos, inductivos y abductivos . Las demostraciones matemáticas son deductivas, por supuesto; pero no es obvio que las pruebas legales lo sean. (Si aún no lo ha hecho, también puede ser útil ver algunas pruebas matemáticas 'en acción'. Por ejemplo, 'A Mathematical Introduction to Logic' de Enderton es formalmente riguroso y muy legible. O eche un vistazo a Robbins y Courant's ' Qué son las matemáticas". Para una perspectiva más filosófica, véase, por ejemplo, 'La búsqueda de la certeza' de Giaquinto.)

Dado que hace una distinción entre el mundo matemático y el mundo real, eche un vistazo al debate Realismo vs Nominalismo . Un desafío al que se enfrenta el realista es la cuestión de cómo podemos saber acerca de las matemáticas si los números son objetos abstractos.

Finalmente, otra forma de acercarse a la naturaleza del 'mundo matemático' puede ser preguntar sobre el Estatus de los Axiomas , por ejemplo: ¿Cómo conocemos las 'verdades básicas'? Véase, por ejemplo, 'Defending the Axioms' de Maddy y la reseña de Mary Leng.

Estos son solo algunos consejos, ninguno de los cuales responde directamente a su pregunta. Sin embargo, como dije anteriormente, si puede reducir un poco la pregunta, es mucho más probable que encuentre una respuesta satisfactoria.

(Espero dar una respuesta razonablemente corta eligiendo una perspectiva específica, en lugar de intentar una descripción general).

El intuicionismo se presentó como una forma de abordar los problemas que tenía la gente con el platonismo matemático cuando intentaban formalizar la lógica verbal. Descubrieron que cosas como la paradoja de Russel eran más difíciles de evadir de lo que uno podría suponer. Y eso asestó un duro golpe a la forma ordinaria y platónica de ver el proceso de las matemáticas.

Los intuicionistas señalaron que el platonismo podría ser un resultado más que la causa real de lo que sucede en el proceso matemático. Que las matemáticas no se trata de ideas absolutamente estables, sino que busca esas ideas para el uso de las otras ciencias.

Una interpretación del neointuicionismo es que las matemáticas son una ciencia experimental real. Es la forma más pura de psicología. Determina experimentalmente qué conceptos intuitivos los humanos no pueden dejar de lado fácilmente una vez que los tienen, y cómo esos conceptos se combinan bien o mal. Entonces, las matemáticas no estudian un reino fijo de la naturaleza fuera de nosotros, estudian el pensamiento humano y los procesos creativos.

1. Esto supone 'sí' a su pregunta 1. Pero no dice cuáles son. Parecen existir porque los encontramos. Y asumimos que hay más de ellos porque seguimos encontrándolos.

Hace esto de la misma manera que lo hace la química, tomando productos que ya ha establecido su capacidad para crear de manera confiable y usándolos juntos en un entorno artificial.

La prueba, pues, no es una cosa específica que pueda establecerse y fijarse. Se basa en qué intuiciones estables se pueden atraer que no se socavan fácilmente, y cómo se pueden combinar de acuerdo con patrones que encontramos difíciles de rechazar.

(El efecto secundario de este punto de vista por el cual el intuicionismo es más famoso es que deberíamos ser tentativos sobre el alcance de la 'probabilidad' y no asumir que todas las cosas que demostramos serán completamente consistentes entre sí. Encontramos que las contradicciones son difíciles psicológicamente, por lo que deberíamos evitarlos, pero no tenemos ninguna razón para creer que la intuición humana es internamente consistente).

2. Esto nos da una respuesta clara a su segunda pregunta por observación directa: la creatividad es obviamente parte de estos procesos, y no podrían funcionar sin ella. Incluso la construcción de algoritmos y sistemas formales en sí misma es una actividad creativa impulsada por el sentimiento de claridad y nuestro gusto humano compartido por la elegancia en la lógica.

Desde este punto de vista, los resultados matemáticos son relevantes, pero lo que realmente se está estudiando y evolucionando son los procesos de combinación y derivación.

Los sistemas formales y los resultados previos brindan formas en que podemos verificar si estamos de acuerdo, pero no nos resuelven los problemas. En la medida en que los problemas ya se hayan resuelto mecánicamente, esas son herramientas de ingeniería y ya no son un tema de estudio para las matemáticas reales.

3. Esta es la diferencia entre las matemáticas y otras formas de demostración. Se enfoca en ensamblar intuiciones puras y modelos abstraídos de situaciones en formas puramente mecánicas, sin mezclar con otros datos. No tiene como objetivo resolver los problemas en cuestión, sino proporcionar métodos para abordar los problemas en general que automáticamente se sentirán confiables para una amplia gama de usuarios humanos.

Solo intentaré responder una pequeña parte de su pregunta. Usted pregunta, más o menos: "¿existen ciertas estrategias en matemáticas que usamos para probar cosas?" Bueno, para probar teoremas, ciertamente hay algunas estrategias que los matemáticos usan una y otra vez. He enumerado un par a continuación.

• Reductio ad Absurdum: Para probar que un determinado enunciado es verdadero, suponemos que lo contrario es verdadero y tratamos de llegar a una contradicción. Si esto ocurre, entonces podemos decir que la afirmación original es verdadera. Esta técnica a menudo se llama prueba por contradicción.

• Inducción: Cuando queremos probar un enunciado P(n) para cada elemento n de los números naturales, a menudo usamos la inducción. Esto se hace probando que el enunciado se cumple para un número natural particular n_0 y luego mostrando que si el enunciado se cumple para n, entonces debe cumplirse para n+1. El ejemplo de libro de texto para esto muestra que n^2 <= 2^n para n >= 5.

Existen muchas otras herramientas para descubrir demostraciones, pero tienden a ser más especializadas, dependiendo de la rama de las matemáticas en la que estamos tratando de encontrar una demostración. Por ejemplo, en un análisis real, podemos tratar de demostrar que una propiedad P(x) se cumple para cada x en la recta numérica real. Para hacer esto, podemos mostrar en cambio que el conjunto de valores x tal que se cumple P(x), {x : P(x)}, es tanto abierto como cerrado . Entonces, a partir de otro teorema de topología, podemos concluir que P(x) se cumple para todo número real.

Su próxima pregunta es: si existen todas estas técnicas para crear pruebas, ¿dónde entra la creatividad? Bueno, la creatividad se usa para unir todas las piezas de una manera que tenga sentido. Además, se usa cuando todas las técnicas no son suficientes para completar una prueba, lo que sucede con mucha frecuencia. Aquí es cuando se inventan nuevas técnicas, y pueden volverse muy comunes o limitarse a unos pocos casos especiales.

Finalmente, ¿es este tipo de imaginación diferente de usar una computadora para probar todos los caminos posibles en una prueba para ver si podemos encontrar lo que queremos? Bueno, tal vez se podría decir que estamos usando las mismas técnicas una y otra vez, y que esto podría programarse en una computadora. Sin embargo, esto probablemente requeriría una enorme cantidad de tiempo de cálculo, más que la vida útil del universo. La diferencia es que cuando creamos nuestras pruebas rigurosas, a menudo tenemos un esbozo vago de cómo queremos proceder, y el rigor viene después. La creatividad está en generar una idea de cómo queremos avanzar en una prueba: la intuición detrás de por qué algo es cierto. Esto requiere imaginación y perspicacia.