Categorical semantics explained – what is an interpretation?
There are (at least) two different sort of things you can do, roughly corresponding to syntax and semantics.
You can study the internal logic of a category, which lets you use a logical language as a convenient tool for doing calculations with in a category. e.g. objects are types, propositions are subobjects, et cetera.
Conversely, given a suitable language, we can construct its syntactic category consisting of all the types you can construct in the language and the functions you can define between them, and satisfying all of the relations you can prove hold between them. And thus we can use category theory to help us think of type theories.
On the semantic side we can think of a category $T$ (possibly with extra structure; e.g. a sketch) as being a theory. Then models of this theory in a category $C$ will be functors $F : T \to C$ of a certain type.
Of course, these aren't unrelated; if we have the theory of a group, we might then construct $T$ to be its syntactic category, and require the functors defining models of $T$ to be of the sort that preserves the logic used.
Conversely, if we're in the habit of studying functors out of some category $T$, it may be worth considering the theory given by internal language of $T$ and view functors as being models of that theory.
A common type of this construction is one we can do with universal algebra (e.g. the theory of groups, given as operations and equations). If we have some variety of universal algebra, we can take $T$ to be the opposite category of the category of finitely presented algebras, and then models will be functors from $T$ that preserve finite limits.
To address your comment that
that intuitionistic propositional logic (IPL) correspond to bicartesian closed categories (BCC)
the basic idea (and which is similar in other examples of categorical semantics of this sort) is to give a category of sufficiently structured categories $\mathfrak{C}$ (corresponding to the models of our logic) with the morphisms being the morphisms which preserve the logical structure. In the case of IPL, it should be functors which preserve finite products and coproducts.
Let's say by IPL we understand IPL with some atomic propositions $A_1, A_2, \dots$. So each object in $\mathfrak{C}$ should be a bicartesian closed category with an object $A_i^{\mathcal{C}}$ for each atomic proposition $A_i$ and the functors should additionally preserve the interpretation of these symbols. That is, $F : \mathcal{C} \to \mathcal{D}$ is a morphism in $\mathfrak{C}$ if $F$ preserves products and coproducts and $F(A_i^\mathcal{C}) = A_i^\mathcal{D}$.
Our logic itself corresponds to the initial object $0$ in this category. The objects of $0$ will just be the strings generated by the grammar $s = A_i \;|\; s \times s \;|\; s + s \;|\; \top \;|\; \bot $.
The maps in $\mathrm{Hom}_0(X, Y)$ should just be the terms of type $X \to Y$ (where the objects of $0$ are interpreted as types in the obvious way, giving no introduction or elimination rules for the $A_i$) in the simply typed lambda calculus with tuples and sums, modulo I think extensional equality.
What is an interpretation? A functor? I think that's a fair answer. So, the spotlight of your query focuses on the question: what is its domain?
Well, it is good that you say that you have the background, because I'm about to put that to the test - out of necessity so as to be able to make the answer (relatively) succinct.
Let's start from basics ... in a new and different setting.
The fundamental objects studied by logic are predicates, while the fundamental relation addressed is that of inference. We write $A ⊢ B$ to state that predicate $B$ may be inferred from predicate $A$. In a categorical formulation of logic, each predicate is an object, the inference relation is an arrow, so that $A ⊢ B$ could just as well be written $A → B$, while a morphism $f: A → B$ is a proof that witnesses that inference. For that relation, we can just as well write $f: A ⊢ B$, or equivalently as $B ⊣ A: f$; and for bi-directional inferences, we could write $f: A ⊣⊢ B: g$ to denote the relation pair $(f: A ⊢ B, A ⊣ B: g)$.
(Footnote: there actually are attempts to account for sequents within categorical logic, but I won't get into that here. So I restrict inferences so that they have one and only one predicate on the left and right.)
Suppose we call the category that contains the basics of logic $$ - that's our domain.
In logic, predicates are formed by connectives. We'll use this term very broadly to encompass a wide variety of operations, while yet providing uniform treatment for them all. A connective operates on predicates, and in this domain, each such operation will be represented by a functor from various combinations formed of $$ into $$, itself.
For the following, we'll use the following conventions that for a category $$, $||$ denotes its set of objects, while for each $A, B ∈ ||$, $(A,B)$ denotes the set of morphisms for $A → B$ (or $A ⊢ B$ in $$). The unit category is $1$, with $|1| = {0}$ and $1(0,0) = \{1_0\}$. The category $^†$ is the reverse of category $$; and $×$ is the direct product of categories $$ and $$. For a set $T$, we'll denote, by $^T$, the indexed product of $$, where $|^T| = ||^T$ and for each $A, B ∈ ||^T$, $^T(A,B) = ∏_{t∈T} (A(t),B(t))$.
Thus, if $f: A → B$ (or $f: A ⊢ B$) in $$, then $B ← A: f$ (or $B ⊣ A: f$) in $^†$.
Finally, we may also include the category $^⇔$, which is given by $|^⇔| = ||$ and for $A, B ∈ ||$, $^⇔(A,B) = (A,B)×(B,A)$. Distinguished subsets of $^⇔(A,B)$ include $$\{ (f,g)∈^⇔(A,B) ¦ f∘g∘f = f, g∘f∘g = g \}$$ for generalized inverses and $$\{ (f,g)∈^⇔(A,B) ¦ f∘g = 1_B, g∘f = 1_A \}$$ for inverses, which define respective subcategories, the last of which is the maximal groupoid contained in $$.
The corresponding relation in $^⇔$ is $f: A ⊣⊢ B: g$, for $(f,g) ∈ ^⇔(A,B)$.
(I'm a fan of symmetry - and also of Noether - so, I like it when things are made so as to respect duality as much as possible.)
The minimum set of connectives we'll want for $$, along with the functors we'll associate them with, are some or all of those drawn from the following set:
- $⊤,⊥: 1 → $ respectively for True and False,
- $∧,∨: × → $ respectively for And and Or,
- $⊃: ^†× → $, $⊂: ×^† → $ respectively for OnlyIf and Unless,
- $∀,∃: ^T → $, respectively for All and Some: quantifiers bound to a set $T$ of terms of a type, which we'll also call $T$.
With each connective, we associate a natural bijection between two families of inferences, one which contains the connective and the other which does not.
- $(C,⊤) ⇔ 1(0,0) = \{1_0\}$, $(⊥,D) ⇔ 1(0,0) = \{1_0\}$, for $C, D ∈ ||$;
- $(C,A∧B) ⇔ (C,A)×(C,B)$, $(A∨B,D) ⇔ (A,D)×(B,D)$, for $A, B, C, D ∈ ||$;
- $(C,A⊃B) ⇔ (C∧A,B)$, $(A⊂B,D) ⇔ (A,B∨D)$, for $A, B, C, D ∈ ||$;
- $(C,∀A) ⇔ ^T(C,A)$, $(∃B,D) ⇔ ^T(B,D)$, for $A, B ∈ |^T|$ and $C, D ∈ ||$.
And ... that's it!
As I said, I'll put your background to the test. So, as an exercise: describe all of what is entailed by requiring that these be natural bijections. Each of these natural bijections entails a bundle of identities (i.e. commutative diagrams) and corresponding proof rules, as do the corresponding functors.
Intuitionism includes all of these connectives, except the one for Unless; while bi-intuitionism includes them all. A Cartesian closed category is precisely characterized by one which includes the connectives for True, And and OnlyIf. A bi-Cartesian closed category also includes Or and False. (Edit: False is not in a Cartesian closed category, as I originally stated. I corrected that.) A bi-Cartesian bi-closed category also includes Unless ... and always reduces to a partial order (i.e. if $f, f': A ⊢ B$, then $f = f'$).
To this list, we can also add the defined connectives
- $¬,⨽: ^† → $, respectively for strong Not (as "is false") and weak Not (as "not true"),
- $≡,≢: ^⇔ × ^⇔ → $ respectively for Iff and Xor,
- $¬A ⊣⊢ A⊃⊥$, $⨽B ⊣⊢ ⊤⊂B$,
- $A≡B ⊣⊢ (A⊃B)∧(B⊃A)$, $A≢B ⊣⊢ (A⊂B)∨(B⊂A)$.
- $(C,¬A) ⇔ (C∧A,⊥)$, $(⨽B,D) ⇔ (⊤,B∨D)$, for $A, B, C, D ∈ ||$;
- $(C,A≡B) ⇔ (C∧A,B)×(C∧B,A)$, $(A≢B,D) ⇔ (A,B∨D)×(B,A∨D)$, for $A, B, C, D ∈ ||$;
- If $m:C'⊢C$, $n:D⊢D'$, $k:A⊣⊢A':k'$, $l:B⊣⊢B':l'$, then we have $k:A⊢A'$, $k':A'⊢A$, $l:B⊢B'$, $l':B'⊢B$. The morphisms in $(C,A≡B)$ and $(A≢B,D)$ are respectively $(m,(k,k')≡(l,l'))$ and $((k,k')≢(l,l'),n)$. The corresponding morphisms in $(C∧A,B)×(C∧B,A)$ should be $(m∧k',l)$ and $(m∧l',k)$, while those in $(A,B∨D)×(B,A∨D)$ should be $(k',l∧n)$ and $(l',k∧n)$.
- Thus if $f: C∧A ⊢ B$ and $g: C∧B ⊢ A$ map to $h: C ⊢ A≡B$, then $(l'∘f∘m∧k,k'∘g∘m∧l)$ maps to $((k,k')≡(l,l'))∘h∘m$. Similarly, if $f: A ⊢ B∨D$ and $g: B ⊢ A∨D$ map to $h: A≢B ⊢ D$, then $(l'∨n∘f∘k,k'∨n∘g∘l)$ maps to $n∘h∘((k,k')≢(l,l'))$.
Finally, for the quantifiers, we can write
- $(∀x:T)A(x) ⊣⊢ ∀[x:T ↦ A(x)]$,
- $(∃x:T)A(x) ⊣⊢ ∃[x:T ↦ A(x)]$,
An interpretation is simply any category that $$ maps to by a functor - whichever way we choose to define $$. I've given you several alternatives.
As a side-note, it is worth pointing out the following:
- Each of the natural bijections involving $C$ are "left-invariant": we can conjoin extra statements on the left to $C$ on both sides of an equivalence to come up with another instance of the equivalence.
- Each of the natural bijections involving $D$ are "right-invariant": we can disjoin extra statements on the right to $D$ in a similar way.
- It is not possible to create an "internal" lambda abstraction, unless all the rules are left-invariant. The corresponding dual (a "gamma" abstraction, we might perhaps call it) would similarly require all the rules to be right-invariant.
- Right-invariance for the $C$-rules and left-invariance for the $D$-rules characterize "watershed" conditions seen in lattice-theory
- For $⊤$, $⊥$: two-sided invariance is already assured.
- For $∧$, $∨$: two-sided invariance is equivalent to distributivity.
- For $∀$, $∃$: two-sided invariance is equivalent to "indexed distributivity", of the respective forms: $$(∀x)(A(x) ∨ D) ⊢ (∀x)A(x) ∨ D,$$ $$C ∧ (∃x)B(x) ⊢ (∃x)(C ∧ B(x)).$$
- Bi-intutionism has both forms of indexed distributivity, intuitionism has only the one for $∃$, but it is entirely possible to modify intuitionism by adding the one for $∀$ as an extra rule.
- For $⊃$, $⊂$ (or any of $¬$, $⨽$, $≡$, $≢$): two-sided invariance makes the logic a classical logic, and all connectives are defineable and all rules become two-sided invariant. It actually turns the category not just into a partial order, but a boolean lattice.
- Ways to get around the "collapse" issue for bi-cartesian, bi-closed categories are an active area of research; but I personally don't see it as a problem. The relevant condition (that $f,f': A ⊢ B$ entails $f = f'$), in other contexts - like braided monoidal categories - is called "coherence" and is not only a desired property, but is specifically sought for - which is what the "hexagon diagrams" in braided monoidal categories are there for. We can get around collapse by defining different layers of equivalence by which of the commutative diagrams are to be permitted. For bi-intuitionist and classical logic, there would be a intuitionalist layer of weak equivalence, an indexed distributive intuitionist layer and a bi-intuitionist layer.
So, classical logic can be included in this framework by making all of the natural bijections invariant on both the left and right; conjoining a $C$ on the left of all the $D$-rules, and disjoining a $D$ on the right of all the $C$-rules. The roles played by $C$ and $D$ are entirely analogous to the role played by continuations in programming languages and may be deemed, respectively, the "left continuation" and "right continuation" of the rule. In sequent calculus, they are each replaced by finite sequences of statements.
The quantum logic of von Neumann cannot easily be fit into this framework, because it is non-distributive; although in more recent times - by virtue of the work of Isham et al. - von Neumann's logic framework has been superseded by a newer one rooted in bi-intuitionist logic.
The rule $A ⊢ ¬¬A$ is valid in intuitionist logic, while $⨽⨽B ⊢ B$ and $¬B ⊢ ⨽B$ are both valid in bi-intuitionist logic. The inclusion of any of the converses $¬¬A ⊢ A$, $B ⊢ ⨽⨽B$ or $⨽B ⊢ ¬B$ is also a watershed for classical logic. But instead of posing these rules separately - which breaks the simple scheme just laid out here - it's easier to stay within the paradigm by extending the natural bijections to allow continuations on both the left and right.