Modern Logic: Since Gödel: Gentzen

views updated

MODERN LOGIC: SINCE GÖDEL: GENTZEN

The first systematic formulations of the propositional and predicate calculi were presented axiomatically, on the analogy of certain branches of mathematics. In 1934, Gerhard Gentzen (1909–1945), a logician of Hilbert's school, published a formalization of logical principles more in accordance with the way in which these principles are customarily applied. (A similar approach was developed independently by S. Jaśkowski; see below, section on Polish logicians.) In illustrating his technique Gentzen considered how we might establish as valid the schema (X ∨ (Y & Z )) ⊃ (X ∨ Y ) & (X ∨ Z ). Assuming that the antecedent holds, either X is true, or Y & Z is true. In the former case we can pass to each of X ∨ Y and X ∨ Z and hence to their joint assertion. Assuming now Y & Z, we may infer Y, whence X ∨ Y, and likewise Z, whence X ∨ Z. In this case the conjunction is once more derivable. Since it is derivable from each disjunct of the original assumption, we may assert the implication unconditionally.

In this simple form of argument the justification of the schema has been broken down into a series of uncomplicated steps, each involving either the introduction or the elimination of a logical connective. Extracting the rules that were applied and supplementing them with similar rules governing the use of the other connectives, we arrive at a system of "natural" deduction—either NJ (intuitionist logic) or NK (classical logic). Gentzen considered the former more natural than the latter, but whichever we opt for, it appears that the resultant codification of logical principles is more natural, on at least two counts, than a codification presented in axiomatic fashion.

In the first place, we avoid the devious moves that may be necessary to establish a logical principle from an axiomatic basis and follow more closely a pattern of reasoning that we should intuitively adopt. In the second place, the conception of logic as a system of axioms and theorems adjoined to some given subject matter appears inappropriate, since, in their application to, say, a branch of mathematics, principles of logic function not as true statements forming part of the theory in question but as rules of inference allowing us to establish relations of consequence between propositions of the theory.

In addition to the systems NJ and NK, Gentzen devised related formalizations of logic, the L -systems, in which derivable formulas are shown to possess a particularly direct form of proof. These systems contain the "cut" rule, a generalized form of modus ponens that, like modus ponens, has the disadvantage that we cannot work back from a schema to premises from which it could have been derived. However, although the cut rule is crucial in showing the equivalence of the L -systems with the earlier N -systems, Gentzen showed that the cut rule can be eliminated from any proof in the L -systems. This powerful metatheorem simplifies the reconstruction of proofs of valid formulas, yielding a decision procedure for the propositional fragments of LJ and LK and greatly facilitating the search for proofs in the full calculi. Gentzen further applied his Hauptsatz to proofs of consistency; in particular, he showed one formalization of arithmetic to be noncontradictory. The formalization in question does not contain a schema of unrestricted induction, but in later works Gentzen remedied this defect, overcoming the obstacle to such proofs presented by Gödel's results by making use of a principle of transfinite induction which cannot be reduced to ordinary induction within the system. It is a matter of controversy whether such a proof represents the attainment of one of Hilbert's goals, a finitary consistency proof for classical number theory.