Home Philosophy Advances in Proof-Theoretic Semantics
Abstract Wilfrid Hodges' opinion is that some ideas of Peter Schroeder-Heister and the author concerning logical consequence are largely sound and probably uncontroversial, but he criticizes some of their aspects. In this note Hodges' critique of the author is found misplaced.
Categorial proof theory
I am glad Wilfrid Hodges took in  an interest in my philosophical paper , but I am sorry his reading of it is marred by misunderstanding, and leads to imprudent reproaches. I don't find Peter Schroeder-Heister's ideas are evaluated correctly in , but I will make comments only on what is said there, in the last few pages, on my paper.
In the middle of Sect. 1.3 of , where the critique of my paper starts, Wilfrid says that “at the heart of their [Peter's and my] arguments against 'model-theoretic semantics' is the question what can be defined in terms of what”. I was unaware that I was producing arguments against model-theoretic semantics, and as much unaware that I was dealing with Wilfrid's question. Concerning the arguments against modeltheoretic semantics, the dogmas (assumptions that everybody makes, and nobody calls into question) discussed by Peter and me are accepted not only in that kind of semantics, but also in proof-theoretic semantics, and my paper discusses their acceptance in the later kind of semantics. Concerning defining, at two places (in Sects. 5 and 6 of ) I mentioned the inductive definition of derivations and codes for them, and the definition of inference, i.e. deduction (as I said in Sect. 2 of , I used the word “inference” to accord with Prawitz's usage), as an equivalence class of derivations. Elsewhere, I spoke of definition only when I mentioned the opinions of others. “The question what can be defined in terms of what”, burdened (as the linguist Anna Wierzbicka) by the legacy of Aristotle, is hardly “at the heart of my arguments”. My ideas, as should be quite clear from my paper, are very far from Aristotle. They come from categorial proof theory, a mathematical field at the border of category theory and proof theory.
Wilfrid seems to think that speaking of priority and primacy means one must be speaking about “what can be defined in terms of what”. One may reasonably claim that for explaining how an organism functions physiological notions, like for example homoeostasis, have primacy over anatomical notions, like for example parenchyma or stroma. This does not mean that the later notions are definable in terms of the former ones, and not vice versa. In defining anatomical notions concerning organs one may, but need not, rely on physiological notions, but one would equally rely on anatomical notions—in particular on the notion of organ—when defining physiological notions. In general, in the order of explanation, it seems indisputable that one may claim precedence for the notions of a science that seeks laws accounting for phenomena over the notions of a taxonomical science (see , Sect. 10). Nearer to the field of logic, theoretical linguistics and its notions would have for explaining how language functions precedence, primacy, over descriptive linguistics and its notions.
In a different register, in the order of exposition and not the order of explanation, some notions can have for deep and natural reasons precedence over others without this meaning that the later notions are simply definable in terms of the former. In logic, one usually has that in the order of exposition the connectives of propositional logic have primacy, priority, over the quantifiers of predicate logic, without the latter being definable in terms of the former. In the foundations of mathematics, one usually has that in the order of exposition logical notions, the connectives and the quantifiers, together with the axioms concerning them, have priority over the set-theoretical membership relation, together with the axioms concerning it, without the latter being definable in terms of the former, as some authorities still expected a hundred years ago. I will return to matters of primacy towards the end of this note.
I argue in  and elsewhere that the notion of inference should not be understood as the notion of consequence relation. I don't understand what Wilfrid means by saying before (1.10) that I forgot the codes of inferences. It is quite the opposite. I argue that an inference should not be taken as an ordered pair made of the premise and the conclusion, an ordered pair which is a member of a consequence relation. With inferences we do not have a relation, but a graph in the sense of category theory, which is given by a function assigning to every arrow an ordered pair of objects (some graph-theorists call that a directed graph, and others, following , could call it a directed pseudograph).
Wilfrid finds after (1.9) that a notation for derivations (does he mean by that the same as I mean by inference or deduction?) in which he draws triangles “has the advantage that it allows one to write several hypotheses”. The usual notation in the style of Gentzen with sequents plural on the left can claim the same merit. In the context where we are interested in identity of inferences there is no mathematical loss, and there is a gain in clarity, if we restrict ourselves to the categorial format with a single object as the source of an arrow. Since the premises are finite in number, we can replace a plurality of them by their conjunction, and the absence of them by the propositional constant true. If on the other hand we are interested in the question of reducibility of inferences to normal form, then it might be worthwhile to move to a multicategorial, or operadic format, with a plurality of objects as sources. Moreover, this should be done in an analogue of bicategories, i.e. weak 2-categories (see ). One can also envisage working in polycategories (see ).
I argued at length against psychologism concerning inference towards the end of Sect. 4 of , and also in Sects. 6 and 7. In Wilfrid's remarks after (1.12) in , though at the end of the paragraph he admits that “a psychological analysis of 'making an inference' is not the right way to go”, there are still psychologistic tones in his mentioning that “people can perform an act called making an inference”. So I am afraid that the point Wilfrid ascribes to me with approval is not exactly mine. If one understands inference psychologistically, as much as Wilfrid seems to do, that point may be acknowledged, but I don't think it has much worth from a technical, proof-theoretical, point of view.
To speak of impersonal inferences, not performed as an act, not made by anybody, need not be natural. This may be something in the technical language of prooftheorists. The task of proof theory however is not to stick to ordinary language, but to speak about mathematical structures involved in deduction. One finds the very interesting and important partial algebras in question in categorial proof theory (see the elementary talk ). Model theory, as it was conceived up to now, is blind for their logical role.
Wilfrid's indignant remarks where I am accused to be saying that “the vast mass of twentieth century researchers in philosophy of logic and language all make a mistake not far short of adding 2 to 4 and getting 11” seem to stem from his assuming that a Kosta made of straw is accusing the philosophers interested in logic and language of confusing a psychologistic inference with a non-psychologistic consequence. Without putting psychologism into the picture, it was already shown by Gentzen that from a purely technical point of view it is worth studying inference syntactically, though Gentzen's sequents could be read as consequence, i.e. a generalized implication (this is how, for example, Church read them). Without psychologism, the difference between inference and consequence becomes mathematically even clearer in categorial proof theory, where one studies identity of inferences. Gentzen did not study that (though one may perhaps take that his results are pointing in that direction).
I believe that at least 95 % of logicians, and 99 % of philosophers of logic and language, do not care about the codes of inferences and identity of inferences formalized by systems of equations between these codes. They are quite happy with having inferences that amount to consequence relations. Inferences that have respectively the same premises and the same conclusions are for them always the same. Being one of the rare logicians working in categorial proof theory on identity of inferences (i.e. identity of deductions), in the footsteps of Lambek and Mac Lane, I dare advance the figures of these percentages.
The primacy of propositions over deductions, i.e. of asserting over deducing, is in the order of explaining how language functions, and is of the same kind as the primacy of asserting over naming, which Dummett speaks about in Chap. 1 of , and which is mentioned in Sect. 2 of . Dummett's words are: “Frege's account, if it is to be reduced to a slogan, could be expressed in this way: that in the order of explanation the sense of a sentence is primary, but in the order of recognition the sense of a word is primary.” (, p. 4) In the penultimate paragraph of  Wilfrid says: “In the mainstream semantic and model-theoretic literature that I've seen, nobody talks about 'prior' notions or about one notion having 'primacy' over another.”
One should first realize that in accordance with what was said about primacy and defining at the beginning of this note, and contrary to what it seems Wilfrid would have in the wake of Aristotle, this is not simply a matter of defining the notion of deduction in terms of the notion of proposition, or vice versa, or defining the notion of proposition in terms of the notion of name, or vice versa. The literature that would supply what Wilfrid says he has not seen or heard could start with that reference to Dummett and continue with the references to Frege  and Wittgenstein ( and ), which are also in . It is surprising that after starting so auspiciously, on the shoulders of giants such as these last two, we don't manage to end up in the mainstream semantic literature.
I agree however with Wilfrid that model-theorists usually do not care about philosophical questions concerning meaning. I don't think this is because they have superior knowledge, but because together with interest they lack knowledge about these philosophical matters—as well as knowledge about many interesting and important mathematical matters of logic not in their realm.
1. Došen, K.: Logical consequence: a turn in style. In: Dalla Chiara, M.L. et al. (eds.) Logic and Scientific Methods, Volume I of the 10th International Congress of Logic, Methodology and Philosophy of Science, Florence 1995, pp. 289-311. Kluwer, Dordrecht (1997). mi.sanu.ac.rs/kosta/publications.htm
2. Došen, K.: Algebras of deductions in category theory. In: Jokanovic´ et al. (eds), Third Mathematical Conference of the Republic of Srpska, Proceedings, Trebinje 2013, Zbornik radova, vol. I, pp. 11-18. Univerzitet u Istocˇnom Sarajevu, Fakultet za proizvodnju i menadžment, Trebinje (2014). mi.sanu.ac.rs/kosta/DosenAlgebrasofDeductions.pdf; mk.rs.ba/wp-content/uploads/2015/02/TOM1-Copy.pdf, pp. 1–8 mi.sanu.ac.rs/ kosta/publications.htm
3. Došen, K.: Inferential semantics. In: Wansing, H., (ed.) Dag Prawitz on Proofs and Meaning, pp. 147-162. Springer, Cham (2015). Preprint of 2012: mi.sanu.ac.rs/kosta/ publications.htm
4. Došen, K., Petric´, Z.: Weak cat-operads (2010). Preprint v. 8: arXiv.org
5. Došen, K., Petric´, Z.: Graphs of plural cuts. Theor. Comput. Sci. 484, 41-55 (2013). arXiv.org
6. Dummett, M.A.E.: Frege: Philosophy of Language. Duckworth, London (1973)
7. Frege, G.: Die Grundlagen der Arithmetik: Eine logisch mathematische Untersuchung über den Begriff der Zahl. Verlag von Wilhelm Koebner, Breslau (1884) (English translation by J.L. Austin: The Foundations of Arithmetic: A Logico-Mathematical Enquiry into the Concept of Number, 2nd revised edn, Blackwell, Oxford, 1974)
8. Harary, F.: Graph Theory. Addison-Wesley, Reading, Mass. (1969)
9. Hodges, W.: A strongly differing opinion on proof-theoretic semantics? In: Piecha, T., Schroeder-Heister, P., (eds.) Advances in Proof-Theoretic Semantics. Springer, Berlin (2015). This volume
10. Wittgenstein, L.: Logisch-philosophische Abhandlung. Annalen der Naturphilosophie 14, 185262 (1921) (English translation by C.K. Ogden: Tractatus logico-philosophicus, Routledge, London, 1922, new translation by D.F. Pears and B.F. McGuinness, Routledge, London, 1961)
11. Wittgenstein, L.: Philosophische Untersuchungen. Blackwell, Oxford (1953) (English translation by G.E.M. Anscombe: Philosophical Investigations, fourth edition with revisions by
P.M.S. Hacker and J. Schulte, Wiley-Blackwell, Oxford, 2009)