A Critical Comparison of Natural Deduction Systems

Natural deduction is the logical system most commonly used in teaching elementary logic. However, different textbooks may adopt different versions of the natural deduction system, which can be quite annoying to many teachers and students of logic. More precisely, with regard to the inference rules for quantifiers, there are two completely different systems of natural deduction. One system (which I shall call the “Gentzen system”) has a rule of “existential instantiation” that looks pretty complicated, whilst the other system (which I shall call the “Copi-Kahane system”) has a much simpler rule for existential instantiation. Although most of the Chinese textbooks for elementary logic use the rules of the Copi-Kahane system, there are still some textbooks for elementary logic or intermediate logic which use the Gentzen system. This leads to some problems especially in teaching logic, as students may find it somehow difficult to learn intermediate logic (which usually use the Gentzen system) if what they learn in elementary logic is the Copi-Kahane system. In this paper, I shall critically compare the Gentzen