Una regla de inferencia (prueba por casos) que permite derivar C a partir de A ∨ B junto con una derivación de C bajo la suposición A y otra derivación de C bajo la suposición B. Formalmente: de A ∨ B, [A ⇒ C], [B ⇒ C] inferir C.

Principio

Si una conclusión se sigue de cada disyunto por separado, y al menos un disyunto se cumple, entonces la conclusión se cumple incondicionalmente; la eliminación de la disyunción transfiere consecuencias por casos a una consecuencia global.

Demostración

Dado A ∨ B, asume A y deriva C; asume B y deriva C; luego descarga las suposiciones para concluir C. Ejemplo: de «Hace sol ∨ está nublado», y las pruebas «si hace sol entonces picnic» y «si está nublado entonces picnic», concluye «picnic».

Aplicación incorrecta

Aplicar la eliminación de la disyunción sin proporcionar derivaciones separadas válidas para cada disyunto, o usarla con una disyunción infinita o mal formada sin abordar cómo los casos cubren todas las posibilidades; también usarla para inferir información específica de un caso que no es común a todos los casos.

Consecuencia

Facilita el razonamiento riguroso por casos y la eliminación de alternativas una vez que se demuestra una consecuencia común; central en pruebas estructuradas, pattern matching de programas y tácticas de demostración en asistentes de pruebas.

Inversión

Contrasta con la introducción de la disyunción: ésta crea una disyunción a partir de un hecho único, mientras que la eliminación resuelve una disyunción en una sola consecuencia; una reversión incorrecta intentaría derivar disyuntos a partir de la consecuencia global sin justificación.

Límite

Válida en los sistemas de prueba clásicos e intuicionistas; en entornos constructivos se deben suministrar construcciones explícitas para las derivaciones desde cada disyunto, y en lógicas con infinitos disyuntos o alternativas no exclusivas se requiere cuidado adicional para asegurar la cobertura completa de los casos.

Tensión semántica

Aparece tensión entre la eliminación de la disyunción y las lecturas no deterministas o probabilísticas de la disyunción: la prueba por casos requiere cobertura de todas las alternativas lógicas, mientras que otras interpretaciones pueden tratar la disyunción como una elección tentativa o incierta.

Síntesis

La eliminación de la disyunción es la regla que colapsa una alternativa demostrable en una única conclusión mostrando que cada posible caso implica esa conclusión; operacionaliza el razonamiento por casos y es indispensable para combinar análisis de casos en resultados incondicionales.