Full completeness

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 \mathcal{C}. Moreover, suppose we have a semantic map \llbracket - \rrbracket mapping every proof \Pi of an entailment A \vdash B to a morphism

\llbracket \Pi \rrbracket : \llbracket A \rrbracket \to \llbracket B \rrbracket

Then this semantic interpretation is fully complete when for every f : \llbracket A \rrbracket \to \llbracket B \rrbracket there exists a proof \Pi of A \vdash B with f = \llbracket \Pi \rrbracket.

References

The notion of full completeness was introduced by Abramsky and Jagadeesan in a paper at FSTTCS 1992. The journal version is

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}
}