Deriving semantics from pragmatics
Kris Brown
Press s for speaker notes, q to reveal hidden slides
Background (1/6)
$$
$$
Project Timeline
- 2024: Formal pragmatics \(\to\) semantics construction for propositional logics
Recently there was a book that made a big step forward in understanding the relationship between pragmatics and semantics.
Background (2/6): semantics
Competing strategies for understanding the meanings of our ordinary language:
Bits of language have meaning by referring to the world.
Let me explain how I’m going to use those terms. You might say they are competing strategies for understanding the meanings in our ordinary language. Let’s start with the semantic attitude which draws from the way we understand meaning in artificial languages.
. . .
One possibility:
- particular nouns pick out objects (from some set of `real-world objects’)
- adjectives pick out subsets of objects (i.e. predicates)
- sentences pick out subsets of possible worlds (the worlds in which they’re true)
andpicks out the intersection of such subsets
The semantic attitude might take it that for example, our particular nouns pick out objects in some domain of real-world objects, that our adjectives pick out subsets of these, that our sentences pick out subsets of possible worlds and our logical conjunction intersects these sets, and so on. To handle more richness of language, people throw in other gizmos like accessibility relations to handle modality.
Background (3/6): semantic analysis example
\[ [\![ \text{Amy is poor and honest} ]\!] \\ [\![ \text{Amy is poor} ]\!] [\![ \text{and} ]\!] [\![ \text{Amy is honest} ]\!] \\ \underset{\rm Predicate}{\underbrace{{[\![ \text{Poor} ]\!]}}}(\underset{\rm Object}{\underbrace{{[\![ {\text{Amy}} ]\!]}}}) \underset{\rm Connective}{\underbrace{\raisebox{-1mm}{$\cap$}}} \underset{\rm Predicate}{\underbrace{{[\![ \text{Honest} ]\!]}}}(\underset{\rm Object}{\underbrace{{[\![ {\text{Amy}} ]\!]}}})\\ \]
Let’s consider an example sentence. We could potentially analyze ‘Amy is poor and honest’ to have this covert or implicit logical structure, involving objects, predicates, and a propositional connective.
. . .
\[\text{As conjunctions: }[\![ \text{and} ]\!]=[\![ \text{but} ]\!] = \cap\] \[[\![ \text{Amy is poor and honest} ]\!] = [\![ \text{Amy is poor but honest} ]\!]\] \[[\![ \text{Amy is poor and honest} ]\!] \vDash [\![ \phi ]\!] \quad \text{ iff }\quad [\![ \text{Amy is poor but honest} ]\!]\vDash [\![ \phi ]\!]\]
Now, let’s assume that, as conjunctions, ‘and’ and ‘but’ are taken to have the same ‘literal’ meaning (that of intersecting scenarios), this means that ‘Amy is poor and honest’ and ‘Amy is poor but honest’ have the same semantic value (literal meaning)! Therefore any sentence phi which semantically is a consequence of one must be likewise for the other.
. . .
As a final comment on the semantic attitude, I’ll highlight that this has the upshot that it neatly explains how language is compositional: the meaning of a complex is often the meaning of its parts combined in some algorithmic way.
Background (4/6): pragmatics
To say something is to do something, a speech act.
The meanings of speech acts are to be read off of their consequences.
By contrast, the pragmatic attitude starts with observing that we do a lot of things with language which are not simply referring to or describing the world.
. . .
- E.g. “Court is in session” not a description of the court
- E.g. propriety of a chess move not justified by reference.
- Rule for knight movement is constitutive what it means to be a knight.
For example a judge declaring court is in session isn’t describing it as such but making it the case. People like to talk about ‘language games’ in this space: the analogy is good because games are a setting where there are genuine rules that regulate proper and improper behavior, and proper moves are not justified by reference (the knight moves the way it does because we have agreed that’s the rule, not because actual horses move that way, for example).
. . .
- Assume we have at least two specific kinds of speech acts: assertion and denial.
- Assume a normative status ‘impropriety’, e.g. \({\rm Improper}(A^+)\) means it’s improper to assert \(A\).
- \({\rm Improper}(A^+,\ B^-) \ \ \equiv\ \ A \vdash B\ \ \equiv\ \ B\text{ follows from }A \ \ \equiv \ \ A \text{ is a reason for }B\)
The last thing I’ll say about pragmatics: we can get a notion of consequence with just some very basic ingredients. Two very particular speech acts (assertion and denial) and a notion of a speech act being `improper’. This model, which is called bilateralism, interprets the norm which which forbids simultaneously asserting A and denying B, as a norm in which A is a good reason for B which we denote with the turnstile.
Background (5/6): semantics versus pragmatics
Competing strategies for understanding the meanings of our ordinary language:
Language has meaning by referring to the world.
To say something is to do something (speech act).
Meanings are to be read off of the consequences.
So where might these two attitudes come in contact with each other?
. . .
\[\text{When all goes well: }\quad [\![ A ]\!]\vDash [\![ B ]\!] \quad \text{ iff } \quad A \vdash B\]
They both have a sense of consequence, so we expect these to agree. The problem is: what if they don’t? This is similar to the problem of a formal model which disagrees with your starting assumptions / intuitions / data. Did you make a mistake in your definitions? Did you make a computational error? Or were your starting intuitions wrong? Or did you have bad data?
. . .
\[\text{However: }\quad [\![ \text{Amy is poor but honest} ]\!]\nvDash [\![ \text{Wealth+honesty are related} ]\!]\]
\[\quad \ \text{... yet: } \quad [\![ \text{Amy is poor but honest} ]\!]\vdash [\![ \text{Wealth+honesty are related} ]\!]\]
Which side of this biconditional has explanatory priority? At the core of this debate is whether it is more enlightening to first understand the use of language or to understand the meanings of the components of our language.
Background (6/6): project timeline
- 2024: Formal pragmatics \(\to\) semantics construction for propositional logics
(5 min) There has been a lot of ink spilled both ways in this debate (e.g. “Why Meaning (Probably) Isn’t Conceptual Role” (fodor1993meaning?)). This book, Reasons for Logic, starts with a notion of pragmatic rationality (in terms of assertions and denials) and derives a semantic space, semantic consequence relation, and recursive semantic clauses. It shows how depending on the structure of the input pragmatic reason relation, when you turn the semantic crank you might end up with any variety of substructural (propositional) logics.
. . .
- Concise presentation of the technical formalism, showing design decisions as ‘natural’
- Generalization to syntax with subsentential structure (e.g. predicate logic)
However, there were two issues from my perspective!
- it was not easy to concisely explain the work and justify all of its choices as particularly natural.
- the wide scope was limited syntactically to logics that had no subsentential structure. E.g. no FOL.
Background (6/6): project timeline
Project Timeline
2024: Formal pragmatics \(\to\) semantics construction for propositional logics
2025: Described as the \(\eta\) of an adjunction involving simple, commonplace categories.
The first issue was addressed in work I did in 2025, which I presented at ACT 2026. It turns out, in some sense, the technical apparatus was “just” the unit of a particular adjunction, the free addition of Girard quantale structure to their model of a pragmatic system of norms.
. . .
2026: Generalized internally to any \(\mathcal{E}\) (some fixed topos with a natural numbers object)
2026: Instantiate \(\mathcal{E}\mapsto \mathsf{Nom}\), use particularities of nominal sets to address predicate logic.
The second issue has really made a lot of progress after a comment of David Jaz Myers who encouraged me to look into nominal sets. In order to take that advice, it was important to formulate the above in terms of an arbitrary topos.
Technical Outline
- The ‘free sequent-set’ functor
- Girard quantales
- Implication frames + the logical completion
- Interpreting MALL and classical logic in a frame
- Nominal sets to model subsentential structure
(7 min) Here is the mathematical story. I’ll first have to tell you the propositional story at a topos-agnostic level before telling you about nominal sets.
The free sequent-set functor
\[F^\vdash \colon \mathcal{E}\to \mathsf{Quant}_\mathcal{E}\]
This functor sends an object of a topos to the power object of its object of sequents, which are pairs of (internal) multisets on that object.
So, in Set, this sends a set of propositional atoms to subsets of the set of all propositional sequents you could build out those elements. (we admit that we have baked in the exchange law (by using commutative monoids) into our framework.)
The free sequent-set functor … is a left adjoint
\[F^\vdash \colon \mathcal{E}\to \mathsf{Quant}_\mathcal{E}\qquad U^\vdash \colon \mathsf{Quant}_\mathcal{E}\to \mathcal{E}\]
All three composite functors of the free sequent-set functor are left adjoints, so the overall functor is one too. Obviously the free commutative monoid and free join completion are, but so is the doubling functor (which is left adjoint to itself).
. . .
The (co)unit might seem kind of messy at first…
\[\begin{align*} \eta^\vdash_X(x) &= \langle \{([x],0)\}, \{(0,[x])\} \rangle\\ \varepsilon^\vdash_X(S) &= \bigvee\big\{\textstyle\bigotimes_j a^+_j\otimes\bigotimes_k b^-_k \ \big|\ \langle\sum_j(a^+_j,a^-_j),\sum_k(b^+_k,b^-_k)\rangle\in S\big\} \end{align*}\]
I think these (co)unit formulas are quite intimidating and maybe even suspicious at first glance. In particular, if “S” is a set of pairs of multisets of pairs of elements, it seems to be discarding about half of its data (the negative “a” stuff and the positive “b” stuff).
The free sequent-set functor … is a left adjoint
\[F^\vdash \colon \mathcal{E}\to \mathsf{Quant}_\mathcal{E}\qquad U^\vdash \colon \mathsf{Quant}_\mathcal{E}\to \mathcal{E}\]
… but the oddness comes from the doubling self-adjunction:
\[\mathsf{CMon}(X^2,Y)\cong \mathsf{CMon}(X,Y)^2\cong \mathsf{CMon}(X,Y^2)\]
\[\begin{align*} \eta^{\rm Dbl}_X(&x) &=&\ \langle (x,0), (0,x) \rangle\\ \varepsilon^{\rm Dbl}_X(\langle (a,b)&,(c,d)\rangle) &=&\ a+d \end{align*}\]
But this is just because the doubling functor adjunction isn’t very familiar to us. We’re used to free monoids and join completions, but the the doubling functor happens to have these units and counits.
Internal Girard quantales live inside pointed quantales
A sequence of forgetful functors:
So hold that thought on the free sequent-set functor.
The second ingredient involves a sequence of forgetful functors. We start with the category of quantales internal to our topos. There is a forgetful functor from pointed quantales, which have a global point and therefore an internal-hom operation (which we’ll call the bot operation). We then could define a wide subcategory including just the morphisms compatible with the double-bot operation.
Then it turns out that the full subcategory where the double-bot operation is the identity is the category of internal of Girard quantales (these are thin, cocomplete, star-autonomous categories).
. . .
Girard quantales are a reflective subcategory of pointed quantales with continuous maps
(I can explain more with a hidden slide, but let’s move on for now).
Extra: Pointed quantales and residuation
\[\begin{align*} (-)^\bot\in\ &\mathsf{Sup}_\mathcal{E}(\mathcal{Q},\mathcal{Q}^{\rm op}) :=& a\mapsto \bigvee\{b\ |\ a\otimes b\leq \bot\}\\ j(-) \in\ &\mathsf{Quant}_\mathcal{E}(Q,Q) := &(-)^{\bot\bot} \end{align*}\]
Dashed lines are supp-lattice morphisms, solid lines are quantale homomorphisms
Given any pointed quantale in our topos, we can define a residuation (or internal hom) which is an internal Sup-lattice morphism to the opposite suplattice. If we do this twice, however, we get a quantale morphism.
When we epi-mono factorize this, we get a quantale that has some interesting properties.
Internal implication frames (1/4): definition
An object of \(\mathsf{IF}^{\rm cont}_\mathcal{E}\) is a pair \((X,I)\)
- An object \(X \in \operatorname{Ob}\mathcal{E}\)
- A sequent sub-object \(I \rightarrowtail \mathbb{N}[X]^2\quad\) (i.e. \(1\to F^\vdash X\))
Now we can take a pullback of two of the functors we’ve seen so far to define the category of something called an implication frames internal to our topos. An implication frame (what the philosophers called it) is an object equipped with a distinguished subobject of its object of sequents. So in Set this is a set (of propositional atoms) equipped with a subset of all the possible pairs of multisets one could build.
This is precisely the toy model of pragmatic reason relations: there is a norm governing the assertions and denials of various claimables, but no structure is antecedently presumed about this pragmatic consequence relation.
Internal implication frames (2/4): example frame in \(\mathsf{Set}\)
Some assumptions about a frame \((X,I)\) to make it finitely representable:
\(X=\{a,b\}\)
Multiplicity doesn’t matter for whether or not a sequent is good or not.
\[\begin{array}{||c||c|c|c|c||} \hline\hline \mathcal{P}(X)^2 & 0 & a^- & b^- & a^-b^- \\ \hline\hline 0 & \vdash & \vdash a & \vdash b & \vdash a,b \\ \hline a^+ & a \vdash & a\vdash a & a \vdash b & a \vdash a,b \\ \hline b^+ & b\vdash & b \vdash a & b \vdash b & b \vdash a,b \\ \hline a^+b^+ & a,b\vdash & a,b\vdash b & \vdash & a,b\vdash a,b\\ \hline\hline \end{array}\]
Even though the definition is simple, I just wanted to show a simple implication frame concretely so that you have a feel for one. This one has two possible things that can be said and, of the 16 possible sequents that can be built out of those atoms,
. . .
\[\begin{array}{||c||c|c|c|c||} \hline\hline I & 0 & a^- & b^- & a^-b^- \\ \hline\hline 0 & \checkmark & \checkmark & \times & \checkmark \\ \hline a^+ & \times & \checkmark & \times & \checkmark \\ \hline b^+ & \times & \times & \checkmark & \checkmark \\ \hline a^+b^+ & \checkmark & \checkmark & \checkmark & \checkmark \\ \hline\hline \end{array}\]
E.g. in this frame:
\[a\vdash a\]
\[\quad \vdash a\]
\[b\nvdash a\]
In this example frame, 11 of the 16 are endorsed by the frame. It showcases an example of nonmonotonicity: ‘a’ is a theorem but ‘b’ does not imply ‘a’.
Extra: Why represent radically substructural relations?
Logical consequence relations are a source of $ $ relations. Common assumptions:
- monotonicity: weakening, portability of reasoning
- transitivity1: (mixed) cut, composability of reasoning
Ordinary language monotonicity violation:
“I’ll strike a match, \(x\)” \(\textcolor{red}\vdash\) “\(x\) will light” ||| “I’ll strike a match, \(x\)”, “\(x\) is wet” \(\nvdash\) “\(x\) will light”
Ordinary language transitivity violation:
“bird(\(x\))” \(\textcolor{red}{\vdash}\) “flies(\(x\))” ||| “penguin(\(x\))”, “flies(\(x\))” \(\vdash\) ||| “bird(\(x\))”, “penguin(\(x\))” \(\nvdash\)
Transitivity violation from distinguishing explicit contradictions from implicit ones:
\(C \wedge \neg C\vdash\) ||| \(C \wedge \neg C\vdash A \wedge \neg A\) ||| \(B\vdash A\wedge \neg A\) ||| \(B \textcolor{red}\nvdash\)
One may say “good reasoning” ought satisfy these because, look how successful mathematics and scientific communities have been! If we’re taken in by such a suggestion, we’ll then revisit the earlier implications we wrote and then conclude we must have been wrong.
But this gets the priority backwards modeling reason relations and the reason relations themselves: if the logician’s toolset is insufficiently rich to account for representing the “follows from” relation of a social practice, then it’s not the social practice that is wrong.
Internal implication frames (3/4): free pointed quantale
The pullback of a left adjoint along a fibration is itself a left adjoint, so \(\pi_{\mathsf{PQ}}\) is a left adjoint!
So we’ll use the fact that being a left adjoint is preserved by a pullback with a fibration.
This means that our pullback projection pi-PQ is a left adjoint as well.
Internal implication frames (4/4): free Girard quantale
An object of \(\mathsf{IF}^{\rm cont}_\mathcal{E}\) is a pair \((X,I)\)
- An object \(X \in \operatorname{Ob}\mathcal{E}\)
- A sequent sub-object \(I \rightarrowtail \mathbb{N}[X]^2\quad\) (i.e. \(1\to F^\vdash X\))
Compose free pointed quantale with \(\mathsf{GQ}\) reflective subcategory adjunction:
The pullback projection to pointed quantales is also a left adjoint, so we can compose the adjunction with the Girard quantale reflective subcategory to get the overall adjunction which I claim is the mathematical core of the philosopher’s pragmatics-to-semantics pipeline, which they had uncovered via different means.
Semantic consequence relation
The unit is \(\eta_\mathcal{X}\colon \mathcal{X}\to \hat{\mathcal{X}}\) where \(\hat{\mathcal{X}}:=(\hat{X},\hat{I})\) is the corresponding semantic frame.
\[\hat X = \{(A,B)\ |\ A,B \in F^\vdash X, A=A^{II}, B=B^{II}\}\]
Semantic values are pairs of sub-sequent objects (premisory role and conclusory role)
- Only the former is relevant to consequence when the value is a premise
- Only the latter is relevant to consequence when the value is a conclusion
\[\langle a_+,a_-\rangle,\langle b_+,b_-\rangle \vDash \langle c_+,c_-\rangle,\langle d_+,d_-\rangle \iff a_+\otimes b_+\otimes c_-\otimes d_- \subseteq I\]
Semantic values come equipped with a classical negation: swap!
\[\qquad \eta(x)\mapsto \langle \{([x],0)\}^{II}, \{(0,[x])\}^{II}\rangle \] \[\text{Conservativity:}\quad \Gamma \vdash \Delta \iff [\![ \Gamma ]\!]\vDash [\![ \Delta ]\!]\]
The key thing is the unit of the adjunction.
The elements of the semantic frame are pairs of elements of the free sequent-set object, which has elements which are subobjects of pairs of multisets. Importantly these are the closed such sequent-sets. The philosophers call these “implicational roles”. It’s a kind of equivalence class which identifies things which can be substituted for each other without changing the goodness of an inference in any context.
We start with some implication frame and end up with an upgraded one (which has its own consequence relation) and an interpretation into it.
We can understand the upgraded frame as the semantic frame whose elements are semantic values.
Special kinds of implication frames
| Formula | Interpretation | Formula | Interpretation |
|---|---|---|---|
| \([\![ \neg A ]\!]\) | \(\langle \texttt{a}_-,\texttt{a}_+\rangle\) | \([\![ A\wedge B ]\!]\) | \[\left\langle \begin{matrix} \texttt{a}_+ \otimes \texttt{b}_+, \\ \texttt{a}_-\wedge \texttt{b}_- \wedge (\texttt{a}_-\otimes \texttt{b}_-) \end{matrix} \right\rangle\] |
| \([\![ A\otimes B ]\!]\) | \(\langle \texttt{a}_+\otimes \texttt{b}_+,\texttt{a}_+\mathop{\mathrm{\raisebox{-0.2ex}{⅋}}}\texttt{b}_+\rangle\) | \([\![ A\oplus B ]\!]\) | \(\langle \texttt{a}_+ \vee \texttt{b}_+,\, \texttt{a}_- \wedge \texttt{b}_- \rangle\) |
DeMorgan duals: classical disjunction \(\vee\), multiplicative disjunction \(\mathop{\mathrm{\raisebox{-0.2ex}{⅋}}}\), additive conjunction \(\&\)
One thing I’ll forgo is an explanation of how to ‘naturally’ derive these semantic clause formulas. These are operations you can perform on any semantic values of any implication frame.
. . .
Reflexive implication frames:
- contain all sequents \(x \vdash x\)
- Semantic consequence is supralinear
Indefeasibly-reflexive+contractive frames
- contain all sequents \(\Gamma, x \vdash x, \Delta\)
- \(\Gamma, x \vdash \Delta\iff \Gamma,x,x\vdash \Delta\)
- Semantic consequence is supraclassical
Note it is exactly MALL when reflexive sequents are the only good sequents.
This is nice because we have a test for taking our domain of interest and picking an appropriate logic for modeling it. It’s kind of obvious, but if you ever have any inferences whose goodness relies on multiplicity somewhere, obviously classical logic is not suited for what you’re trying to do and you should reach for something closer to linear logic.
The book talks more about all sorts of substructural logics (e.g. K3, ST) which likewise can be characterized in terms of features of the implication frame. One thing that is interesting is that linear logic is appropriate just in virtue of satisfying reflexivity: you don’t need cut!
Extra: Supralinearity
\[\boxed{ \begin{array}{c} \Gamma \vdash A, \Delta\\ \hline\hline \Gamma,\neg A \vdash \Delta \end{array} }\]
\[ \begin{align*} &&\pi_2(\langle \texttt{a}_+,\texttt{a}_-\rangle) &\subseteq (\Gamma_+\Delta_-)^\bot \\ {\scriptscriptstyle \iff\hspace{-3mm}}&& \texttt{a}_- &\subseteq (\Gamma_+\Delta_-)^\bot \\ {\scriptscriptstyle \iff\hspace{-3mm}}&& \pi_1(\langle \texttt{a}_-,\texttt{a}_+\rangle) &\subseteq (\Gamma_+\Delta_-)^\bot \\ \end{align*}\]
\[\boxed{ \begin{array}{c} \Gamma, A\vdash \Delta\\ \hline \hline \Gamma \vdash \neg A,\Delta \end{array} }\]
\[\begin{align*} &&\pi_1(\langle \texttt{a}_+,\texttt{a}_-\rangle) &\subseteq (\Gamma_+\Delta_-)^\bot \\ {\scriptscriptstyle \iff\hspace{-3mm}}&& \texttt{a}_+ &\subseteq (\Gamma_+\Delta_-)^\bot \\ {\scriptscriptstyle \iff\hspace{-3mm}}&& \pi_2(\langle \texttt{a}_-,\texttt{a}_+\rangle) &\subseteq (\Gamma_+\Delta_-)^\bot \\ \end{align*}\]
\[\boxed{ \begin{array}{c} \Gamma,A,B \vdash \Delta \\ \hline\hline \Gamma, A \otimes B\vdash \Delta \end{array} }\]
\[ \begin{align*} \texttt{a}_+ \texttt{b}_+ &\subseteq \Gamma_+\Delta_-^\bot \\ \text{ (Holds }&\text{by defn)}\\ \end{align*} \]
\[\boxed{ \begin{array}{c} \Gamma \vdash A,\Delta \quad \Theta \vdash B,\Omega \\ \hline \Gamma, \Theta \vdash A \otimes B, \Delta,\Omega \end{array} }\]
\[ \begin{align*} (\Gamma_+\Delta_-\subseteq \texttt{a}_-^\bot) &\wedge (\Theta_+\Omega_- \subseteq \texttt{b}_-^\bot) \\ {\scriptscriptstyle \implies} \Gamma_+\Delta_- \Theta_+&\Omega_- \subseteq \texttt{a}_-^\bot \texttt{b}_-^\bot\\ {\scriptscriptstyle \iff} \Gamma_+\Delta_- \Theta_+&\Omega_- \subseteq (\texttt{a}_- \mathop{\mathrm{\raisebox{-0.2ex}{⅋}}}\texttt{b}_- )^\bot\\ \end{align*}\]
\[\boxed{ \begin{array}{c} \Gamma, A \vdash \Delta \quad \Gamma, B \vdash \Delta\\ \hline\hline \Gamma, A \oplus B \vdash \Delta \end{array} }\]
\[ \begin{align*} (\Gamma_+\Delta_- \subseteq a_+^\bot)&\wedge (\Gamma_+\Delta_- \subseteq \texttt{b}_+^\bot) \\ {\scriptscriptstyle \iff} \Gamma_+\Delta_- &\subseteq \texttt{a}_+^\bot \wedge \texttt{b}_+^\bot \\ {\scriptscriptstyle \iff} \Gamma_+\Delta_- &\subseteq (\texttt{a}_+ \vee \texttt{b}_+)^\bot \\ \end{align*}\]
\[\boxed{ \begin{array}{c} \Gamma \vdash A,\Delta\\ \hline \Gamma \vdash A \oplus B,\Delta \end{array} }\]
\[ \begin{align*} \Gamma_+\Delta_- &\subseteq \texttt{a}_-^\bot \\ {\scriptscriptstyle \implies} \Gamma_+\Delta_- &\subseteq \texttt{a}_-^\bot \vee \texttt{b}_-^\bot \\ {\scriptscriptstyle \iff} \Gamma_+\Delta_- &\subseteq (\texttt{a}_- \wedge \texttt{b}_-)^\bot \\ \end{align*}\]
The quantale operation otimes in the validations to the right of each rule is represented via concatenation for space. Invertible steps are denoted with , whereas implications are denoted with .
parr and & need not be checked, as they are definable as De Morgan duals of and .
. . .
Suppose \(\Gamma \vdash_{\rm MALL}\Delta\). By cut-elimination for MALL, \(\Gamma \vdash_{\rm MALL}\Delta\) has a cut-free proof. The base case is that the proof is a single identity rule, which holds in \(\mathcal{X}'\) in virtue of being a reflexive implication frame. Each remaining step in the proof is a logical rule of MALL, which holds in \(\mathcal{X}'\). Therefore \(\Gamma \vDash \Delta\). That the valid atomic sequents are precisely \(\bot\) is a restatement that \(\eta_\pm\) is conservative.
Conservativity in logic means that the addition of new vocabulary does not change the goodness of inferences between sentences that only use the old vocabulary. This is requiring that morphisms not merely preserve but also embed it.
Extra: Idempotent Example (1/3)
Let \(\mathcal{X}:=(X,\bot_\mathfrak{B})\) where \(X=\{a,b\}\) and \(\bot_\mathfrak{B}\) is given by the following table.
E.g. \(a\vdash a,b\) and \(a\nvdash b\) for this frame.
\[\begin{array}{||c||c|c|c|c||} \hline\hline \bot_{\mathfrak{B}} & 0 & a^- & b^- & a^-b^- \\ \hline\hline 0 & \checkmark & \checkmark & \times & \checkmark \\ \hline a^+ & \times & \checkmark & \times & \checkmark \\ \hline b^+ & \times & \times & \checkmark & \checkmark \\ \hline a^+b^+ & \checkmark & \checkmark & \checkmark & \checkmark \\ \hline\hline \end{array}\]
Here is an individual RSR computation
\[\begin{array}{||c||c|c|c|c||} \hline\hline \{a^+\}^\bot & 0 & a^- & b^- & a^-b^- \\ \hline\hline 0 & \times & \checkmark & \times & \checkmark \\ \hline a^+ & \times & \checkmark & \times & \checkmark \\ \hline b^+ & \checkmark & \checkmark & \checkmark & \checkmark \\ \hline a^+b^+ & \checkmark & \checkmark & \checkmark & \checkmark \\ \hline\hline \end{array}\]
Here are all of the singleton RSRs:
\[\begin{array}{||c||c|c|c|c||} \hline\hline (-)^\bot & 0 & a^- & b^- & a^-b^- \\ \hline\hline 0 & \bot_\mathfrak{B}& X_b & X_\pm & \top \\ \hline a^+ & X_\pm & \top & X_\pm & \top \\ \hline b^+ & X_\mp & X_\mp & \top & \top \\ \hline a^+b^+ & \top & \top & \top & \top \\ \hline\hline \end{array}\]
\[X_\pm:=\top\setminus\mathcal{P}[\{a^+,b^-\}] \qquad X_b:=\top \setminus \{b^+,b^+a^-\}\] \[X_\mp :=\top\setminus\mathcal{P}[\{a^-,b^+\}] \qquad \top:=\mathcal{P}[X+X]\]
Let’s do a small example with a language where there are two possible things that can be asserted, a and b. Furthermore, we’ll assume this frame is idempotent, so our candidate implications (which are either simply good or simply bad) have sets rather than multisets on either side of the turnstile. The advantage of idempotent frames is that the set of possible candidate implications is finite: there are just 16 for two propositions. I’ve drawn this to the right, where a + means on the left hand side (the assertions) and a - means the right hand side (the denials). We’ll derive everything in this example mechanically, starting from just this matrix of raw data.
Extra: Idempotent Example (2/3)
Now we can derive more inferential roles in \(\mathbb{R}\) by taking intersections of the singleton roles from the previous table, but this just yields one new role \(X_\bot=\{a^+,b^+\}^\bot = X_\pm\cap X_\mp\).
\[\begin{array}{||c||c|c|c|c||} \hline\hline (-)^{\bot\bot} & 0 & a^- & b^- & a^-b^- \\ \hline\hline 0 & X_b & \bot_\mathfrak{B}& X_\mp & X_\bot \\ \hline a^+ & X_\mp & \bot_\mathfrak{B}& X_\mp & X_\bot \\ \hline b^+ & X_\pm & X_\pm & X_\bot & X_\bot \\ \hline a^+b^+ & X_\bot & X_\bot & X_\bot & X_\bot \\ \hline\hline \end{array}\]
\[\begin{array}{||c||c|c|c|c|c|c||} \hline\hline \vee & X_b & X_\bot & \bot_\mathfrak{B}& X_\pm & X_\mp & \top \\ \hline\hline X_b & X_b & X_b & X_b & \top & X_b & \top \\ \hline % 1 X_\bot & X_b & X_\bot & \bot_\mathfrak{B}& X_\pm & X_\mp & \top \\ \hline % 2 \bot_\mathfrak{B}& X_b & \bot_\mathfrak{B}& \bot_\mathfrak{B}& X_\pm & X_b & \top \\ \hline % 3 X_\pm & \top & X_\pm & X_\pm & X_\pm & \top & \top \\ \hline % 4 X_\mp & X_b & X_\mp & X_b & \top & X_\mp & \top \\ \hline % 5 \top & \top & \top & \top & \top & \top & \top \\ \hline\hline % 6 \end{array}\]
\[\begin{array}{||c||c|c|c|c|c|c||} \hline\hline \otimes & X_b & X_\bot & \bot_\mathfrak{B}& X_\pm & X_\mp & \top \\ \hline\hline X_b & X_b & X_\bot & \bot_\mathfrak{B}& X_\pm & X_\mp & \top \\ \hline % 1 X_\bot & X_\bot & X_\bot & X_\bot & X_\bot & X_\bot & X_\bot \\ \hline % 2 \bot_\mathfrak{B}& \bot_\mathfrak{B}& X_\bot & \bot_\mathfrak{B}& X_\pm & X_\bot & X_\pm \\ \hline % 3 X_\pm & X_\pm & X_\bot & X_\pm & X_\pm & X_\bot & X_\pm \\ \hline % 4 X_\mp & X_\mp & X_\bot & X_\bot & X_\bot & X_\mp & X_\mp \\ \hline % 5 \top & \top & X_\bot & X_\pm & X_\pm & X_\mp & \top \\ \hline\hline % 6 \end{array}\]
The Hasse diagram for the six values of R are shown.
We can compute the two ways to combine inferential roles.
Extra: Idempotent Example (3/3)
We have base cases:
\[[\![ a ]\!]=\langle \{a^+\}^{\bot\bot},\{a^-\}^{\bot\bot} \rangle=\langle X_\mp,\bot_\mathfrak{B}\rangle \qquad [\![ b ]\!]=\langle \{b^+\}^{\bot\bot},\{b^-\}^{\bot\bot} \rangle=\langle X_\pm,X_\mp \rangle\]
We can use the formula for semantic consequence to show that \(\Gamma \vdash \Delta \iff [\![ \Gamma ]\!]\vDash [\![ \Delta ]\!]\).
We can compute syntactically that \({a,b\vdash a\wedge b}\) from \({a,b\vdash a}\) and \({a,b\vdash b}\) and \({a,b\vdash a,b}\) in \(\mathcal{X}\).
We also observe on the right that \({[\![ a ]\!],[\![ b ]\!]\vdash [\![ a\wedge b ]\!]}\).
\[\begin{align*} \pi_1([\![ a ]\!]) \otimes \pi_1([\![ b ]\!]) \otimes \pi_2([\![ a \wedge b ]\!]) &\subseteq \bot_\mathfrak{B}\\ \pi_1([\![ a ]\!]) \otimes \pi_1([\![ b ]\!]) \otimes\qquad \qquad\qquad\qquad\quad& \\ \pi_2([\![ a ]\!]) \vee \pi_2([\![ b ]\!]) \vee (\pi_2([\![ a ]\!]) \otimes \pi_2([\![ b ]\!])) &\subseteq \bot_\mathfrak{B}\\ X_\mp \otimes X_\pm \otimes (\bot_\mathfrak{B}\vee X_\mp \vee (\bot_\mathfrak{B}\otimes X_\mp)) &\subseteq \bot_\mathfrak{B}\\ X_\mp \otimes X_\pm \otimes X_b &\subseteq \bot_\mathfrak{B}\\ X_\bot &\subseteq \bot_\mathfrak{B}\\ \end{align*}\]
\(\mathcal{X}\) satisfies “containment” (\(\Gamma\vdash \Delta \in \bot\) whenever \(\Gamma\) and \(\Delta\) overlap), so \(\vDash\) is supraclassical.
However \(\vDash\) is not monotone: we have \(\ \vDash [\![ b ]\!]\) and \([\![ a ]\!]\nvDash [\![ b ]\!]\).
This fact about the property of the frame satisfying containment therefore the induced semantic consequence relation being supraclassical is one example of many in R4L of how traditional logics (although restricted to propositional logics, such as K3, LP, TS, ST) can all be viewed as the implication spaces of implication frames satisfying such-and-such properties.
Extra: Full NMMS calculus
When restricted to indefeasibly reflexive, contractive frames, the semantics is sound and complete for NMMS (Non-monotonic, multisuccedent logic).
Technical Outline
1. The ‘free sequent-set’ functor
2. Girard quantales
(Hidden: deriving reflector of Girard quantale reflective subcategory)
3. Implication frames and the logical completion
(Hidden: why model radically-substructural reason relations?)
4. Interpreting MALL and classical logic in a frame
(Hidden: Supralinearity proof)
(Hidden: small example frames in \(\mathsf{Set}\) and their logical completion)
(Hidden: Nonmonotonic Multisuccedent Sequent calculus)
- Nominal sets to model subsentential structure
(17:30)
I would describe everything up to this point as “applied category theory of the first kind” where you take something somebody has already done and redescribe it in the language of category theory. This can be elucidating and helpful and various ways (e.g. we can now summarize the pragmatics to semantics pipeline in a pithy sentence, we can now justify their choice of the semantic values (of pairs of sets of pairs of multisets), a semantic consequence relation which seems to ignore half of its input, and semantic clauses which seem scary at first for something as simple as classical conjunction.
However, ACT of the second kind, you solve a problem that the domain expert knew about before they met you.
The category of nominal sets
Two ways of looking at \(\mathsf{Nom}\) the category of nominal sets:
Let \(\mathbb{A}=\{a,b,c,...\}\) be a countably infinite set.
A nominal set is a finitely-supported \(\rm Perm\ \mathbb{A}\) action.
- Each element \(x \in X\) has a support, the variables it depends on.
- If the support is fixed by some permutation \(\pi\), then \(\pi\)’s action fixes \(x\)
There are two different / equivalent ways to view the category of nominal sets. The first considers them as a group action from permutations of a countably infinite set A of names. The constraint is that each element is unchanged by permutations that fix some finite set of names, thus we have a ‘support’ function which tells us, for any element, which names it ‘actually’ depends on.
This is not just a category but a topos. We’ll see later what the power objects look like.
. . .
Let \(\mathbb{I}\) be the category of finite sets and injective maps.
A nominal set is a pullback-preserving functor \(\mathbb{I}\to\mathsf{Set}\).
We can also treat nominal sets as Set-valued functors from the category of finite sets and injections, ones that happen to preserve pullbacks.
. . .
\[\Delta \mapsto \{\text{subset of $X$ which is supported by $\Delta$}\}\]
To connect this to the previous representation, we think of the functor as sending a context ∆ to the elements of X which are supported by ∆.
Also, if you’re familiar with combinatorial species: the objects of Nom are essentially in bijection with combinatorial species; it’s just that the morphisms are more flexible.
Extra: Elements of nominal sets
Let \(X \in \mathsf{Nom}\) and \(Q_{ab} \in X\) be an element with support \(\{a,b\}\).
- this is not necessarily the same thing as a syntax term application \(Q(a,b)\)
- \(\sigma_{ab}\bullet Q_{ab} \ \ \ \ \ \ = Q_{ba}\ \ \ \ \ \overset{?}{=}Q_{ab}\ \ \ \ \ \ \) (in general, may or may not be equal)
- \(\sigma_{ab}\bullet Q(a,b)= Q(b,a)\ne Q(a,b)\) (terms are free nominal set elements)2
This is more and less expressive than standard predicate logic syntax:
- Can represent unordered predicates
- Cannot represent \(Q(a,a)\) — this might as well be an element \(Q'(a)\) with support \(\{a\}\)
- Substitution only defined for free variables (or permutations)
So the elements of nominal sets have a set of names they depend on. It’s easy to think of an element of a nominal set as a predicate applied to some variables, as in FOL; however, this can be misleading. Rather it’s always a quotient of such term: nonidentity permutation of the variables always gives a distinct term. This lets us be still quite abstract about what these elements actually are, beyond the fact that they depend on variables and that variables can be permuted.
What is a nominal implication frame in \(\mathsf{Nom}\)
It is a nominal set \(X\) equipped with a sub-nominal \(I\rightarrowtail \mathbb{N}[X]^2\).
“Claimables” are now allowed to depend on parameters: e.g. \(\psi, P_a,P_b,Q_{ab}\)
Sequent components can share variables: e.g. \(P_a \vdash Q_{ab}\) and \(Q_{ba},P_a \nvdash Q_{ab}\)
\(I\) still picks out the subset of good sequents, but it must be equivariant:
label names cannot matter: \(P_a \vdash Q_{ab} \iff P_b \vdash Q_{ba} \iff P_a \vdash Q_{ac}\)
notation to help with this: \(P_- \vdash Q_{-=}\)
So now let’s instantiate our general definition of an implication frame in this specific topos.
A nominal implication frame now has extra structure on its set of propositional atoms. We know what (finite set of) parameters each atom depends on, and we know how non-merging substitutions act on the set of atoms. The sequents you can build out of these atoms can share variables, and the frame picks which sequents are the good sequents. However, now the category Nom imposes a guard rail: our choice of the good sequents can’t depend on the choice of variable names.
What is the free Girard quantale in \(\mathsf{Nom}\)
Consider the elements of \(F^\vdash X\): finitely-supported subsets of \(\mathbb{N}[X]^2\).
- \(I\) itself is such a subset, supported by \(\varnothing\) because it’s equivariant.
- The subset \(\{P_a,P_b\}\) is not equivariant but it is finitely supported
- The infinite subset \(\{P_a,P_c,P_d,...\}\) is not finitely supported.
Let \(\mathfrak{G}\) be the free internal Girard quantale for \((X,I) \in \mathsf{IF}_{\mathsf{Nom}}\).
- These are the \((-)^{II}\)-closed f.s. subsets of \(\mathbb{N}[X]^2\).
\(\mathfrak{G}\) has Girard quantale structure – we can ignore the group action structure and recover propositional connectives on semantic elements, \(\mathfrak{G}^2\).
The sequent-sets that our free sequent-set functor gives us now are not arbitrary subsets of the sequents, but rather those which are finitely supported. I is supported
So we again can look at closed subsets and take pairs of those as semantic elements.
MALL Hyperdoctrine
If we view \(\mathfrak{G}\) from the indexed perspective, we have a functor \(\mathbb{I}\to \mathsf{GQ}\).
We do have more structure which is transparent when viewing the nominal set G as a copresheaf.
. . .
This is the data of a MALL hyperdoctrine if some other properties obtain:
- Left/right adjoints for each \(\Gamma \rightarrowtail \Delta\)
- Frobenius reciprocity
- Beck-Chevalley
We almost have the structure of a hyperdoctrine, though the Beck-Chevalley condition is not guaranteed by default (I think of this in analogy to how reflexivity was required for the semantic clauses of MALL to behave as expected). Let’s approach these components one by one.
MALL Hyperdoctrine: adjoints
Let \(S \in \mathfrak{G}(\Gamma+\Delta)\) with \(\iota\colon \Gamma\hookrightarrow\Delta\).
\[\forall^\Delta_\Gamma(S)=\bigcap_{b \notin \Gamma} S[a:=b] \qquad \text{ and } \qquad \exists^\Delta_\Gamma(S) =(\bigcup_{b \notin \Gamma} S[a:=b])^{\bot\bot}\]
- \(\forall^\Delta_\Gamma\) sends a role to the largest role contained in \(S\) which doesn’t depend on \(\Delta\) names.
- \(\exists^\Delta_\Gamma\) is the smallest role which doesn’t depend on \(\Delta\) names and contains \(S\).
So you can go from a role in a large context to a small are just the intersection and join of the roles in the smaller context that
. . .
\[ \small \begin{align*} y &\leq_\Gamma \forall^\Delta_\Gamma(S) && \\ &\iff y \leq \textstyle\bigcap_{\pi \in G_\Gamma} \pi S && \text{definition}\\ &\iff \forall \pi:\ y \leq \pi S && \text{universal property of }\textstyle\bigcap\\ &\iff \forall \pi:\ \pi^{-1}y \leq S && \phi_{\pi^{-1}}\text{ order-auto.},\ \phi_{\pi^{-1}}(\pi S)=S\\ &\iff \forall \pi:\ y \leq S && y\in \mathfrak{G}(\Gamma),\ \text{so }\pi^{-1}y = y\\ &\iff y \leq S && \text{independent of }\pi,\ \operatorname{id}\in G_\Gamma\\ &\iff \mathfrak{G}_\mathcal{Q}(\iota)(y) \leq_{\Gamma+\Delta} S && \text{weakening is the inclusion} \end{align*} \]
I’ve included a proof.
MALL Hyperdoctrine: Beck-Chevalley and Substitution-equivariance
Let \(\iota\colon \Gamma\rightarrowtail \Delta\). B.C. conditions are:
\[\exists^{a}_\Gamma \cdot \mathfrak{G}(\iota) = \mathfrak{G}(\iota+\{a\}) \cdot \exists^{a}_\Delta \quad \text{ and }\quad \forall^{a}_\Gamma \cdot \mathfrak{G}(\iota) = \mathfrak{G}(\iota+\{a\}) \cdot \forall^{a}_\Delta\]
Although nominal sets don’t naturally support arbitrary substitution, we have something close when there is an internal monoid structure on the set. This property is called substitution-equivariance.
Frobenius reciprocity holds automatically, where things get interesting is Beck Chevalley.
Substitution-equivariance (1/n)
\(A \rightarrowtail M\), is substitution-equivariant iff closed under identifying names in the following sense. Suppose \(\{a,b\}\subseteq \Gamma\) with let \(x_a \in M(\Gamma\setminus\{b\})\) and \(y_b \in M(\Gamma\setminus\{a\})\) and \(x_ay_b \in A(\Gamma)\). Substitution-equivariance means that \(x_ay_a \in A(\Gamma\setminus\{b\})\), where \(y_a:=y_b[b{:=}a]\).
Let me define what it means for a subobject to be closed under arbitrary substitutions. This only makes sense when we’re talking about a subobject of a monoid.
Substitution-equivariance (2/n)
\(A \rightarrowtail M\), is substitution-equivariant iff closed under identifying names in the following sense. Suppose \(\{a,b\}\subseteq \Gamma\) with let \(x_a \in M(\Gamma\setminus\{b\})\) and \(y_b \in M(\Gamma\setminus\{a\})\) and \(x_ay_b \in A(\Gamma)\). Substitution-equivariance means that \(x_ay_a \in A(\Gamma\setminus\{b\})\), where \(y_a:=y_b[b{:=}a]\).
Consider \(\mathbb{A}\) as a nominal set. Then \(\mathbb{N}[\mathbb{A}]\) is the nominal set of multisets of names.
- Let \(A \rightarrowtail \mathbb{N}[\mathbb{A}]\) pick out all multisets which mention some \(a\in\mathbb{A}\) at least twice.
✅: \(\{c^2,a,b\}=\{c,a\}+\{c,b\} \in A(\{a,b,c\})\) and \(\{c,a\}+\{c,a\} \in A(\{a,c\})\)
- Let \(B \rightarrowtail \mathbb{N}[\mathbb{A}]\) be the complement of \(A\).
❌: \(\{a,b\} = \{a\} + \{b\} \in B(\{a,b\})\) and \(\{a\}+\{a\} \notin A(\{a\})\).
Substitution-equivariance (3/n)
\(A \rightarrowtail M\), is substitution-equivariant iff closed under identifying names in the following sense. Suppose \(\{a,b\}\subseteq \Gamma\) with let \(x_a \in M(\Gamma\setminus\{b\})\) and \(y_b \in M(\Gamma\setminus\{a\})\) and \(x_ay_b \in A(\Gamma)\). Substitution-equivariance means that \(x_ay_a \in A(\Gamma\setminus\{b\})\), where \(y_a:=y_b[b{:=}a]\).
Consider Roberts Rules of Order, which states a motion must be seconded for the motion to be considered. We encode this norm in an implication frame.
\({\rm Motion}(a,m),{\rm Second}(b,m)\vdash {\rm Considered}(m)\)
This is an element of \(I\). But we do not want the following in \(I\), which is required by sub. equivariance:
\({\rm Motion}(a,m),{\rm Second}(a,m)\vdash {\rm Considered}(m)\)
Therefore we should allow the possibility of frames which are not substitutionally-equivariant.
Here’s an example from of an implication frame whose subobject \(I\) of good implications is not substitutionally equivariant. It is nevertheless reasonable: requiring substitutional equivariance as part of the definition of a frame is against the pragmatist spirit of taking an arbitrary network of consequence relations as the input data.
Interpretations of quantifiers
For the semantic clause, let \([\![ \phi(\Gamma;a) ]\!]\) have \(\texttt{p}\) as a premisory role and \(\texttt{c}\) as a conclusory role.
\[[\![ \forall a\colon \phi(\Gamma;a) ]\!]:=\langle \forall^a_\Gamma(\texttt{p}),\ \exists^a_\Gamma(\texttt{c}) \rangle \qquad [\![ \exists a\colon \phi(\Gamma;a) ]\!] := [\![ \neg \forall a\colon \neg \phi(\Gamma;a) ]\!]\]
We can think of \(\forall\) as an infinite (additive) conjunction:
\[[\![ \forall a\colon \phi(\Gamma;a) ]\!] \equiv [\![ \mathop{\&}\limits_{b \notin \Gamma} \phi(\Gamma;a)[a:=b] ]\!]\]
The following semantic clause for \(\forall a\colon \phi(\Gamma;a)\) would be tantamount to (if such infinite conjunctions were legitimate formulas).
Extra: Future work
An ordered implication frame is a preorder \((X,\leq)\) equipped with a monotone map \(\mathbb{N}[X^{\rm op}+X]\to 2\)
The order codifies a kind of substitutional license: \(A \leq B\) means that conclusions can be weakened \(A \mapsto B\) and premises can be weakened \(B \mapsto A\).
An enriched implication frame is a \(\mathcal{V}\)-category \(\mathcal{A}\) equipped with a \(\mathcal{V}\)-presheaf in \(\widehat{S[\mathcal{A}^{\rm op}+\mathcal{A}]}\), where \(S(-)\) denotes the free symmetric monoidal \(\mathcal{V}\)-category.
It’s not clear what \(\mathcal{V}\)-enrichment leads to:
In \(\mathsf{Set}\)-enriched setting, a frame a set of substitutions between any two claimables.
There is also a set of reasons why \(\Gamma \vdash \Delta\).
Thank you for listening
And even more thanks to:
Kevin Carlson
David Jaz Myers
Evan Patterson
Lucy Horowitz
And the Research on Logical Expressivism (ROLE) group:
- Robert Brandom, Ulf Hlobil, Ryan Simonelli, Rea Golan, Shuhei Shimamura, and others.