Élimination de la conjonction

En calcul des propositions, l'élimination de la conjonction (aussi appelé élimination du et, élimination du [1], ou simplification)[2],[3],[4] est une inférence immédiate[Quoi ?] 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.[pas clair] La règle permet de raccourcir les démonstrations en dérivant l'un des conjontifs[Quoi ?] d'une conjonction sur une ligne[Quoi ?] par lui-même.

La règle est composée de deux sous-règles[Quoi ?] distinctes, qui peuvent être exprimées en langage formel[Comment ?]:

et

Les deux sous-règles signifient en même temps que, chaque fois qu'une instance "" apparaît sur une ligne[Quoi ?] d'une démonstration, soit "", soit "" peut être placé sur une ligne subséquente[Quoi ?] par lui-même[Qui ?].

Notation formelle[pourquoi ?]Modifier

Les sous-règles[Quoi ?] de l'élimination de la conjonction peuvent être écrites en notation séquent[Quoi ?]:

 

et

 

où   est un symbole métalogique[pas clair] qui signifie que   est une déduction logique de   et   est également une conséquence de  

et exprimée en tautologies[Quoi ?] ou en théorèmes de la logique propositionnelle:

 

et

 

où   et   sont des propositions exprimées dans un système formel[Lequel ?].

RéférencesModifier

  1. (en) David A. Duffy, Principles of Automated Theorem Proving, New York, Wiley, Sect.3.1.2.1, p.46
  2. Copi and Cohen [citation nécessaire]
  3. Moore and Parker [citation nécessaire]
  4. Hurley [citation nécessaire]