A theorem about a logical system L and a semantics S stating that a formula is provable in the logic L if and only if it is valid in the semantics S. A completeness theorem consists of a soundness and an adequacy theorem: it confirms that the logic is expressing and deriving precisely the properties that are valid according to the semantics.