title: Élimination de la conjonction
text: # Élimination de la conjonction
  
  En calcul des propositions, l'élimination de la conjonction (aussi appelé élimination du et, élimination du ∧, ou $simplification)^,^,$ est une inférence immédiate valide, sous forme d'argument et de règle d'inférence qui rend la conclusion selon laquelle, si la conjonction A et B est vrai, alors A est vrai et B est vrai. La règle permet de raccourcir les démonstrations en dérivant l'un des conjontifs d'une conjonction sur une ligne par lui-même.
  
  La règle est composée de deux sous-règles distinctes, qui peuvent être exprimées en langage formel:
  
      ${\frac {P\land Q}{\therefore P}}$
  
  et
  
      ${\frac {P\land Q}{\therefore Q}}$
  
  Les deux sous-règles signifient en même temps que, chaque fois qu'une instance "$P\land Q$" apparaît sur une ligne d'une démonstration, soit "$P$", soit "$Q$" peut être placé sur une ligne subséquente par lui-même.
  
  ## Notation formelle
  
  Les sous-règles de l'élimination de la conjonction peuvent être écrites en notation séquent:
  
      $(P\land Q)\vdash P$
  
  et
  
      $(P\land Q)\vdash Q$
  
  où $\vdash$ est un symbole métalogique qui signifie que $P$ est une déduction logique de $P\land Q$ et $Q$ est également une conséquence de $P\land Q$
  
  et exprimée en tautologies ou en théorèmes de la logique propositionnelle:
  
      $(P\land Q)\to P$
  
  et
  
      $(P\land Q)\to Q$
  
  où $P$ et $Q$ sont des propositions exprimées dans un système formel.
  
  