The Connectives

4. Existence and Uniqueness of Connectives

Chapter 4 Existence and Uniqueness of Connectives§4.1 PHILOSOPHICAL PROOF THEORY 4.11 Introduction In this chapter, we will discuss the existence (§4.2) and uniqueness (§4.3) of sentential connectives in the sense of connective in which connectives are not simply syntactic operations, but operations building formulas with certain inferential properties and relationships (as in 1.19). The present section fills in some of the background to that discussion, and the current subsection begins at the beginning, which is to say: with Gentzen. Recall that Gentzen [1934] introduced both the natural deduction approach and the sequent calculus approach to logic, relating these to each other and to the more traditional ‘Hilbert’ formalisms. The latter consist of axiomatic presentations of logic in Fmla. Gentzen’s sequent calculi were developed in Set-Set for classical logic and Set-Fmla0 for intuitionistic logic (1.27 and 2.32 respectively: as we have noted, strictly the “Set” here should be “Seq”, for historical accuracy). The natural deduction approach in both the classical and intuitionistic cases, he pursued, ‘naturally’ enough (though not inevitably: 1.27) in Set-Fmla. It is the latter approach (and framework) with which we are concerned here, with its characteristic organization of introduction and elimination rules for each connective (and quantifier – though these do not enter our discussion). Of this mode of organization, Gentzen made a very suggestive remark , the precise elaboration of which has greatly exercised Prawitz, Dummett, and other writers in the tradition of what we have chosen to call philosophical proof theory: the project of analyzing proofs with a view to throwing light on the meanings of the logical constants rather than for the derivation of technical results (consistency, decidability, etc.). Gentzen’s remarks on introduction and elimination rules began with the following sentence (we continue the quotation in the notes, p. 626): The introductions represent, as it were, the ‘definitions’ of the symbols concerned, and the eliminations are no more, in the final analysis, than the consequences of these definitions. (Gentzen [1934], p. 80.) 511 512 CHAPTER 4. EXISTENCE AND UNIQUENESS OF CONNECTIVES The “as it were”, as well as the scare-quotes around “definitions”, are an acknowledgment that in no standard sense of the term are we dealing with ordinary definitions here; and the ‘final analysis’ gestured toward still remains to be agreed upon. We will track some moves made by Prawitz in the desired direction, concentrating on what is known as Positive Logic, which is to say: the {∧, ∨, →}-fragment of intuitionistic logic; we will often use “PL” to abbreviate “Positive Logic”. A natural deduction proof system for PL – PNat, we can call it (as mentioned in 1.23) – may be obtained from Nat (or INat) by taking only the introduction and elimination rules for the three connectives listed. Note that the logical framework in which this example—and indeed most of our discussion in the present chapter—is couched, is Set-Fmla rather than Set-Set. (See Remark 1.21.1(i), p. 106.) First, a terminological issue must be addressed. The problem is over the word semantics. It has associations with concepts such as truth and reference, connecting language with the world. It also has associations with meaning. The double association presents no difficulty to those who see the basis of an account of meaning in a specification of the truthconditions of sentences, proceeding, inter alia, through the assignment of references to subsentential expressions. (For simplicity we ignore here such things as tone and conventional implicature: see 5.11.) But if one holds a theory according to which the central concepts to be used in elucidating meaning are not those, such as truth and reference, purporting to connect the linguistic with the non-linguistic, then a decision must be made as to whether semantics is to be deemed the study of meaning or rather that of the connections now discarded as not central to that study. A theory on which the meanings of the connectives are given by introduction and elimination rules, or (as suggested by the quotation from Gentzen) by the introduction rules alone, or indeed—another possible position—by the elimination rules alone, then it is not the connections between sentences and extra-linguistic reality that we need to have in focus for the study of meaning, so much as the connections—specifically, the inferential connections—between some sentences and others. For most of this Chapter, we will follow the convention that...