Conjunction introduction
If we have a proofstratagie like this, in order to prove a conjunction (P ∧ Q). We need a prove of P
and a proof of Q. We can translate many of these boxes into this form where we use the inference
rule for conjunction to describe if some set of assumptio gamma we can prove P, and from a set
of assumption gamma we can prove Q. Then we know that from some set of assumption gamma
we can prove P ∧ Q.
Conjunction elimination
If we have a prove of P ∧ Q we can always conclude that P holds.
Recall that ¬P behaves just like P ⇒ ⊥. These two rules are really just
instances of the rules for P ⇒ Q, where Q taken to be ⊥.
Similarly, P ⇔ Q behaves the same as P ⇒ Q ∧ Q ⇒ P.
, Conjunction introduction
If you can prove P, than you know that P V Q
holds, if you can prove Q than you know that P
V Q holds.
Conjunction elimination
Suppose we have proven P V Q, to
use a proof we show that some
statement R, if we know that P V Q
holds, if P holds then we can prove R
If Q holds I can prove R, then I can
conclude that R is always going to be
true. Regardless of which of P or Q is
true.
If we know P ∨ Q holds:
− … and we know that R holds whenever P does;
− … and we know that R holds whenever Q does;
− … we can conclude that R must always hold.
Exercise:
Give a proof that ⊢ (P ∨ ⊥) ⇒ P.