Preamble

I am sharing an office with Francesco Paoli and, ever since I arrived in Cagliari (that was in February), Nissim Francez’s book Proof-theoretic semantics was always of Francesco’s desk. Okay, this is the wrong way of putting it; for one thing, I’ve read it. What I mean is that the book was never re-shelved. That’s a good faith for a book.

This particular book deserves aplenty a friendly review and I have planned to write one but never quite got to doing it. This (i.e., training myself to keep a regular blog) is as good as any an excuse to finally take some steps in that direction.

Note to self: Markdown for italic not rendered. Check. css (?).

The review

This review will come up in three instalments. The first is an overview of the first part of the book; the second is a discussion of several points of disagreement between Nissim and I followed by some general comments on my ‘aesthetical experience’ when reading the book; the third and final instalment is an overview of the second part of the book.

Since this is a practice run for the blog, I won’t bother with the niceties one usually puts in a positive review. I’ll save that for the official review. Instead, I’ll just say it outright here: I really like the book. You too should like it!

The first instalment

Overview of the first part

Francez’s book is, to date, the only extensive monograph on proof-theoretic semantics – i.e., the incarnation of logical inferentialism ostensibly inaugurated by Gentzen and subsequently developed by Prawitz, Dummett, and others. With a twist, for Francez attempts to apply those ideas to fragments of the natural language. This twist occupies the second part of the book and I shall have little to say about it. For me, the best bits are in the first part.

The ‘Introduction’ cursorily explores some of the philosophical underpinnings of logical inferentialism as embodied into proof-theoretic semantics. Unsurprisingly, this is pretty standard stuff; Francez does little to elaborate on the finer points of the matter. Nevertheless, the newcomer, even if starting the Phisolophy station, may find some worthwhile exploring paths. (I also haste to add that this judgement does not apply beyond this point.) I am more excited by the fifth section of the Introduction, ‘Natural-deduction proof-systems’. (I hate these hyphens.) This is a systematic and very careful presentation of natural deduction in Gentzen’s tree format. Everything is introduced by precise definitions and clear examples. It’s great to have it at hand, especially since it is the kind of stuff that I can’t stand writing. The chapter ends with a section on the idea of natural deduction rules as meaning conferring. Again, this is pretty straightforward and no-nonsense.

The first part of the book, ‘Proof-theoretic semantics in logic’ consists of five chapters. Chapter 2 presents some familiar logics (minimal, intuitionist, classical, relevant; it also contains a brief subsection on modal logic). This is more than enough for making the book self-contained, but one will not gain much knwoledge about these logics from here. The presentation is clear and illuminating; the pace is pleasantly alert. Moreover, it already touches on central issues in the development of proof-theoretic semantics for these logics. For instance, the section on classical logic (2.2) is organised around the troubles generated by negation (via double negation elimination, the law of the excluded middle and ‘indirect proof’ (i.e., classical reductio ad absurdum)).

The third chapter (‘The basis of acceptability of ND-rules as meaning conferring’) unfolds the drama of proof-theoretic semantics. About half of the chapter is occupied by the discussion of harmony. Recall that this is a term introduced by Dummett to designate the match of strength between the introduction and elimination rules for a constant. In turn, harmony is taken as a mark of the rules for that constant being well-behaved. Or, to put it slightly differently, it marks the success of the rules in defining a coherent (logical) concept. (I’ll say more about harmony in the second instalment.) Francez discusses in detail three formal accounts of harmony – intrinsic harmony, harmony in form and symmetric harmony. (I will discuss these in more detail in the second part of this review.) These are related to each other as well as to other concepts in the same ballpark, specifically, normalisability and conservativeness. The presentation is clear and easy to follow, especially if one is confortable with the logician’s/mathemathician’s habbit of breaking the prose into designated environments. Alas, Thomas Mann and other aesthetes have no reason to fear competition as far as style is concerned. The second part of the chapter looks at the logics introduced previously and checks whether their rules are harmonious. You know the story: intuitionist logic is the winner; the other competitors appeal the decision. It is well known that classical logic doesn’t pass muster when it is formulated in SET:FMLA (i.e., when the formulation allows the use of many premises but restricts the number of conclusions to one). The solution to this problem is postponed for the subsequent chapter.

Chapter 4 tackles the problem of harmonising classical logic. Francez considers the two main strategies, i.e., changing the framework and adopting a bilateralist perspective. The change of framework amounts to switching to a multiple-conclusion consequence relation. I am rather excited by Francez treating here the extra complication brought about by the possibility of formulating multiple-conclusion natural deduction calculi with either additive or with multiplicative rules. This topic deserves a lot more attention than it has previously received in the literature and Francez’s discussion of it is a welcome step in that direction. I am almost equally happy with him unearthing some lost gems of the literature on natural deduction, such as Boricis’s paper.

The second strategy is to move from rules dealing only with assertions to rules dealing with both assertion and denial. Francez discusses in some detail Rumfit-style bilateralism and provides a very nice account of intrinsic harmony in bilateral systems. The final section of the chapter surveys briefly ‘alternative conceptions of harmony justifying [c]lassical [l]ogic’. One of these relies on the adoption of ‘impure’ rules. Such rules mention in their schematic formulation more than one logical constant. (For reference, Peter Milne is their champion (or godfather – and yes, I do encourage you to think about the film!), but Gentzen himself was not worried about purity; his NK has negation governed by the zero-premise rule A or not-A, i.e., by tertium non datur.) I, for one, don’t like them. That aside, I am rather baffled by Francez’s ‘own position’ which is that:

As long as the goal is the justification of Classical Logic (which anyway contains disjunction), I find the arguments acceptable. Furthermore, I find the general use of impure ND-rules acceptable for the justification of any logic containing all the operators mentioned in the impure rules. However, when the goal is the (schematic) definition of negation, when added to an arbitrary object language […] I find the use of impure rules for defining negation unacceptable. After all, harmony (here achieved via the use of impure rules) is not a goal by itself – it only serves to rule out “bad” definitions that do not satisfy the more immediate demands of purity and separability. (p. 180)

I have a hard time wrapping my head around why the conditions of correct definition of a connective (here negation) may be overridden by whatever happens in a certain logic, such as it containing another connective, in this case disjunction. Besides, what is this goal, of justifying classical logic, if not the goal of showing that its connectives are harmonious? It may be that I am misunderstanding something here. But I classify Francez’s preferred account of harmony – intrinsic harmony – as one which is aims at locality. That is, as an account which aims to characterise harmony only in terms of properties of introduction/elimination rules for a constant, independently of what else happens in the logic under consideration. This makes his conclusion even stranger. (Locality is an aim which I myself find misguided, but that is another question.)

The penultimate chapter in Part I is entitled ‘Proof-theoretic semantic values’. This is a very interesting development, if one that I am not feeling too confident in judging. Francez develops what is essentially a theory of ‘grounds’ (in Prawitz’s sense). Grounds receive a precise formal definition (p. 185) and their theory is pushed up to defining, in a remarkably simple way, proof-theoretic logical consequence in relation to them. According to this definition A follows from a set of sentences X iff and only if the grounds for A are included into the ground for X. There is a wealth of stuff to think about in this chapter, whether one is provoked by the idea of ‘reifying’ proof-theoretic meanings or tempted to explore further Francez’s suggestion that his results ‘can be seen as fully in concert with Dosen’s characterisation of connectives as internalizing structural properties’. (This is an idiosyncratic selection. Read the chapter and you’ll find other interesting stuff.)

The final chapter in this part, ‘Other developments’, surveys other topics in proof-theoretic semantics. It goes over Schroeder-Heister style higher order rules (which discharge derivations, not only formulae), validity concepts in proof-theoretic semantics, the sequent calculus as a system for developing proof-theoretic semantics and reductive harmony – a harmony-based approach to what Dummett called first and second degree justification of logical laws. (I don’t really understand how the material is organised in this chapter. Section 6.2., ‘Validity of Arguments’, is 12 lines long; it is followed by two sections, entitled, respectively, ‘Model-theoretic validity’ (6.3) and ‘Proof-theoretic validity’ (6.4). The first is brief and largely recapitulative; the second is longer and meatier. For instance, it includes a 6 pages long subsection on Schroeder-Heister’s theory of ‘definitional reasoning’. I am not quite sure what goes on here. This is definitely not how I would have organised the same material. Despite this, I very much enjoyed reading it. A good reason to deliver these remarks inside parentheses.)