Categorical Harmony and Paradoxes in Proof-Theoretic Semantics

Abstract There are two camps in the theory of meaning: the referentialist one including Davidson, and the inferentialist one including Dummett and Brandom. Prooftheoretic semantics is a semantic enterprise to articulate an inferentialist account of the meaning of logical constants and inferences within the proof-theoretic tradition of Gentzen, Prawitz, and Martin-Löf, replacing Davidson's path “from truth to meaning” by another path “from proof to meaning”. The present paper aims at contributing to developments of categorical proof-theoretic semantics, proposing the principle of categorical harmony, and thereby shedding structural light on Prior's “tonk” and related paradoxical logical constants. Categorical harmony builds upon Lawvere's conception of logical constants as adjoint functors, which amount to double-line rules of certain form in inferential terms. Conceptually, categorical harmony supports the iterative conception of logic. According to categorical harmony, there are intensional degrees of paradoxicality of logical constants; in the light of the intensional distinction, Russell-type paradoxical constants are maximally paradoxical, and tonk is less paradoxical. The categorical diagnosis of the tonk problem is that tonk mixes up the binary truth and falsity constants, equating truth with falsity; hence Prior's tonk paradox is caused by equivocation, whereas Russell's paradox is not. This tells us Prior's tonk-type paradoxes can be resolved via disambiguation while Russell-type paradoxes cannot. Categorical harmony thus allows us to demarcate a border between tonk-type pseudo-paradoxes and Russell-type genuine paradoxes. I finally argue that categorical semantics based on the methods of categorical logic might even pave the way for reconciling and uniting the two camps.

Introduction

Broadly speaking, there are two conceptions of meaning: the referentialist one based on truth conditions as advocated by Davidson [7], and the inferentialist one based on verification or use conditions as advocated by Dummett [10] or more recent Brandom [5]. Along the latter strand of the theory of meaning, proof-theoretic semantics undertakes the enterprise of accounting for the meaning of logical constants and inferences in terms of proof rather than truth, thus replacing Davidson's path “from truth to meaning” by another Dummettian path “from proof to meaning”; the term “proof-theoretic semantics” was coined by Schroeder-Heister (for a gentle introduction, see Schroeder-Heister [21]; he also coined the term “substructural logic” with Došen). It builds upon the proof-theoretic tradition of Gentzen, Prawitz, and Martin-Löf, tightly intertwined with developments of Brouwer's intuitionism and varieties of constructive mathematics, especially the Brouwer-Heyting-Kolmogorov interpretation, and its younger relative, the Curry-Howard correspondence between logic and type theory, or rather the Curry-Howard-Lambek correspondence between logic, type theory, and category theory (see, e.g., Lambek and Scott [12]). Note however that Brouwer himself objected to the very idea of formal logic, claiming the priority of mathematics to logic (cf. Hilbert's Kantian argument in [11] concluding: “Mathematics, therefore, can never be grounded solely on logic”). “Harmony” in Dummett's terms and the justification of logical laws have been central issues in proof-theoretic semantics (see, e.g., Dummett [10] and Martin-Löf [14]).

Combining proof-theoretic semantics with category theory (see, e.g., Awodey [2]), the present paper aims at laying down a foundation for categorical proof-theoretic semantics, proposing the principle of categorical harmony, and thereby shedding structural light on Prior's “tonk” and related paradoxical logical constants. Prior's invention of a weird logical connective “tonk” in his seminal paper [18] compelled philosophical logicians to articulate the concept of logical constants, followed by developments of the notion of harmony. In a way harmony prescribes the condition of possibility for logical connectives or their defining rules to be meaning-conferring, and as such, it works as a conceptual criterion to demarcate pseudo-logical constants from genuine logical constants. Let us recall the definition of Prior's tonk. Tonk can be defined, for example, by the following rules of inference as in the system of natural deduction:

ξ ϕ

ξ ϕ tonk ψ ξ ϕ tonk ψ

(tonk-intro.) ξ ψ (tonk-elim.) (1)

In any standard logical system (other than peculiar systems as in Cook [6]), adding tonk makes (the deductive relation of) the system trivial, and thus we presumably ought not to accept tonk as a genuine logical constant. In order to address the tonk problem, different principles of harmony have been proposed and discussed by Belnap [3], Prawitz [17], Dummett [10], and many others. From such a point of view, harmony is endorsed to ban tonk-like pathological connectives on the ground that their defining rules violate the principle of harmony, and are not meaning-conferring as a consequence of the violation of harmony. They cannot be justified after all.

In the present paper, we revisit the tonk problem, a sort of demarcation problem in philosophy of logic, from a novel perspective based on category theory. In his seminal paper [13], Lawvere presented a category-theoretical account of logical constants in terms of adjoint functors, eventually giving rise to the entirely new discipline of categorical logic (see, e.g., Lambek and Scott [12]) including categorical proof theory. Note that “categorical logic” is sometimes called “categorial logic” in philosophy to avoid confusion with the philosopher's sense of “categorical” (like “categorical judgements”); especially, Došen, a leading researcher in the field, uses “categorial logic”, even though “categorical logic” is widely used in the category theory community. Categorical logic is relevant to proof-theoretic semantics in various respects, as explicated in this paper as well. Among other things, a fundamental feature of the link between categorical logic and proof theory is that categorical adjunctions amount to bi-directional inferential rules (aka double-line rules) of certain specific form in terms of proof theory; by this link, categorical terms can be translated into proof-theoretic ones. Building upon Lawvere's understanding of logical constants, in this paper, I formulate the adjointness-based principle of categorical harmony, and compare it with other notions of harmony and related principles, including Belnap's harmony [3], Došen's idea of logical constants as punctuation marks [8, 9], and the reflection principle and definitional equations by Sambin et al. [19]. And the final aim of the present paper is to shed new light on the tonk problem from the perspective of categorical harmony.

In comparison with other concepts of harmony, there is a sharp contrast between categorical harmony and Belnap's harmony in terms of conservativity; at the same time, however, uniqueness is a compelling consequence of categorical harmony, and so both endorse uniqueness, yet for different reasons. The principle of categorical harmony looks quite similar to Došen's theory of logical constants as punctuation marks, and also to the theory of the reflection principle and definitional equations by Sambin et al. It nevertheless turns out that there are striking differences: some logical constants are definable in Sambin's or Došen's framework, but not definable according to categorical harmony, as we shall see below. It is not obvious at all whether this is an advantage of categorical harmony or not. It depends upon whether those logical constants ought to count as genuine logical constants, and thus upon our very conception of logical constants; especially, what is at stake is the logical status of substructural connectives (aka multiplicative connectives; in categorical terms, monoidal connectives).

Finally, several remarks would better be made in order to alleviate common misunderstandings on categorical semantics. The Curry-Howard correspondence is often featured with the functional programmer's dictum “propositions-as-types, proofs-as-programs”. Likewise, the Curry-Howard-Lambek correspondence may be characterised by the categorical logician's dictum “propositions-as-objects, proofsas-morphisms.” One has to be careful of categorical semantics, though. For the Curry-Howard-Lambek correspondence does not hold in some well-known categorical semantics. The correspondence surely holds in the cartesian (bi)closed category semantics for propositional intuitionistic logic, yet at the same time, it is not true at all in the topos semantics for higher-order intuitionistic logic (or intuitionistic ZF set theory), and it does not even hold in the logos (aka Heyting category) semantics for first-order intuitionistic logic. For the very facts, the latter two semantics are called proof-irrelevant: they only allow for completeness with respect to the identity of propositions, and does not yield what is called full completeness, i.e., completeness with regard to the identity of proofs. Some category theorists who do not care about the proof-relevance of semantics tend to say that the topos semantics is a generalisation of the cartesian (bi)closed category semantics; however, the claim is only justified in view of the identity of propositions, and it is indeed wrong in light of the identity of proofs, which is not accounted for in the topos semantics at all. Note that locally cartesian closed categories yield proof-relevant semantics for Martin-Löf's dependent type theory, and toposes are locally cartesian closed. If we see toposes as semantics for dependent type theory, then the topos semantics is proof-relevant; yet, this is an unusual way to interpret the term “topos semantics”. The Curry-Howard-Lambek correspondence is now available for a broad variety of logical systems including substructural logics as well as intuitionistic logic, yet with the possible exception of classical logic. Although quite some efforts have been made towards semantics of proofs for classical logic, there is so far no received view on it, and there are impossibility theorems on semantics of classical proofs, including the categorical Joyal lemma. For classical linear logic, nonetheless, we have fully complete semantics in terms of so-called ∗-autotonomous categories.

The rest of the paper is organised as follows. In Sect. 2, we review Lawvere's categorical account of logical constants, and then formulate the principle of categorical harmony. There are several subtleties on how to formulate it, and naïve formulations cannot properly ban tonk-type or Russell-type logical constants. Comparison with Došen's theory is given as well. In Sect. 3, we further compare the principle of categorical harmony with Belnap's harmony conditions and Sambin's reflection principle and definitional equations. The logical status of multiplicative (monoidal) connectives is discussed as well, and three possible accounts (i.e., epistemic, informational, and physical accounts) are given. In Sect. 4, we look at tonk and other paradoxical logical constants on the basis of categorical harmony, thus exposing different degrees of paradoxicality among them. Especially, what is wrong with tonk turns out to be equivocation. The paper is then concluded with prospects on the broader significance of categorical logic in view of the theory of meaning. Little substantial knowledge on category theory is assumed throughout the paper.