  In Gentzen’s natural deduction system for first-order logic derivations are written in tree form and based on the well-known rules. For example, implication has the following introduction and elimination rules