¿Cuál es la intuición detrás del uso de la Ley del Medio Excluido en la Deducción Natural?

La ley del tercero excluido es algo similar a un análisis de casos (por ejemplo, para una serie alterna de casos pares, impares). En este caso, la intuición detrás de la ley del tercero excluido es que uno de los casos es trivial: ¬φ ⊢ ∃x. (φ → ψ)

Como es habitual, cada uno de los casos es más sencillo que la pregunta original. Esto es especialmente cierto aquí: como el caso anterior es trivial, solo queda mostrar el otro caso, por lo que, en general, obtiene una hipótesis (es decir, φ) de forma gratuita que puede usar en su deducción.

Según la respuesta anterior de @Sudix, la intuición detrás del uso de la Ley del Medio Excluido en la prueba de:

$(φ → ∃x ψ) ⊢ ∃x (φ → ψ)$

es aplicar un "análisis de caso".

(i) Suponga que$φ$no se sostiene, es decir, se supone$¬φ$.

Esto significa (por la tabla de verdad para el condicional ) que$φ → ψ$es VERDADERO, y por lo tanto también$∃x (φ → ψ)$es verdad.

(ii) Suponga ahora que$φ$sostiene, es decir, asume$φ$.

Sabemos que la premisa$(φ → ∃x ψ)$tiene, y esto significa (nuevamente por la tabla de verdad para el condicional ) que también$∃x ψ$es VERDADERO, es decir que$ψ$es VERDADERO para algunos$x$.

De este modo,$φ → ψ$es VERDADERO para algunos$x$, es decir$∃x (φ → ψ)$es verdad.

No lo llamaría un 'truco' sino una buena 'estrategia', y con el tiempo, a medida que hagas más y más de estas pruebas, comenzarás a reconocer los momentos en los que usas la Ley de Sería bueno usar Excluded Middle ... y en qué declaración usarlo.

También me gustaría señalar que el hecho de que alguna prueba funcione usando la Ley del Medio Excluido no significa que necesites la Ley del Medio Excluido. En otras palabras, no deberías sentir que no podrías completar la prueba si no pensaras en usar Excluded Middle.

De hecho, en este caso, también puedes hacer una prueba por contradicción:

Para una intuición, uno podría pensar en un ejemplo o modelo de la ley del tercero excluido, por ejemplo, el conjunto de todos los subconjuntos$P(X)$de un conjunto$X$cuando se trata de un$\phi$el conjunto$P_\phi:=\{x\in X | \phi(x) \}$de todos los elementos$x$en$X$para cual$\phi(x)$es verdad e interpretando$\neg \phi$como el complemento$(P_\phi)^c:=\{x\in X|x\not\in P_\phi\}$, además$\land$se interpreta como$\cap$y$\lor$como$\cup$(este es también el ejemplo estándar de un álgebra booleana ).

Esta estructura obedece a la ley del tercero excluido , porque en esta estructura para cualquier$A\in P(X)$sostiene que$X=A\cup A^c$, es decir, cualquier elemento$x\in X$está en$A$o esta en el complemento$A^c$.

Por cierto, no todas las estructuras obedecen la ley del medio excluido, por ejemplo, un álgebra de Heyting en general no es un modelo de la ley del medio excluido. Un ejemplo estándar de álgebra de Heyting es, por ejemplo, el conjunto de subconjuntos abiertos de un espacio topológico (con$\neg$interpretado como parte interna del complemento ).