Is there any actual semantic difference between soundness and correctness? Can I use these words interchangeably when talking about formal reasoning, proof, logics, etc.?

Otherwise, is there a specific difference between something that is sound and something that is correct?

  • 3
    $\begingroup$ Soundness is a technical term. Correctness isn't. $\endgroup$ – André Nicolas Sep 6 '13 at 18:23
  • $\begingroup$ Does that imply I should avoid using correctness in formal articles? I do see it quite often however... Or simply that soundness is less likely to be understood outside of the formal community? $\endgroup$ – anol Sep 6 '13 at 19:42
  • $\begingroup$ Soundness is the name of a (family of) results. You should not use "correctness" as a substitute. In informal mathematical English, one can say that an argument is correct, or that it is sound. In that context, they are virtual synonyms. But that's a quite different usage than in the Soundness theorem(s). $\endgroup$ – André Nicolas Sep 6 '13 at 19:50
  • $\begingroup$ Correctness is a technical term in some contexts (although maybe not the ones the OP is asking about.) For example, Shoenfield's absoluteness theorem says that the constructible universe $L$ is $\Sigma^1_2$-correct (but we would not say that it is $\Sigma^1_2$-sound.) $\endgroup$ – Trevor Wilson Sep 6 '13 at 20:55

Usually in logic correctness is a property of sequences/trees of formulas/sequents (depending on the system considered) that express they are valid proofs: that is that they are sequences/trees which are build applying the inference rules of the logic considered.

Soundness is a property of a logic, where by a logic we mean a proof system (i.e. a set of inference rules) and a semantics, basically a logic is sound if every time we have $T \vdash \varphi$ (that is $\varphi$ can be proved by the inference rules from the formulas in $T$) we also have that $T \models \varphi$ (that is $\varphi$ is true in every model of $T$).

So correctness is a concept that belongs to the syntactic setting while soundess links syntax with semantics.

Of course there are other possible use of the term correctness but these use belongs outside the realm of logic (or at least I cannot think of other uses of the word in logics).

Hope this helps.


From our Discrete Math course:

A derivation rule $R$ is correct if for every set $M$ of formulas and for every formula $F$, $M \vdash_R F$ implies $M \models F$: $$M \vdash_R F \Rightarrow M \models F.$$ A calculus (finite set of derivation rules) $K$ is sound or correct if for every set $M$ of formulas and for every formula $F$, if $F$ can be derived from $M$ then $F$ is also a logical consequence of $M$: $$M \vdash_K F \Rightarrow M \models F.$$ and $K$ is complete if for every $M$ and $F$, if $F$ is a logical consequence of $M$, then $F$ can also be derived from $M$: $$M \models F \Rightarrow M \vdash_K F.$$

Therefore, a calculus is sound if and only if every derivation rule is correct.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.