Soundness

Correctness (English soundness ) is an important feature of formal systems or calculi and concerns the relationship between syntax and semantics, which is colloquially: What is formally derivable is also true ( within the given semantics).

In formal logic derivability is expressed by the syntactic derivative operator and inference by the semantic entailment relation: A calculus is correct iff for statements of quantities and always follows. The semantics of closing is model- theoretically defined. if and only if every model of, is also a model of true.

For the correctness of a calculus is sufficient if each derivation rule is conclusive. In a correct calculus can derive any formula that is not true in the model chosen.

The counterpart of the correctness is the completeness of a formal system. It says: What is semantically correct, can be derived as well. Completeness rates are usually much more difficult to prove than correctness rates; so the proof of the correctness of the sequent calculus of predicate logic is not a problem, while the completeness theorem is more difficult.