A semantics of proofs is fully complete just if every element of the semantics is the denotation of some proof.
In symbols, suppose we have a categorical model of a proof system (e.g. natural deduction in a category . Moreover, suppose we have a semantic map mapping every proof of an entailment to a morphism
Then this semantic interpretation is fully complete when for every there exists a proof of with .
Abramsky, Samson, and Radha Jagadeesan. 1994. ‘Games and Full Completeness for Multiplicative Linear Logic’. The Journal of Symbolic Logic 59 (2): 543. https://doi.org/10.2307/2275407. [arXiv]
@article{abramsky_1994,
title = {Games and {Full} {Completeness} for {Multiplicative} {Linear} {Logic}},
volume = {59},
doi = {10.2307/2275407},
number = {2},
journal = {The Journal of Symbolic Logic},
author = {Abramsky, Samson and Jagadeesan, Radha},
year = {1994},
pages = {543}
}