Database: Idempotence of conjunction

Proposition 61: Idempotence of conjunction (inference rule)

(a) Given that \phi holds, we may infer that the conjunction \phi \wedge \phi holds: \cfrac{\vdash \phi}{\vdash (\phi \wedge \phi)}. (b) Given that \phi \wedge \phi holds, we may infer that \phi holds: \cfrac{\vdash (\phi \wedge \phi)}{\vdash \phi }.

Proof: (a): Using that \phi holds as both of the premises required in conjunction introduction, we infer that \phi \wedge \phi holds.

(b): We infer by conjunction elimination that \phi holds. \square

This database entry builds on the following:

  1. Terminology: Class, statement
  2. Definition: Conjunction
  3. Terminology: Inference
  4. Terminology: Inference rule
  5. Inference rule: Conjunction introduction
  6. Inference rule: Conjunction elimination