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,
defining them in terms of the other connectives by
- $¬A ⊣⊢ A⊃⊥$, $⨽B ⊣⊢ ⊤⊂B$,
- $A≡B ⊣⊢ (A⊃B)∧(B⊃A)$, $A≢B ⊣⊢ (A⊂B)∨(B⊂A)$.
The corresponding natural bijections are
- $𝐋(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 ∈ |𝐋|$;
The last two need further elaboration to make them consistent with the respective functors.
- 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)]$,
and adopt the convention, more broadly, of writing *any* operator that acts on functions equivalently as a binding operator. This treatment of quantifiers stays strictly first-order, avoiding the better-known higher-order type-theoretic formalisms making up the Lambda Cube and is suitable either for single-sorted term signatures, where there is just one type
$T$ whose underlying set includes all terms, or multi-sorted term algebras, where there are multiple types
$T$, each with its own pair of bounded quantifiers.
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.
