É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 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:
et
Les deux sous-règles signifient en même temps que, chaque fois qu'une instance "" apparaît sur une ligne d'une démonstration, soit "", soit "" 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:
et
où est un symbole métalogique qui signifie que est une déduction logique de et est également une conséquence de
et exprimée en tautologies ou en théorèmes de la logique propositionnelle:
et
où et sont des propositions exprimées dans un système formel.
Références
- (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Conjunction elimination » (voir la liste des auteurs).
- (en) David A. Duffy, Principles of Automated Theorem Proving, New York, Wiley, Sect.3.1.2.1, p.46
- Copi and Cohen
- Moore and Parker
- Hurley