Eliminación de conjunciones

En lógica proposicional , la eliminación de conjunción (también llamada eliminación y , ∧ eliminación , ^[1] o simplificación ) ^{[2] [3] [4]} es una inferencia inmediata válida , una forma de argumento y una regla de inferencia que hace la inferencia de que, si la La conjunción A y B es verdadera, entonces A es verdadera y B es verdadera. La regla permite acortar demostraciones más largas derivando uno de los conjuntos de una conjunción sobre una recta por sí mismo.

Un ejemplo en inglés :

Está lloviendo y llueve a cántaros.

Por eso 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 aparezca una instancia de " " en una línea de una prueba, " " o " " pueden colocarse por sí solas en una línea posterior. El ejemplo anterior en inglés es una aplicación de la primera subregla. ${\displaystyle P\land Q}$ ${\displaystyle P}$ ${\displaystyle Q}$

Notación formal

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 hay un símbolo metalógico que significa que es una consecuencia sintáctica de y también es una consecuencia sintáctica de un sistema lógico ? ${\displaystyle \vdash }$ ${\displaystyle P}$ ${\displaystyle P\land Q}$ ${\displaystyle Q}$ ${\displaystyle P\land Q}$

y expresado como tautologías veritativas o teoremas de lógica proposicional:

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

y

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

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

Referencias

1. David A. Duffy (1991). Principios de la demostración automatizada de teoremas . Nueva York: Wiley.Secc.3.1.2.1, p.46
2. Copi y Cohen ^{[ cita necesaria ]}
3. Moore y Parker ^{[ cita necesaria ]}
4. Hurley ^{[ cita necesaria ]}