El tema de las creencias de Aristóteles es algo complejo, y me limitaré a enlazar un artículo de la Enciclopedia Stanford: La tradicional plaza de la oposición .
La respuesta a la pregunta principal depende del tipo de lógica constructiva que empleemos. En lo que suele llamarse lógica constructiva "intuicionista", tenemos una regla llamada " principio de explosión "(también llamado ex falso quodlibet ), que dice que si se puede demostrar una contradicción entonces, a partir de ésta, podemos concluir cualquier fórmula que deseemos. Esta regla también está presente en la lógica clásica, pero no es tan fuerte constructivamente como en la lógica clásica, porque no tenemos medio excluido en los sistemas constructivos. Sin embargo, algunas variedades más débiles de la lógica constructiva hacen no incluyen el principio de explosión.
Supongamos que aceptamos ese principio. He aquí cómo demostrar "Todos los unicornios tienen alas" en el estilo constructivo informal habitual, suponiendo que sabemos que no hay unicornios. Saber que no hay unicornios, constructivamente, significa que tenemos un método para derivar una contradicción de cualquier prueba de "hay un unicornio".
A continuación tenemos que pensar en el significado constructivo de "Todos los unicornios tienen alas". Demostrar constructivamente que "Todos los unicornios tienen alas" significa producir un procedimiento que, dado un objeto $x$ y una prueba de que $x$ es un unicornio, produce una prueba de que $x$ tiene alas. Esto está relacionado con el Interpretación de BHK de la lógica constructiva.
Uno de estos procedimientos es el siguiente:
- En primer lugar, supongamos que nos dan una prueba de que algún objeto $x$ es un unicornio. En particular, tenemos una prueba de "hay un unicornio".
- Pero sabemos que no hay unicornios. En otras palabras, conocemos alguna prueba de una contradicción de "hay un unicornio".
- Por lo tanto, podemos derivar una contradicción de (1) y (2).
- Por último, utilizamos el principio de explosión, que dice en particular que de una contradicción podemos concluir " $x$ tiene alas".
En general, este procedimiento da una prueba de " $x$ tiene alas" de cualquier prueba de " $x$ es un unicornio". Esto significa que podemos demostrar que "Todo unicornio tiene alas" constructivamente, si asumimos el principio de explosión.
Otra aproximación a esto es ignorar el cuantificador, y trabajar en lógica constructiva proposicional. En este caso suponemos $\lnot U$ (algo no es un unicornio) y quieren demostrar $W$ (que algo tiene alas). Así que queremos ver el esquema $$ (\lnot U) \to (U \to W). $$ Este esquema es demostrable en lógica proposicional intuicionista (que incluye el principio de explosión), pero no es demostrable en lógica mínima que es una forma más débil de lógica constructiva sin el principio de explosión.
La prueba de la identidad $(\lnot U) \to (U \to W)$ en la lógica intuicionista es en realidad muy simple. $\lnot U$ significa $U \to \bot$ , donde $\bot$ es un símbolo para una declaración contradictoria, y el principio de explosión dice que podemos asumir $\bot \to W$ . A continuación, obtenemos $U \to W$ de $U \to \bot$ et $\bot \to W$ aplicando la regla de inferencia de _silogismo hipotético_ que es constructivamente aceptable.
