¿Por qué se acepta el principio de explosión en la matemática constructiva?

Question

Creo que algo falla en el principio de explosión, porque según éste, si sé $P\wedge \lnot P$ Puedo deducir $Q$ aunque no sé nada sobre $Q$ .

¿Es realmente constructivo decidir si $Q$ es cierto sólo viendo $P$ sin relación con $Q$ ? Si $P\wedge \lnot P$ sostiene, cómo construyo una razón para $Q$ ?

Answer 1

Como ha señalado correctamente @DanielV, el principio de explosión (aka ex falso quodlibet ) sólo dice que $(P \land \lnot P) \to Q$ es válida para cualquier fórmula $Q$ (posiblemente sin relación con $P$ ). Esto no significa que $Q$ se mantiene, pero sólo que si $P \land \lnot P$ celebrada entonces $Q$ (que podría ser cualquier cosa) se mantendría; como en un sistema consistente $P \land \lnot P$ nunca se sostiene, del principio de explosión no podemos inferir si $Q$ se mantiene o no.

Por lo tanto, el principio de explosión no contradice la constructividad, esta es la razón por la que se acepta en un entorno constructivo como la lógica intuicionista. El principio de explosión sólo dice que si una teoría contiene una sola inconsistencia, dicha teoría es trivial, es decir, puede demostrarlo todo. Por lo tanto, según el principio de explosión, sólo hay una teoría inconsistente: la teoría trivial que tiene cada frase como teorema.

Una justificación informal del principio de explosión es la siguiente: si $P$ y su negación $\lnot P$ son ambos asumido, entonces $P$ se mantiene, de lo que se deduce que al menos una de las reivindicaciones $P$ y alguna otra afirmación (arbitraria) $Q$ se mantiene. Sin embargo, como sabemos que $P$ o $Q$ se mantiene, y también que $P$ no se sostiene (es decir, $\lnot P$ se mantiene) podemos concluir que $Q$ sostiene. Este argumento es constructivo, ya que es válido tanto en la lógica clásica como en la lógica intuicionista.

---

Hay lógicas que rechazan el principio de explosión: lógicas paraconsistentes y en particular lógica mínima . Estas lógicas permiten distinguir entre teorías inconsistentes y razonar con ellas. La idea es que debería ser posible razonar con información incoherente de forma controlada y discriminatoria, algo que impide el principio de explosión.

Para más información, consulte aquí , aquí y aquí .

Answer 2

En el Interpretación de BHK de la lógica constructiva, una proposición es "verdadera" cuando se proporciona un testigo para ella. Se obtienen diferentes nociones de lógica constructiva definiendo "testigo" de diferentes maneras. Por ejemplo, se podría decir que un testigo es una máquina de Turing que computará la evidencia relevante. Para nuestros propósitos, digamos que para cada proposición asignamos un conjunto de testigos. Pero no lo hacemos de forma arbitraria. Para una variable de proposición, podemos asignar un conjunto de testigos de forma arbitraria, pero, en particular, para $A\to B$ asignamos como conjunto de testigos el espacio de funciones entre el conjunto de testigos de $A$ y el conjunto de testigos de $B$ . Todo esto es para decir, que para este ejemplo, un testigo de una implicación es una función (teórica de conjuntos) de un conjunto de testigos de $A$ a un conjunto de testigos para $B$ . También asignamos el conjunto vacío de testigos a $\bot$ el conectivo nulo para la falsedad correspondiente a una contradicción 1 .

Para la noción particular de "testigo" que acabamos de describir, el principio de explosión es "verdadero" constructivamente porque es atestiguado. En particular, es atestiguado por la función vacía. Para la mayoría de las otras opciones comunes para la noción de "testigo", hay algún análogo de la función vacía. Una forma de generalizar la interpretación BHK, en el caso de la Lógica Proposicional Intuicionista (LPI), es decir que tenemos un Categoría Heyting de testigos y la interpretación BHK es un functor de Heyting desde la categoría sintáctica de Heyting (delgada) que describe la IPL a esa categoría de Heyting de testigos. Las categorías de Heyting tienen objetos iniciales que representan $\bot$ y la flecha única de un objeto inicial a cualquier otro objeto es la generalización de la función de vacío. Siempre que nuestra categoría de testigos tenga un objeto inicial (que se comporte bien en un cierto sentido y tengamos también otras cosas "estructurales"), entonces podemos interpretar la $\bot$ conectivo. Teniendo el $\bot$ medios conectivos que tienen el principio de explosión en la forma $\bot\vdash\varphi$ para todos $\varphi$ .

Por supuesto, podríamos dejar caer $\bot$ y debilitar el requisito de que la categoría de testigos sea Heyting y de que tengamos un functor Heyting para no incluir las cosas del objeto inicial. Eso es algo completamente razonable y llevará a una lógica paraconsistente como la lógica mínima. No se trata tanto de "si apoyamos el principio de explosión" como de "si tenemos (algo equivalente a) el $\bot$ conectivo". Sin embargo, al dejar de lado $\bot$ significa que necesitamos una historia diferente para la negación, $\neg$ o dejar caer la negación por completo. Para las lógicas intuicionistas, la negación suele ser definido como $\neg\varphi\equiv\varphi\to\bot$ .

1 I fuertemente recomiendan proporcionar $\bot$ como conectivo primitivo (para las lógicas donde las contradicciones tienen sentido). Siempre hablando de $P\land\neg P$ es tedioso y un tanto chapucero. ¿Por qué tengo que elegir arbitrariamente alguna proposición irrelevante $P$ ¿sólo para hablar de un concepto fundamental como la contradicción?

Answer 3

Esta es una forma de verlo. Supongamos que estamos trabajando en un sistema de deducción natural con un $\lor$ -regla de eliminación que va $$ \frac{\Gamma\vdash P\lor Q \qquad \Gamma, P\vdash R \qquad \Gamma, Q\vdash R}{\Gamma\vdash R} $$ Esto nos permite demostrar cosas por análisis de casos una vez que hemos demostrado una $\lor$ que nos dice que tenemos que estar en uno de los casos.

Ahora bien, ¿cuál es el fundamental cosa sabiendo $\neg P$ nos dice? Podría decirse que en la regla anterior no necesitará para llevar a cabo la $\Gamma, P\vdash R$ parte de la prueba porque $P$ no puede ocurrir realmente .

Nosotros podría lograr eso al tener un montón de especialistas $\lor$ -Reglas de eliminación como $$ \frac{\Gamma\vdash P\lor Q \qquad \Gamma, P\vdash A \qquad \Gamma\vdash\neg A \qquad \Gamma, Q\vdash R}{\Gamma\vdash R} $$ pero es más simple envolver todas las variantes en una sola regla que diga:

Si te encuentras en una rama de una prueba en la que parecen sostenerse dos cosas contradictorias, significa que esa rama de la prueba no era realmente necesaria, y se te permite cancelarla por completo fingiendo que ya has demostrado lo que pretendías en esa rama.

Eso es básicamente lo que hace el principio de explosión.

Es constructivo aceptable porque intuitivamente sólo hay dos formas de utilizarlo:

1. O bien sus supuestos iniciales en la prueba son imposibles de satisfacer. Entonces no nos importa concluir un sinsentido. Lo que hacer es que si nuestros supuestos se cumplen, la conclusión también lo hará. Si no es así, nos conformamos con meter y sacar basura.

2. O has introducido una suposición temporal adicional en alguna parte del árbol de la prueba que crea la contradicción. Por ejemplo, el $\Gamma,P\vdash R$ premisa en nuestro $\lor$ -la regla de eliminación lo hace. Entonces podemos justificar el uso de la explosión argumentando que la rama en la que ocurrió la explosión no era realmente necesaria porque las condiciones en las que sería relevante no pueden ocurrir.

3. Si el supuesto adicional proviene de un introducción regla como $\to$ -introducción, el argumento de que "esta rama no es necesaria" no es tan inmediatamente convincente. Sin embargo, en ese caso podemos argumentar que seguimos estando "constructivamente seguros", porque entonces nuestra conclusión de esa regla de introducción es algo que implica $\to$ . Y la única manera de que podamos utilice ese resultado es usándolo en modus ponens (también conocido como $\to$ -eliminación). En que vez que alguien alegue que puede probar el antecedente de la $\to$ pero sabemos que no es realista porque la suposición lleva a una contradicción. Así que esto nos dice que la rama de la prueba donde se encuentra el modus ponens será en sí misma una rama innecesaria, por lo que constructivamente no tenemos que preocuparnos por las travesuras allí. Nunca se ejecutará.

   La historia para $\neg$ -La introducción es similar a la de $\to$ -introducción; luego el principio de la explosión mismo es la regla de eliminación correspondiente.