ABSTRACT
A Gentzen system for a logic is another sort of proof theory, similar to natural deduction, but with a number of important differences. Gentzen systems parallel natural deduction systems by having two rules for each connective.1 However, instead of rules for introducing and eliminating connectives in the consequent position, we have rules only for introducing connectives. Connectives are never eliminated by the connective rules. To make up for the loss of one half of our rules, we add new rules to introduce connectives in the antecedent of a consecution. Each connective (barring special cases) will have two rules, one licensing an introduction of that connective in the consequent of the consecution, and the other licensing its introduction in the antecedent. This gives Gentzen systems powerful properties.
