Database: Idempotence of conjunction

Proposition 44: 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 \wedge \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: Inference, entailment
  2. Terminology: Inference rule
  3. Definition: Conjunction
  4. Inference rule: Conjunction introduction
  5. Inference rule: Conjunction elimination