The original sin of proof-theoretic semantics

Proof-theoretic semantics is an alternative to model-theoretic semantics. It aims at explaining the meaning of the logical constants in terms of the inference rules that govern their behaviour in proofs. We argue that this must be construed as the task of explaining these meanings relative to a logic, i.e., to a consequence relation. Alas, there is no agreed set of properties that a relation must have in order to qualify as a consequence relation. Moreover, the association of a consequence relation to a logical calculus is not as straightforward as it may seem. We show that these facts are problematic for the proof-theoretic project but the problems can be solved. Our thesis is that the consequence relation relevant for proof-theoretic semantics is the one given by the sequent-to-sequent derivability relation in Gentzen systems.

1. This is a “connective” introduced as a disjunction and eliminated as a conjunction which trivialises transitive logics. While it does not directly threaten Gentzen’s programme (cf. Humberstone 2011, p. 537), it has been one of the sources of the problem of definitional success via inference rules, q.v. the next section.

2. For instance, Humberstone (2011, p. 538 sq.) identifies Belnap’s antecedent context of deducibility with the purely structural fragment of the logic at issue, i.e., with the fragment that does not contain any logical constant at all; Garson (2001) with its entire c-free fragment (where c is the logical constant we are defining), which may contain other logical constants.

3. For a monographic account of PTS documenting extensively a great variety of work in this spirit, see Francez (2015).

4. We use the shudder quotes to mark that we use “standard” as a term of art. We follow Schroeder-Heister and use it to refer to the canonical work of Gentzen, Dummett, Prawitz and their many faithful followers. Hereafter, with the partial exception of the final section, we will no longer mark this focus, as it should be evident from the discussion. We also wish to emphasise that by taking this as our target, we are not setting ourselves up to futilely storming the museum of outdated PTS views. The achievements of the “founding fathers” are so momentous that, though rarely made explicit (ours is an insidious enemy!), these assumptions are in force even today.

5. In this paper we will freely change terminological registers, switching between “formula” and “statement”, “sentence”, or “assertion” at will. The convention is that a formula represents a statement (sentence, assertion) within a formal system of logic. The choice between the registers is determined by the naturalness of the chosen term in the context.

6. The deliberate ambiguity of the word “collection” will be addressed only later in the paper.

7. Again, there is deliberate ambiguity here: what the comma means in X, Y : B depends on what kind of “collections” are at stake. The issue will be amply debated in the sequel.

8. The formula C is a parameter in this formulation of the rule. So with respect to sequent calculi a context is not merely a list of undischarged assumptions, but, roughly, the collection of formula-occurrences that are neither used nor produced by the application of the rule.

9. Throughout this paper we restrict our attention to propositional logics; therefore the labels for the various logical calculi refer to their propositional fragments.

10. That is, in it every derivation can be “reduced” to a derivation of the same conclusion in which no formula is both the conclusion of an I-rule and the major premiss of an immediately following application of an E-rule for the same constant.

11. See, however, Ripley (2018) for a more sophisticated discussion of this last point.

12. For more on this see Read (2000) and Jacinto and Read (2017); for related approaches to harmony see Schroeder-Heister (2018) and Francez (2015) and the references therein.

13. Roughly, this is the property that every formula in a derivation is a subformula of the formulas occurring in its endsequent.

14. There is an enormous body of literature on harmony. Besides the loci classici quoted in text, the reader can consult Francez (2015), Humberstone (2011) and Schroeder-Heister (2018). See also Read (2000) and Tennant (forthcoming) among others.

15. For more on the debate on multiple-conclusions, we refer the interested reader to Steinberger (2011) for an impressive case against multiple-conclusions and to Dicher (2018a) for both a list of some of the defences voiced on their behalf and for one such defence; see also Cintula and Paoli (2016). For a very careful discussion of the set-theoretic structure underlying (the presentation of) a logic see Humberstone (2011), esp. §§1.21 and 1.22; cf. also §§1.16 and 1.17.

16. The literature on substructural logics illustrates this aplenty. See Paoli (2002) and Restall (2000) for monographic presentations of these logics. For the technical aspects of substructurality, the reader can also consult Bimbo (2014).

17. For instance, we see relevant logic being treated as collections of theorems by, e.g., Meyer (1974) and Anderson and Belnap (1975). Although this is now a minority view, it retains its occasional defenders, see e.g. Smith (2012).

18. One should not confuse the axiomatic definition discussed here with Tarski’s famed model-theoretic account of first-order classical consequence. The former is neutral with respect to the classical/non-classical and to the proof-theoretic/model-theoretic dichotomies. We parenthetically observe that Tarski, and the Polish school in general, favoured an equivalent but somehow less intuitive approach in terms of consequence operators.

19. That is, if \(X{\vdash }A\), then \(\sigma (X){\vdash }\sigma (A)\) for all \(\mathcal {L}\)-substitutions \(\sigma \) (defined point-wise). However, this property will play no role subsequently so we do not include it in the formal definition below.

20. An anonymous referee observes that this—to our minds—advantage is of little use to one who does not believe that the Tarskian account of consequence is correct. To move such an objector, the referee suggests, we would need to provide a substantive defence of the Tarskian analysis. We do not believe this to be the case. As it will become apparent in the sequel, the important thing for us is that adherence to Tarski’s account is an available option even for one who opposed it beforehand. We press for a reconsideration of the manner in which Tarskian consequence relations may obtain and its import for PTS. If we are at all successful in this, then it behoves the anti-Tarskian to re-examine their proposals and weigh them against our faithfulness to orthodoxy.

21. There are, of course, exceptions from this general claim. Among relevantists, for instance, Read (1988) has been most appreciative of the importance of these issues. We repeat, however, that here we are interested in trends, rather than individual cases.

22. There is a very elegant alternative to this, developed recently in Francez (2017).

23. \(\mathrm {LJ}\) is obtained from \(\mathrm {LK}\) by restricting succedents to containing at most one formula.

24. An anonymous referee professes some puzzlement as to what the sin may be here, since the heroes of the standard PTS programme are devout Tarskians. This is a case of the road to hell being paved with good intentions. They sin because they enjoy the Tarskian blessings undeservingly: faithfulness to them is achieved accidentally and then embraced dogmatically, to the unwarranted exclusion of derivability relations that may not be Tarskian in the same way. More on this will follow shortly.

25. Technically, it is also possible to drop the single-conclusion requirement and adopt a multiple-conclusion concept of consequence (Scott 1971). But, as already pointed out in footnote 15, this is a controversial move.

26. Dual-intuitionistic logic, \(\mathbf {DIL}\), provides us with another example. A sequent calculus for \(\mathbf {DIL}\) is obtainable from \(\mathrm {LK}\) by applying the “at most one formula occurrence” restriction to the antecedents (Urbas 1996; Aoyama 2004). Since antecedents cannot contain more than one formula, it is impossible to use, e.g., the rules for negation:

    

    to move formulae from the succedent to the antecedent. Thus there is no straightforward way of getting the internal consequence relation of this calculus to be single-conclusion.

27. A rule is admissible in a sequent calculus if and only if its addition to it does not increase its stock of provable sequents.

28. The ingredients of this are, to a large extent, familiar. The reader will recognise in what follows familiar ideas from the literature on, e.g., translations between logics or equivalence of proof systems, cf. Carnielli et al. (2009).

29. An referee points out that this very abstract approach to consequence has a precursor in the work of Paul Hertz; see Schroeder-Heister (2002).

30. A similar account is independently proposed by Pynko (1999). The extra feature in Blok and Jónsson’s version is an elegant abstract treatment of substitution invariance. If U is a set with no structure to be preserved, it makes no sense to introduce substitutions in the usual way—i.e. as endomorphisms of the formula algebra. Blok and Jónsson find an insightful way around this problem, which lies outside the scope of the present paper.

31. Blok and Jónsson dub this relation similarity. The relation they call “equivalence” takes into account the problem of substitution-invariance that we have decided to leave out of the picture.

32. For simplicity, we define this map only for sequents with nonempty antecedents and succedents.

33. In practice, there is no need to worry about \(\mathbf {t}\) when it occurs as the antecedent of a conditional, because we can get rid of it via modus ponens.

34. The commas on the right-hand side of the equivalence have nothing to do with the structural operators of \(\mathrm {LR} ^{+}\); they are the banal commas of set theory.

35. See also Tennant (2017), p. 122.

36. The case in which \(Y\not =\emptyset \) this requires a rather subtle interpretation. First, any statement in \(X\cup \{A\}\) can play the role assigned in our main discussion to A itself. Context is a matter of focus (this can be determined by, say, the rule applied). Second, if, for instance, one construes the comma on the right as an intralinguistic disjunction (or even as a kind of counterpart of such a disjunction), then an ‘inferential context’ must be taken to express or at least to allow the expression of inferential connections between the ‘asserted’ statement and other statements. This is an inescapable burden for the account, as this complication will occur irrespective of the statement on which we focus and irrespective of whether it occurs on the left or on the right of the sequent sign.

37. Ours is not the only available option. Restall (2005) defends a different but equally intratheoretical reading of sequents as incoherent positions consisting of some assertions (in the antecedent) and some denials (in the succedent).

We are grateful to audiences at the Universities of Bucharest, Cagliari, Lisbon, and Milan, where we have presented previous versions of this paper. We would also like to thank the anonymous referees for this journal for their very detailed and helpful comments. We owe thanks to Peter Schroeder-Heister for many valuable comments and pointers to the literature. Thanks are also due to Elia Zardini who provided us with detailed comments on a previous version of this paper. B.D.’s work was financially supported by the FCT – Fundação para a Ciência e a Tecnologia, Portugal, through grant SFRH/BPD/116125/2016. F.P.’s work was financially supported by Fondazione Banco di Sardegna, within the project “Science and its Logics: The Representation’s Dilemma”, Cagliari, number: F72F16003220002”. Both authors gratefully acknowledge the partial financial support of Regione Autonoma Sardegna, within the Project CRP-78705 (L.R. 7/2007), “Metaphor and argumentation”.

Authors and Affiliations

1. Centre of Philosophy, Faculty of Letters, University of Lisbon, Lisbon, Portugal

   Bogdan Dicher

2. Department of Pedagogy, Psychology, Philosophy, University of Cagliari, Cagliari, Italy

   Francesco Paoli

Corresponding authors

Correspondence to Bogdan Dicher or Francesco Paoli.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Reprints and permissions