 This affects arguments about the semantic significance of natural deduction, and slightly complicates some metatheoretic developments, but Fitch’s negative Int-Elim rules are paired in a way that suffices for analogues of many standard results (as we discuss in  §5.3).  It might be noted that Gentzen’s presentation tends to be preferred by writers on technical proof theory, but Fitch’s presentation by writers of elementary textbooks. People who have learned one presentation of natural deduction often initially find others opaque, but with experience the “translation” becomes routine. The transformation of a proof in one style of natural deduction into one in another is a simple matter of cutting and pasting (or perhaps, since Gentzen’s tree-form presentation often requires multiple copies of some formulas, cutting, photocopying, and pasting). But however natural deduction systems are presented, they have rules of two types. There are rules of inference, by which a formula may be inferred from one or more previous formulas. (Some systems also allow “zero-premiss” rules, by which formulas of specified kinds can be written anywhere desired: in effect, logical axiom schemes.) The typically rules of inference include these: