Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics

Gentzen's Approach to Meaning

Gentzen's approach to meaning is commonly described by saying that he had the idea that the meaning of a logical constant is determined by its introduction rule in Natural Deduction, or as he put it himself: “the introductions present, so to speak, the 'definitions' of the symbols concerned” (Gentzen 1934–35 [4, p. 189]). However, this should not be confused with what has later become known as inferentialism, the view that the meaning of a sentence is given by the inference rules concerning the sentence that are in force, which was advocated by Carnap (1934) [1] at about the same time. For Gentzen only some of the inference rules are meaning constitutive, viz. the introduction rules. To indicate their special status, a proof or deduction whose last step is an introduction is now commonly called canonical or is said to be in canonical form[1].

Besides introduction rules there are elimination rules and about them Gentzen says “in an elimination we may use the constant only in the sense afforded to it by the introduction of that symbol”. What is intended is clearly that we may use the constant only in this sense, if we are to justify the elimination inference. Gentzen is obviously concerned with what justifies inferences: the introductions stipulate what the logical constants mean, and the eliminations are justified because they are in accord with this meaning.

He clarifies how his ideas are to be understood by giving one example, saying that given an implication AB as premiss, “one can directly infer B when A has been proved, because what AB attests is just the existence of a proof of B from A[2].

Three important principles can be distinguished here. Firstly, what a sentence “attests” is the existence of a canonical proof. An introduction is therefore immediately justified: given proofs of its premisses, the conclusion is warranted, since what the conclusion attests is just that there is a canonical proof of it—the introductions are self-justifying, as one says, when they are taken to be what gives the meanings of the logical constants. Thus, in view of what a sentence attests, a canonical proof is in order, or is valid, provided only that its immediate sub-proofs are.

Secondly, the justification of an elimination consists more precisely in the fact that given that there are proofs of the premisses of the elimination and that the proof of the major premiss is of the kind attested to exist, that is, is in canonical form, a proof of the conclusion can be obtained from these proofs without the use of that elimination. For instance, as Gentzen points out, a proof of the conclusion B of an implication elimination can be obtained from proofs of the premisses if the proof of the major premiss AB is in canonical form, because then there is a proof of B from A, and by replacing the assumption A in that proof by the proof of the minor premiss A, one obtains a proof of B, as is illustrated by the following figure:

[ A] stands for the set of assumptions that are discharged by the exhibited ⊃-introduction in the first figure and become replaced by the proof of A in the second figure. The operation by which the proof to the left is transformed to the one to the right, that is, substituting in the proof of B from A the proof of the minor premiss A for the occurrences of A that belong to [ A], is what is called an ⊃-reduction. These kinds of reductions, which were introduced explicitly in the proof of the normalization theorem for natural deduction (Prawitz 1965 [16]), but which Gentzen was already quite aware of[3], have in this way a semantic import in being what shows the eliminations to be justified. By this way of reducing a proof that ends with an elimination to another proof of the same conclusion, the conclusion of the elimination becomes warranted, provided of course that this other proof is valid. Thus, proofs that end with eliminations are valid, if the proofs that they reduce to by applying certain reductions are valid.

Thirdly, when saying that we get a valid proof of B by making the substitution just described, we are tacitly taking for granted that a valid proof from assumptions remains valid when making such substitutions.

We can in this way extract from Gentzen's example three principles about what makes something a valid proof or a valid deduction, as I prefer to say (since when the term proof is used, it is normally taken for granted that the reasoning is valid, a convention not strictly adhered to in my informal explanations above). The principles are formulated more precisely below, where I have adopted the terminology that a deduction is open when it depends on assumptions and closed when all assumptions are discharged or bound.

Principle I. Introductions preserve validity: a closed deduction in canonical form is valid, if its immediate sub-deductions are.

Principle II. Eliminations are justified by reductions: a closed deduction not in canonical form is valid if it reduces to a valid deduction.

Principle III. An open deduction is valid, if all results of substituting closed valid deductions for its free (undischarged) assumptions are valid.

Because of the fact that the premises of an introduction and the assumptions that an introduction may bind are of lower complexity than that of the conclusion, these principles can be taken as clauses of a generalized inductive definition of the notion of valid deduction, relative to a basic clause stating what is counted as valid deductions of atomic sentences. The effect of defining the notion inductively in this way is that no deduction is valid if its validity does not follow from I–III and that the converses of I–III hold true too.

When taking into account also inferences involving quantified sentences, we have to reckon with inferences that bind free individual variables: for instance, an ∀Iinference in which ∀x A(x ) is inferred from A(a) is said to bind occurrences of the variable a that are free in sentences of the deduction of A(a); the occurrences are said to be bound in the deduction of ∀x A(x ). A deduction is then said to be open/closed if it contains either/neither occurrences of unbound assumptions or/nor occurrences of unbound variables. Accordingly, in principle III the substitution referred to is also to replace all free individual variables by closed individual terms. We then arrive at a notion of validity for natural deductions in general [4].

Gentzen's idea could be summarized by saying that the meaning of a sentence is determined by what counts as a canonical proof of it, which is to say among other things that non-canonical reasoning must be possible to transform to canonical form in order to be acceptable—spelled out in full, the idea is that the meaning of a sentence is determined by what is required from a valid deduction of it. Although this way of formulating Gentzen's ideas goes beyond what he said himself, the three principles of validity formulated here are implicit in the example that he gave, as has been shown above.

Closed valid deductions may be seen as representing proofs, and I shall sometimes refer to them as Gentzen proofs.

  • [1] 4Prawitz (1974) [19]. The term “canonical proof”, which was used already by Brouwer in a different context, was applied to normal proofs by Kreisel (1971) [13] and to proofs mentioned in the intuitionistic meaning explanations (such as the BHK-interpretation) by Dummett (1975) [2]
  • [2] “kann man … aus einem bewiesenen A sofort B schließ[en]. Denn AB dokumentiert ja das Bestehen einer Herleitung von B aus A” (Gentzen 1934–35 [4, p. 189]
  • [3] Although Gentzen never stated these reductions in any published work, it seemed clear already from his example quoted here that he was aware of them. This was later verified when finding an unpublished manuscript where Gentzen actually proved a normalization theorem for intuitionistic natural deduction with these reductions (see von Plato 2008 [25])
  • [4] What was called “validity based on the introduction rules” by Prawitz (1971) [17] differs from the notion presented here in one substantial respect: in clauses corresponding to principle III, extensions of the set of valid deductions for atomic sentences were considered and it was required that substitutions preserved validity also relative to them; cf. footnote 12 In addition to this notion, I also defined a notion of “validity used in proofs of normalizability”, similar to Martin-Löf (1971) [14] notion of computability, but as pointed out by Schroeder-Heister (2006) [22], this notion of validity is quite different and should not be counted as a semantic notion explicating Gentzen's idea of meaning, because normalizable deductions are defined outright as computable although (if open) they may not be reducible to canonical form
Found a mistake? Please highlight the word and press Shift + Enter  
< Prev   CONTENTS   Next >

Related topics