A theorem about a logical system L and a semantics S for the formulas of L stating that if a formula is provable in the logic L then it is valid in the semantics S. A soundness theorem confirms that the logic is actually expressing and deriving properties that are valid according to the semantics. See also completeness theorem.