Eliminación de la disyunción

En lógica proposicional, la eliminación de la disyunción^[1]​^[2]​^[3]​ (a veces llamada prueba por casos o análisis de casos), es una forma de argumento válido y regla de inferencia que permite la eliminación de un argumento disjunctivo de una prueba lógica. Es la inferencia de que la afirmación ${displaystyle P}$ implica en la afirmación ${displaystyle Q}$ y la afirmación ${displaystyle R}$ también implica ${displaystyle Q}$, por lo tanto, si ${displaystyle P}$ o ${displaystyle R}$ son verdaderos, entonces ${displaystyle Q}$ tiene que ser verdadero. La razón es simple: si al menos una de las afirmaciones P y R son verdaderas, y puesto que al menos una de ellas es suficiente para confirmar Q, entonces Q es ciertamente correcto.

Es decir, la regla se puede definir como:

Donde la regla es que cada vez que las instancias "${displaystyle P o Q}$", y "${displaystyle R o Q}$" y "${displaystyle Plor R}$" aparezcan en una línea de evidencia, "${displaystyle Q}$" puede colocarse en la línea subsiguiente.

La regla para la eliminación de la disyunción puede escribirse en la notación subsiguiente:

donde ${displaystyle vdash }$ es el símbolo metalógico que significa que ${displaystyle Q}$ es una consecuencia sintáctica de ${displaystyle P o Q}$ y ${displaystyle R o Q}$ y ${displaystyle Plor R}$ en algún sistema lógico;

o expresado como una declaración de verdadera tautología funcional o teorema de la lógica proposicional:

donde ${displaystyle P}$, ${displaystyle Q}$ y ${displaystyle R}$ son proposiciones expresadas en algún sistema formal.