 Home Philosophy Advances in Proof-Theoretic Semantics

# Concluding Remarks: From Semantic Dualism to Duality

Let us finally address further potential implications of categorical logic to the theory of meaning. The dualism between the referentialist and inferentialist conceptions of meaning may be called the semantic dualism. Categorical logic may (hopefully) yield a new insight into the semantic dualism, as argued in the following.

From a categorical point of view, “duality” may be discriminated from “dualism”. Dualism is a sort of dichotomy between two concepts. Duality goes beyond dualism, showing that the two concepts involved are actually two sides of the same coin, just as two categories turn out to be equivalent by taking the mirror image of each other in the theory of categorical dualities. Duality in this general sense seems to witness universal features of category theory. Indeed, the classic dualism between geometry and algebra breaks down in category theory. For example, the categorical concept of algebras of monads encompasses topological spaces in addition to algebraic structures. Category theory may be algebraic at first sight (indeed, categories are many-sorted algebras), yet it is now used to formulate geometric concepts in broad fields of geometry, ranging from algebraic and arithmetic geometry to knot theory and low-dimensional topology. It is also a vital method in representation theory and mathematical physics. Technically, there are a great number of categorical dualities between algebraic and geometric structures (e.g., the Gelfand duality and the Stone duality). It may thus be said that the concept of categories somehow captures both algebraic and geometric facets of mathematics at a deeper level, and so there is duality, rather than dualism, between algebra and geometry.

Just as in this sense category theory questions the dualism between algebra and geometry, categorical logic opaques the generally received, orthodox distinction between model theory and proof theory, and presumably even the semantic dualism above, suggesting that they are merely instances of the one concept of categorical logic. For example, the Tarski semantics and the Kripke semantics, which are two major instances of set-theoretic semantics, amount to interpreting logic in the category of sets and the category of (pre)sheaves, respectively (from a fibrational, or in Lawvere's terms hyperdoctrinal, point of view, we conceive of topos-induced subobject fibrations rather than toposes themselves). On the other hand, proof systems or type theories give rise to what are called syntactic categories, and their proof-theoretic properties are encapsulated in those syntactic categories. For example, cartesian biclosed categories and ∗-autonomous categories give fully complete semantics of intuitionistic logic and classical linear logic, respectively, in the sense that the identity of proofs exactly corresponds to the identity of morphisms (note also that the possibility of proof normalisation is implicitly built-in to categorical semantics; if normalisation is not well behaved, syntactic categories are not well defined). There is thus no dualism between model-theoretic and proof-theoretic semantics in categorical semantics. That is, there is just the one concept of categorical semantics that can transform into either of the two semantics by choosing a suitable category (fibration, hyperdoctrine) for interpretation. Put another way, we can make a proof system out of a given structured category (which is called the internal logic of the category; some conditions are of course required to guarantee desirable properties of the proof system), and at the same time, we can also model-theoretically interpret logic in that category. This feature of categorical logic allows us to incorporate both model-theoretic and proof-theoretic aspects of logic into the one concept. In a nutshell, categorical semantics has both proof-theoretic and model-theoretic semantics inherent in it, and from this perspective, there is no dualism, but duality between proof-theoretic and model-theoretic semantics, which may be called the semantic duality.

We must, however, be careful of whether this sort of unification makes sense philosophically as well as mathematically. There may indeed be some conceptual reasons for arguing that we ought to keep model-theoretic and proof-theoretic semantics separate as usual. Yet we may at least say that categorical logic exposes some common features of the two ways of accounting for the meaning of logical constants; at a level of abstraction, model-theoretic and proof-theoretic semantics become united as particular instances of the one categorical semantics. The philosophical significance of that level of abstraction is yet to be elucidated. Found a mistake? Please highlight the word and press Shift + Enter Related topics