Difference between soundness and correctness 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?
 A: 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.
A: 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.
