Proof-theoretic Validity and the Completeness of Intuitionistic Logic

Abstract

As has often been claimed, the introduction (I) and elimination (E) rules of intuitionistic natural deduction systems stand in a certain harmony with each other. This can be understood in such a way that once the I rules are given the E rules are uniquely determined and vice versa. The following is an attempt to elaborate this claim. More precisely, we define two notions of validity, one based on I rules (valid+) and one based on E rules (valid−), and show: the E rules generate a maximal valid+ extension of the I rules, and the I rules generate a maximal valid− extension of the E rules. That is to say, the calculus consisting of I and E rules (i.e., intuitionistic logic) is sound and complete with respect to both validity+ and validity−. This does not mean that the syntactical form of E rules is determined by the I rules and vice versa, but that the deductive power which E rules bring about in addition to I rules is exactly what can be justified from I rules and vice versa. Concerning the approach based on I rules this was already claimed by Gentzen who considered I rules to give meanings to the logical signs and the E rules to be consequences thereof (Gentzen, 1935, p. 189).