Is there a connection between local soundness and completeness in proof theory, and free objects in category theory?

Question

I was watching Frank Pfenning's lecture series on proof theory, where he described the notions of local soundness, and local completeness.

He described local soundness of a logical connective as, informally: "Not too strong", i.e. we should not be able to prove more than our basic premises using the introduction and elimination rules of a connective, and he described local completeness of a connective informally as it being: "Not too weak", i.e. we should be able to recover the original premises through the elimination rules of the connective after using the introduction rules.

Reading Steve Awodey's intuitive description of the rules characterizing free objects in category theory made me wonder if there is a connection between the principles. Namely, (to paraphrase somewhat from his Category Theory book) he said that free objects are characterized by two properties (he describes it first in terms of free monoids):

1. "No junk": Every element $m \in M$ can be written as the product of elements of the generating set.
2. "No noise": No "nontrivial" relations hold in $M$.

Thus, it seems to me that we could characterize local completeness by "no junk", and local soundness by "no noise", so we should be able, in some sense, to replace the notion of a set of introduction and elimination rules for a connective being locally sound and complete with them being a free object of some category. Has this connection been made explicit anywhere?

Answer 1

I'm not sure if anyone has tried to make a direct connection (probably they have, though not quite in these terms), but there is a very straightforward indirect connection. Local soundness and local completeness are the triangle identities of the adjunctions that define logical connectives; parallel, no junk and no noise are also represented by the triangle identities of the free-forgetful adjunction.

Spelling it out, let's look at conjunction as an example on the logical side and free monoids for the algebraic side. The adjunctions are $\Delta \dashv -\times= \mathbf C \times \mathbf C \to \mathbf C$ and $F \dashv U : \mathbf{Mon} \to \mathbf{Set}$.

The units ($\eta$) and counits ($\varepsilon$) are: $$ \eta_A = \lambda a.\langle a,a\rangle: A \to A \times A \quad \quad \eta_S = \lambda s.[s] : S \to UFS \\ \varepsilon_{(A,B)} = (\pi_1, \pi_2) : (A\times B, A\times B) \to (A,B) \quad \quad \varepsilon_M = \text{fold}_M: FUM \to M $$

The triangle identities are: $$ id_F = \varepsilon_F \circ F\eta \quad \quad id_U = U\varepsilon \circ \eta_U$$

The right hand side of the triangle identities for the type theory example in type theory notation: $$ \frac{\frac{M : A}{\langle M,M\rangle : A\times A}}{\frac{\pi_1(\langle M,M\rangle) : A}{M : A}} \quad \frac{\frac{N : B}{\langle N,N\rangle : B\times B}}{\frac{\pi_2(\langle N,N\rangle) : B}{N : B}} \quad \quad \quad \quad \frac{\frac{M : A\times B}{\langle M,M\rangle : (A\times B)\times(A\times B)}}{\frac{\langle\pi_1(M),\pi_2(M)\rangle : A\times B}{M : A\times B}}$$ The identity being that these steps in derivations can be eliminated. These are local soundness and local completeness respectively.

For algebra, the triangle identities concretely look like (using Haskell inspired notation) $$ id = \text{fold}_{(++,[])}\circ \text{map}\ (\lambda x.[x]) \quad \quad \quad \quad m = \text{fold}_{(\oplus,\epsilon)}([m]) $$ where the right hand side of the first equation is required to be (and is) a monoid homomorphism, and $\oplus$ and $\epsilon$ represent the multiplication and unit of the monoid containing $m$.

The first equation is the "no noise" equation saying if we inject elements into the free monoid and combine them, we get back what we started with, i.e. we didn't lose any distinctions. The second equation is the "no junk" equation saying when we "interpret away" the free monoid, nothing extra gets mixed in.

All these laws may look a bit weaker than normal, but that's because functoriality and naturality give additional equations. For example, the "no noise" equation implies via naturality: $$ f = \text{fold}_{(\oplus,\epsilon)} \circ \text{map}\ f \circ \eta$$