Formal proofs with CONDITIONALS ⟨10,02⟩

Let's see how proofs involving conditionals work in a natural deduction system.

Every symbol comes with two rules: a rule for introduction, and a rule for elimination. Since we're concerned with two sorts of conditionals (the material conditional (→) and the biconditional (↔)), we have four kinds of formal proof to look at.

Here they are:

→-elim (modus ponens):
Given (P→Q) and P, derive Q

→-intro:
Assume P, show Q follows, and derive (P→Q).

↔-elim:
From (P↔Q) and Q/P, derive P/Q.

↔-intro:
Assume P, show Q; assume Q, show P; derive (P↔Q).

Note that (P↔Q) is equivalent with ((P→Q) ∧ (Q→P)), and so the ↔-intro rule is equivalent with two applications of →-intro plus one application of ∧-intro.

And that's it!

[giorgossakkatos]

that's some next level teaching. You do a huge service to students taking up Logic as a course by helping clear things up. Thanks a million!