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):
- "No junk": Every element $m \in M$ can be written as the product of elements of the generating set.
- "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?