In logic and deductive reasoning, an argument is sound if it is both valid in form and has no false premises.
In most cases, this comes down to its rules having the property of preserving truth.
In other words, a system is sound when all of its theorems are validities.
The soundness property provides the initial reason for counting a logical system as desirable.
The completeness property means that every validity (truth) is provable.
[citation needed] For example, in an axiomatic system, proof of soundness amounts to verifying the validity of the axioms and that the rules of inference preserve validity (or the weaker property, truth).
If the system allows Hilbert-style deduction, it requires only verifying the validity of the axioms and one rule of inference, namely modus ponens (and sometimes substitution).
Weak soundness of a deductive system is the property that any sentence that is provable in that deductive system is also true on all interpretations or structures of the semantic theory for the language upon which that theory is based.
In symbols, where S is the deductive system, L the language together with its semantic theory, and P a sentence of L: if ⊢S P, then also ⊨L P. Strong soundness of a deductive system is the property that any sentence P of the language upon which the deductive system is based that is derivable from a set Γ of sentences of that language is also a logical consequence of that set, in the sense that any model that makes all members of Γ true will also make P true.
If T is a theory whose objects of discourse can be interpreted as natural numbers, we say T is arithmetically sound if all theorems of T are actually true about the standard mathematical integers.
A deductive system with a semantic theory is strongly complete if every sentence P that is a semantic consequence of a set of sentences Γ can be derived in the deduction system from that set.
In symbols: whenever Γ ⊨ P, then also Γ ⊢ P. Completeness of first-order logic was first explicitly established by Gödel, though some of the main results were contained in earlier work of Skolem.
Informally, a soundness theorem for a deductive system expresses that all provable sentences are true.
Gödel's first incompleteness theorem shows that for languages sufficient for doing a certain amount of arithmetic, there can be no consistent and effective deductive system that is complete with respect to the intended interpretation of the symbolism of that language.
The original completeness proof applies to all classical models, not some special proper subclass of intended ones.