eliminación de conjunciones

En lógica proposicional , la eliminación de conjunciones (también llamada eliminación de conjunciones , eliminación de ∧ , ^{[ 1 ]} o simplificación ) ^{[ 2 ] [ 3 ] [ 4 ]} es una inferencia inmediata válida , una forma de argumento y una regla de inferencia que permite inferir que , si la conjunción A y B es verdadera, entonces A es verdadera y B es verdadera. Esta regla permite acortar demostraciones más largas al derivar uno de los componentes de una conjunción en una línea aparte.

Un ejemplo en inglés :

Está lloviendo a cántaros.

Por lo tanto, está lloviendo.

La regla consta de dos subreglas separadas, que pueden expresarse en lenguaje formal como:

${\displaystyle {\frac {P\land Q}{\therefore P}}}$

y

${\displaystyle {\frac {P\land Q}{\therefore Q}}}$

Las dos subreglas juntas significan que, siempre que una instancia de "${\displaystyle P\land Q}$" aparece en una línea de una prueba, ya sea "${\displaystyle P}$" o "${\displaystyle Q}$" puede colocarse en una línea posterior por sí solo. El ejemplo anterior en inglés es una aplicación de la primera subregla.

Las subreglas de eliminación de conjunciones pueden escribirse en notación secuencial :

${\displaystyle (P\land Q)\vdash P}$

y

${\displaystyle (P\land Q)\vdash Q}$

dónde${\displaystyle \vdash }$es un símbolo metalógico que significa que${\displaystyle P}$es una consecuencia sintáctica de${\displaystyle P\land Q}$y${\displaystyle Q}$es también una consecuencia sintáctica de${\displaystyle P\land Q}$en sistema lógico ;

y expresadas como tautologías veritativo-funcionales o teoremas de lógica proposicional:

${\displaystyle (P\land Q)\to P}$

y

${\displaystyle (P\land Q)\to Q}$

dónde${\displaystyle P}$y${\displaystyle Q}$son proposiciones expresadas en algún sistema formal .