¿Por qué, lógicamente, es válida la prueba por contradicción?

Sí, bueno, una prueba por contradicción involucra dos reglas de inferencia.

(1) la regla de inferencia de "Introducción de la negación" sostiene que si algo implica una contradicción, entonces debe ser falso, ya que generalmente afirmamos que las contradicciones no son verdaderas y, por lo tanto, no pueden inferirse de cosas verdaderas.

Esto es aceptable tanto en sistemas lógicos intuicionistas como clásicos. Aunque hay otros sistemas (como la lógica mínima) que no lo aceptan.

  ($\def\false{\mathsf F}\def\true{\mathsf T}$Semánticamente, esto se debe a que$\false \to \false$es cierto mientras$\true\to\false$Es falso. Esto lleva a algunos sistemas a definir la negación como$\neg \phi ~\equiv~ \phi\to\mathsf F$.)

(2) la regla de "eliminación de doble negación" es que si la negación de una premisa es falsa, entonces la premisa debe ser verdadera. Esto no se acepta en la lógica intuicionista, pero sí en la lógica clásica.

(3) Combinando estas reglas damos el esquema para una prueba por contradicción: suponer una negación de un predicado, demostrar que se infiere una contradicción, deduciendo así que el predicado es verdadero.

Muchos de los problemas que describí aquí se muestran en esta sesión de preguntas y respuestas.

Primero, seamos claros de lo que estamos hablando. Hay dos reglas que a menudo se denominan "prueba por contradicción". La primera, introducción de negación, se puede escribir como$\cfrac{\varphi\vdash\bot}{\vdash\neg\varphi}$que se puede leer como "si podemos derivar que$\varphi$implica falsedad, entonces podemos deducir$\neg\varphi$". También podríamos escribir esto como un axioma:$(\varphi\Rightarrow\bot)\Rightarrow\neg\varphi$. Por alguna razón, así es como Bram28 ha tomado tu declaración, pero no creo que tengas ningún problema con esto. Dirías, "bueno, claramente si asumimos$\varphi$conduce a una contradicción entonces$\varphi$debe haber sido falso y por lo tanto$\neg\varphi$es verdadera". Hay otra regla, más apropiadamente llamada "prueba por contradicción", que se puede escribir$\cfrac{\neg\varphi\vdash\bot}{\vdash\varphi}$o como un axioma$(\neg\varphi\Rightarrow\bot)\Rightarrow\varphi$. Esto parece ser con lo que estás en desacuerdo. Dado que esta última regla ha sido rechazada por muchos matemáticos (constructivistas de varios tipos), no estaría completamente loco si la cuestionara. (En débil defensa de Bram28, probablemente aceptaría "sustituyendo$\neg\psi$en lo anterior, por el mismo argumento podemos demostrar que$\neg\psi$es falso entonces$\psi$es cierto", pero la regla solo muestra que$\neg\neg\psi$es verdad. La regla que le permite pasar de$\neg\neg\psi$a$\psi$es, de hecho, equivalente a la prueba por contradicción.)

Para ser aún más claro sobre lo que estamos hablando, debemos distinguir la sintaxis de la semántica. Si estamos hablando de "reglas de inferencia" o "pruebas", generalmente estamos pensando sintácticamente. Es decir, estamos pensando en símbolos en una página y reglas para manipular esas colecciones de símbolos en otras colecciones de símbolos o reglas sobre lo que constituye arreglos "correctos" de los símbolos, es decir, una prueba. (Las versiones más informales serán oraciones en un lenguaje natural que sigan las "reglas de la razón", pero la idea sigue siendo que la formadel argumento es lo que lo hace válido). La semántica, por otro lado, interpreta esos símbolos como objetos matemáticos y luego decimos que una fórmula (es decir, la disposición de los símbolos) es "verdadera" si se interpreta como un objeto matemático que satisface algunos requisitos dados. propiedad. Por ejemplo, decimos que una fórmula de la lógica proposicional clásica es "verdadera" si su interpretación como función booleana es la constante$1$función.

Entonces, tenemos dos posibles lecturas de su pregunta: 1) ¿Por qué la regla es$\cfrac{\neg\varphi\vdash\bot}{\vdash\varphi}$¿derivado? 2) ¿Por qué es la regla$\cfrac{\neg\varphi\vdash\bot}{\vdash\varphi}$"verdadero"?

Para (1), una respuesta muy insatisfactoria es que a menudo se toma como dada, es decir, es derivable por definición de la lógica. Una respuesta un poco más satisfactoria es la siguiente. Dada una lógica constructiva donde esa regla no es derivable pero la mayoría de las otras reglas "usuales" sí lo son, podemos mostrar que si para todas las fórmulas$\varphi$,$\vdash\varphi\lor\neg\varphi$es derivable, entonces podemos derivar la regla$\cfrac{\neg\varphi\vdash\bot}{\vdash\varphi}$(y viceversa). Otra forma de decir esto es que$\varphi\lor\neg\varphi$es probablemente equivalente a$(\neg\varphi\Rightarrow\bot)\Rightarrow\varphi$. También es demostrablemente equivalente a$\neg\neg\varphi\Rightarrow\varphi$. el axioma$\varphi\lor\neg\varphi$se describe a menudo como "todo es verdadero o falso". Esto no es exactamente lo que significa, pero esta idea de que todo es "verdadero o falso" a menudo se considera intuitivamente obvia. Sin embargo, no hay duda de si$\varphi$es "verdadero" o "falso" en lo anterior. Tenemos reglas para construir pruebas a partir de otras pruebas, y eso es todo lo que hay en esta perspectiva.

Para (2), si usa la semántica de "tabla de verdad" de la lógica proposicional clásica, entonces simplemente calcula. Simplemente necesita demostrar que$(\neg\varphi\Rightarrow\bot)\Rightarrow\varphi$cuando se interpreta es el constantemente$1$funcionan cuando ambos$0$y$1$se sustituyen en la interpretación de la fórmula. Puedes mostrar esto fácilmente. En esta semántica, "prueba por contradicción" es simplemente "verdadero". Cuestionar esto requiere cuestionar la semántica. Una cosa es cuestionar si solo hay dos valores de verdad,$0$y$1$. ¿Por qué no tres o un número infinito de ellos? Esto conduce a lógicas multivaluadas. Alternativamente, podríamos mantener los mismos valores de verdad, pero interpretar las fórmulas como algo diferente a las funciones booleanas. Por ejemplo, podríamos decir que son funciones booleanas pero solo permitimos monótonas, o podríamos decir que son relaciones booleanas totales . Hacer estos cambios requiere adaptar la noción de "verdadero". Para el último ejemplo, podemos decir que una fórmula es "verdadera" si se interpreta como una relación que relaciona todas las entradas booleanas con$1$. Sin embargo, al ser una relación y no solo una función, esto no impide que también relacione algunas o todas las entradas con$0$, es decir, algo puede ser tanto "verdadero" como "falso".

Cambiar la semántica afecta qué reglas y axiomas son sólidos. Una regla o axioma es válido con respecto a una semántica dada, si su interpretación es "verdadera" en esa semántica.$(\neg\varphi\Rightarrow\bot)\Rightarrow\varphi$es sólido con respecto a las "tablas de verdad", pero no con respecto a muchas otras semánticas posibles.

Para resumir, si está trabajando con respecto a la semántica de "tabla de verdad", entonces "prueba por contradicción" es simplemente "verdadera", es decir, cuando se interpreta, se interpreta como una función booleana constantemente "verdadera", y esto puede ser fácilmente calculado. En este caso, todas sus "suposiciones lógicas" están integradas en la noción de semántica de "tabla de verdad". Con respecto a la semántica, la "prueba" es irrelevante. La prueba es un concepto sintáctico. Su discusión sobre "asumir que la premisa es falsa" es (ligeramente distorsionada) una charla teórica de prueba. Con un enfoque semántico, no se puede "suponer que la premisa es verdadera/falsa", ni la fórmula se interpreta como "verdadera" (es decir, una constante$1$función) o no. (Puede tener suposiciones metalógicas de que alguna fórmula es "verdadera", pero esto está sucediendo fuera de la lógica. En última instancia, la moneda del reino matemático es la noción más sintáctica de prueba y la semántica simplemente empuja la prueba a la meta-lógica. )

Es porque la propuesta$(\neg P \Rightarrow (Q \wedge \neg Q)) \Rightarrow P$es una tautología, lo que significa que siempre es cierto sin importar los valores de verdad de$P$y$Q$.

La tautología está diciendo "Si lo contrario de$P$implica algo imposible, entonces$P$."

Funciona de la siguiente manera:

Digamos que tiene un conjunto de declaraciones$\Gamma$, y queremos inferir$\neg \phi$, y lo hacemos mediante una prueba por contradicción.

Así, suponemos$\phi$, y mostrar que eso conduce a una contradicción.

Esto significa que$\Gamma$, Juntos con$\phi$implica lógicamente una contradicción, es decir

y eso significa que es imposible establecer todas las declaraciones en$\Gamma \cup \phi$a la verdad Pero eso también significa que si todas las declaraciones en$\Gamma$son verdaderas,$\phi$tendrá que ser falso, es decir$\neg \phi$tendrá que ser cierto. Y así tenemos

Así, en efecto, hemos probado$\neg \phi$