¿Puede la prueba por contradicción funcionar sin la ley del medio excluido?

Recientemente estuve pensando en la validez de la prueba por contradicción. He leído en los últimos días cosas sobre lógica intuicionista y teoremas de Godel para ver si me darían respuestas a mis preguntas. En este momento todavía tengo preguntas pendientes (tal vez relacionadas con el nuevo material que leí) y esperaba obtener algunas respuestas

( ADVERTENCIA : está a punto de proceder a leer contenido con bases muy confusas en la lógica, tome todo con un grano de sal, se supone que es una pregunta y no una respuesta, hay muchos malentendidos).

Creo que mi pregunta principal es, una vez que demostramos que no A conduce a alguna contradicción, por lo que no A debe ser falso, entonces llegamos a la conclusión de que A debe ser cierto. Esa parte tiene sentido (especialmente si acepto la ley del medio excluido como algo que tiene sentido), pero lo que me molesta es la forma en que ocurre la prueba por contradicción. Primero comenzamos con no A y luego simplemente aplicamos axiomas y reglas de inferencias (digamos mecánicamente) y vemos a dónde nos lleva eso. Por lo general, llega a una contradicción (digamos que A es verdadero o y \ phi es verdadero). Concluimos que no A debe ser falso, por lo que A es verdadero. Esta bien. Pero mi pregunta es, ¿qué tipo de garantías tienen los sistemas formales que$\neg \varphi$$\phi$si aplicara el mismo proceso pero comenzara con A, ¿no obtendría una contradicción allí también ? Creo que hay una suposición oculta que se está demostrando por contradicciones de que si de manera similar el mismo proceso en A no llegara a una contradicción , ¿qué tipo de garantías tenemos de que no sucedería? ¿Hay alguna prueba que sea imposible? En otras palabras, si tuviera una Turning Machine (TM) (o super TM) que funcionó para siempre, que intentó todos los pasos lógicos de cada axioma a partir de la afirmación supuestamente verdadera $A$ , lo que garantiza que NO SE DETENGA debido a encontrar una contradicción ?

Luego hice algunas conexiones con mi pregunta anterior con el teorema de incompletitud de Godel que se parece a esto:

Un sistema formal F que exprese aritmética no puede probar su propia consistencia (dentro de F).

Esto básicamente me dejó en claro que si eso es cierto, entonces la consistencia, es decir, garantizar que A y no A no suceda, es imposible. Por lo tanto, parecía que la prueba por contradicción suponía implícitamente que la consistencia está garantizada de alguna manera (de lo contrario, ¿por qué simplemente seguir adelante y concluir que A es verdadero al demostrar que A no es posible si aún no sabía esa consistencia? y la contradicción donde está bien, para cualquier par de afirmación A y no A)? ¿Es esto incorrecto o me perdí algo?

Entonces pensé, ok, solo incluyamos en nuestros axiomas la regla del medio excluido y luego se resuelven todos los problemas. Pero luego me di cuenta, espera si hacemos eso, solo estamos definiendo el problema en lugar de tratarlo. Si simplemente obligo a mi sistema a ser consistente por definición, eso no significa necesariamente que en realidad sea consistente ... ¿verdad? Solo estoy tratando de dar sentido a estas ideas y no estoy muy seguro de qué hacer, pero esto es lo que me estoy dando cuenta después de unos días de leer cosas y ver videos en casi todos los aspectos de estos conceptos, contradicciones, medios exclusivos, lógica intuicionista, teoremas de integridad e incompletitud de Godel ...

En relación con esto, parece que es esencialmente imposible probar directamente que algo es falso sin la regla del medio excluido (o contradicción). Parece que los sistemas de prueba son buenos para probar declaraciones verdaderas, pero a mi entender son incapaces de mostrar directamente que las cosas son falsas. Quizás la forma en que lo hacen es más indirectamente con contradicción (cuando muestran que algo debe ser falso o que suceden cosas malas), o excluido en el medio (donde conocer el valor de verdad de un solo A o no A nos da la verdad del otro) o proporcionando ejemplos de contador (que básicamente muestra que lo contrario es cierto, por lo que indirectamente usa la ley del medio excluido). ¿Supongo que quizás realmente quiero una prueba constructiva de que algo es falso?

Creo que si pudiera saber que si pruebo que A no es falso (digamos que acepto la contradicción), entonces está bien y no necesito aplicar todas las reglas de inferencia y axiomas infinitamente en A y estoy seguro de que A ganó No se llega a una contradicción. Si eso fuera cierto, entonces creo que podría aceptar pruebas por contradicción más fácilmente. ¿Es esto cierto o la segunda incompletitud de Godel garantiza que no puedo tener esto? Si no puedo tener esto, entonces, ¿qué me sorprende es cómo es posible que tantos años de matemáticos hagan matemáticas que no hayamos encontrado una inconsistencia? ¿Necesito confiar en evidencia empírica de consistencia? O, por ejemplo, I prof F es consistente al mostrar superF prueba F pero dado que nunca necesitaré superF y solo F, ¿no puedo ser contenido que realmente funcione?

Acabo de notar que mi queja también se generaliza a las pruebas directas. Ok, si hice una prueba directa de A, entonces sé que A es cierto ... pero, ¿cómo sé que si hiciera una prueba directa de A, no obtendría una prueba correcta? Parece la misma pregunta solo un énfasis ligeramente diferente ...

Usted preguntó (estoy haciendo su pregunta un poco más clara): "¿Qué garantía formal hay de que no puede suceder que tanto como conduzcan a una contradicción?" Parece preocuparle que si la lógica es inconsistente, entonces la prueba por contradicción es problemática. Pero este no es el caso en absoluto.$\lnot p$$p$

Si la lógica es inconsistente, la prueba por contradicción sigue siendo una regla válida de razonamiento, pero también lo es su negación, y la regla que dice que de podemos concluir que usted es el próximo papa. Una inconsistencia en la lógica no invalida nada: todo lo contrario, ¡valida todo !$1 + 1 = 2$

Hay otra posible fuente de confusión: el título de su pregunta puede leerse como que implica que la ley del medio excluido dice que la lógica es coherente. Eso es incorrecto. La coherencia de la lógica equivale a "no es el caso de que tanto una declaración como su negación tengan pruebas", mientras que el medio excluido es la regla que nos permite probar declaraciones de la forma .$p \lor \lnot p$

Suplementario: no entiendo por qué esta pregunta está generando tanta discusión. Tengo problemas para comprender cuál es el dilema en realidad, y por lo que puedo decir, la pregunta surge de algún tipo de malentendido. Si alguien puede aclarar la pregunta, se lo agradeceré. Además, me gustaría llamar la atención sobre los siguientes puntos:

1. La prueba por contradicción y el medio excluido son equivalentes entre sí, por lo que el título, tal como está escrito, no tiene sentido. Por supuesto, no podemos tener uno sin el otro, son equivalentes.

2. Por lo que puedo entender de la larga discusión en la pregunta, el OP parece estar diciendo, o preocupado, que una inconsistencia en la lógica invalida una prueba. Esto es falso, como señalé anteriormente. Agradecería algún tipo de respuesta del OP: ¿puede el OP ver cómo una inconsistencia en la lógica (es decir, poder probar todo) no invalida ninguna prueba?

3. Creo que es probable, pero no puedo decir con certeza, que el OP cree que la ley de los estados intermedios excluidos que es imposible para y (con una fórmula: ). Esto no está excluido medio. A veces se le llama la ley de no contradicción, y es demostrable (sin exclusión del medio).¬ p ¬ ( p ∧ ¬ p $p$$\lnot p$$\lnot (p \land \lnot p)$

4. El OP piensa que es "imposible probar directamente que algo es falso sin un medio excluido". Él es prueba confusa de negación y prueba por contradicción, que no son lo mismo . La publicación vinculada tiene muchos ejemplos de pruebas constructivas de que algo es falso. De hecho, la mayoría de las pruebas de que algo es falso encontrado en los libros de texto ya son constructivas.

5. La incompletitud de Gödel se arrastra por una razón que puedo discernir. La incompletitud de Gödel proporciona una oración tal que ni ni son demostrables. ¡Esto no implica que no sea demostrable (es, por una simple aplicación de medio excluido)! Tampoco implica que contenga, o algo así. Entonces, ¿cómo es relevante la incompletitud de Gödel aquí?G ¬ G G ∨ ¬ G ¬ G ∧ ¬ ¬ $G$$G$$\lnot G$$G \lor \lnot G$$\lnot G \land \lnot\lnot G$

PD: Pido disculpas por la versión anterior del suplemento que fue grosero.

Creo que su pregunta se reduce a "al hacer una verificación formal con algún tipo de lógica formal, ¿qué tipo de garantía tengo de que la lógica es coherente?". Y la respuesta es: ninguno. Eso es algo que debes asumir. La verificación formal no elimina todos los supuestos; solo te ayuda a ser más claro acerca de lo que estás asumiendo, y tal vez te ayuda a asegurarte de comenzar con suposiciones que parecen razonables.

Si trabaja dentro de una lógica estándar, por lo general, la mayoría de las personas están felices de asumir que la lógica es consistente, incluso si no tienen una prueba de ese hecho. Es cierto que algún día podríamos descubrir que la lógica es realmente inconsistente ... pero la mayoría de la gente cree que esto no es muy probable.

En algunos casos, se puede demostrar que una lógica es consistente, pero eso requiere el uso de otra lógica más poderosa, donde debemos suponer que la segunda lógica es consistente, por lo que todavía tenemos que hacer algunas suposiciones (supongamos que alguna lógica es consistente ) Esto podría tomarse como evidencia de que la primera lógica es probable que sea consistente, si crees que la segunda lógica es probablemente consistente, pero el razonamiento tiene que tocar fondo en alguna parte: hay algunas cosas que debemos asumir y no podemos probar.

Ver, por ejemplo, el segundo problema de Hilbert y esta discusión sobre la consistencia de ZFC (y esto y esto y esto y probablemente muchos más).

Hay muchos puntos filosóficos interesantes que toca su publicación.

Consistencia de la lógica booleana

La cuestión de la coherencia de la teoría de la prueba en la lógica clásica no es tan grave como parece. Básicamente se reduce a lo siguiente:

Podemos definir la lógica booleana como una colección de funciones de operaciones lógicas en los valores de verdad 1y 0. ¿Pero cómo sabemos eso 0≠1?

(tenga en cuenta que simplemente estoy usando 0y 1como símbolos abstractos para los dos valores de verdad; en particular, no estoy asumiendo ninguna noción de entero aquí)

Nosotros, por supuesto, no sabemos que 0y 1somos diferentes. Pero la lógica booleana es tan ridículamente simple que rechazar esta posibilidad es un nivel extremo de escepticismo.

Pero la lógica proposicional clásica se reduce a esto. Recuerde que podemos asignar valores booleanos a las proposiciones atómicas de cualquier manera, y esto se extiende a la asignación de un valor a todas las proposiciones que pueden construirse a partir de las atómicas.

La afirmación "de Pusted puede deducir Q" es literalmente solo una relación de orden; significa lo mismo que la afirmación que "se v(P) ≤ v(Q)cumple para cada función que vasigna valores de verdad a las proposiciones atómicas".

Las reglas de inferencia para la lógica proposicional son precisamente las propiedades para trabajar con el ordenamiento ≤. Prueba de contradicción, en particular, es la observación de que si P ≤ 0, entonces P = 0.

Y volviendo a su problema ... si supiéramos ambos P ≤ 0y ¬P ≤ 0, después de conectar los valores de verdad, finalmente concluiríamos eso 0=1; que verdadero y falso significan lo mismo.

Entonces, si tiene confianza en que "verdadero" y "falso" significan cosas diferentes, entonces debe tener una confianza similar en la coherencia de la lógica booleana.

Prueba por contradicción en la lógica intuicionista

Hay que tener en cuenta que la prueba por contradicción se formula mejor como:

• Si puede derivar contradicciones de P, entonces concluya¬P

De hecho, uno podría definir directamente la negación como la conectiva con esta propiedad. Por ejemplo, en álgebra de Heyting , generalmente verá ¬P definido para significar P → 0.

Tenga en cuenta, en particular, el caso especial

• Si puede derivar contradicciones de ¬P, entonces concluya¬¬P

Lo que usted describió como "prueba por contradicción" proviene de identificarse ¬¬Pcon P. La lógica intuicionista no supone que sean equivalentes.

La consistencia como un contrato formal

Hay más formalismos computacionales para la lógica de codificación; ver cálculo lambda simplemente tipado, tipos dependientes, y en particular el paradigma de "proposiciones como tipos".

Sin entrar en detalles, la contradicción se trata básicamente como un contrato formal. Hay un tipo, al que llamaré 0, y existe el contrato "estas funciones no pueden usarse para construir un elemento de tipo 0".

Si un sistema de este tipo es tan audaz como para permitirle construir una función T → 0, entonces si realmente cumple el contrato, significa que es igualmente imposible construir objetos de tipo T. Este es un punto de vista computacional sobre lo que significa una prueba por contradicción.

En última instancia, esto no es muy diferente de, por ejemplo, una función C que devuelve un puntero que promete no devolver un puntero nulo, o una función C ++ que promete no lanzar una excepción.

Y yendo al círculo completo, volviendo a la lógica clásica, eso es realmente lo que estamos haciendo.

Se nos ofrecen contratos formales, como "a partir de los axiomas de Peano, las reglas de inferencia no le permitirán derivar una contradicción". Si este contrato realmente se confirma, entonces si fue capaz de demostrar que ¬Pimplica una contradicción, entonces Pno puede implicar también una contradicción.

Y si fuera posible violar el contrato, simplemente diríamos "los axiomas de Peano son inconsistentes".

Cuando se utiliza para garantizar la verdad de una declaración formal, todas las pruebas asumen implícitamente la consistencia del sistema en el que se basan. Esto se debe a que si el sistema es inconsistente, todo el sistema está roto y todo el trabajo que hicimos en ese sistema es básicamente basura.

Debido a que no podemos probar que ningún sistema (o al menos cualquier sistema complejo) sea consistente dentro de los límites de ese sistema, debemos tomarlo como una verdad empírica en lugar de una verdad formalmente comprobable. Básicamente, si los matemáticos pasan mucho tiempo trabajando con un sistema formal y nunca se descubre ninguna contradicción, entonces eso es evidencia empírica a favor de la consistencia del sistema. Además, podemos usar un sistema más poderoso para probar la consistencia del sistema con el que estamos trabajando (aunque la consistencia de este sistema más poderoso aún sería empírica: el dinero se detiene en alguna parte).

En esencia, la situación en matemáticas es idéntica a la de la ciencia. Construimos matemáticas basadas en teorías que parecen correctas basadas en toda la información que tenemos disponible sobre esas teorías, y como en la ciencia, no puede probar que una teoría sea correcta; solo puedes probar que es incorrecto.

$S$

No importa en qué sistema de axiomas elijamos basar las matemáticas, siempre existe el peligro de que descubramos una contradicción en ese sistema. Esta es exactamente la razón por la cual los matemáticos no introducen nuevos axiomas en las matemáticas: cada nuevo axioma tiene la posibilidad de ser incompatible con los axiomas que ya están en uso, y todo el trabajo que usa el nuevo axioma tendría que ser reevaluado por completo.

Anexo: Cuando hablo de que una declaración es verdadera para un sistema dado, quiero decir que no se puede refutar dentro de ese sistema si ese sistema es consistente.