Soundness theorem
The
soundness theorem is a
theorem in
mathematical logic stating for a given system of inference rules and system of axioms satisfying certain conditions, any first-order formula that is provable is universally valid.
The converse of the soundness theorem (stating that valid expressions are theorems) is known as Gödel's completeness theorem.