Is there a formal analogy between the binomial theorem and logical implication?

In classical propositional logic, we have

$$(c \to (a \vee b)) \Leftrightarrow (c \to a) \vee (c \to b).$$

Phrasing this in boolean algebras considered as categories with coproducts and exponentials, this gives an isomorphism (identity)

$$(A+B)^C \cong A^C + B^C$$

whereas in general cartesian closed categories, there is only the canonical morphism from right to left. This situation curiously resembles the binomial theorem, with the mixed terms missing on the right hand side.

I am wondering if there might be a general analogue of expanding the exponential $(A+B)^C$ in logic in the style of the binomial theorem, classical logic being the special case where the mixed terms vanish?

My loose intuition comes from the following: Let s="it's sunday", p="I eat pizza", f="I eat fish", then intuitionistically

$$(s \to (p\vee f)) \not\to (s \to p) \vee (s \to f)$$

because if on every sunday I eat fish or pizza, it doesn't mean that I eat fish every sunday or pizza every sunday. This is roughly what's captured by possible world semantics, and the classical statement does hold if we restrict our consideration to a single sunday (a single world). An expansion

$$(p + f)^s = p^s + f^s + \text{mixed terms}$$

would capture the two extreme cases (pizza every day, fish every day) whereas the mixed terms state that I might eat pizza on some days and fish on others. What could be the possible truths that one had to sum over in general? I hope this question makes any sense and allows for some nontrivial insight :)

• You're mixing types and values. $C$ in the example is a type, but binomial theorem uses fixed numbers. Even a set with size $n$ is not equal to the number $n$, because number $n$ has dependencies between the elements, i.e. successor goes from 0 to n, and ordinary set has no such dependency between the elements by default. This is why you need additional commutative diagram in category theory to define how natural numbers are working. – tp1 Oct 31 '17 at 3:37
• @tp1 I know that $C$ is not a number. I am looking for a generalisation that allows for the exponential to be expanded in the style of the binomial theorem. – Dario Oct 31 '17 at 10:20
• It is common to write $(a + b)^c \equiv a^c + b^c \pmod c$ – DanielV Oct 31 '17 at 13:14
• It may be useful to look at combinatorial species (and how that relates to type theory and such) for an answer to this question. – Anton Malyshev Nov 6 '17 at 17:04

Let $A$, $B$, $C$ be finite sets.
Let $A^B$ be the set of all functions $f:B\to A$, and let $\#(A)$ be the cardinality of $A$.
Let $$S_i=\left\{f\in (A\cup B)^C \mid \#\{c\in C: f(c)\in B\}=i\right\}.$$ Then since the number of $f(c)$ that land in $B$ has to be something, $$(A\cup B)^C=\bigcup_{i=0}^{|C|}S_i = S_0\cup S_1\cup \cdots \cup S_{|C|}$$ where $S_0=A^C$ and $S_{|C|}=B^C$.
• Well... $\forall x(c\to (a\vee b))$ does not imply $\forall x(c\to a)\vee\forall x(c\to b)$ and the possible truths to sum over are all the other possibilities (sometimes $c$ and $a$, sometimes $c$ and $b$...) @Dario – Bjørn Kjos-Hanssen Nov 9 '17 at 16:35