Soundness theorem
From Wikipedia, the free encyclopedia
In mathematical logic, a logical system has the soundness property if and only if its inference rules prove only formulas that are valid with respect to its semantics. It most cases, this comes down to its rules having the property of preserving truth, but this is not the case in general.
Soundness theorems are among the most fundamental results in mathematical logic. They provide half the reason for counting a logical system as desirable, so to speak. Once we are assured that no falsehoods are provable, the second half of having a desirable system comes from the completeness property which assures us that every validity (truth) is provable. Together they assure us that all and only validities are provable.
Most proofs of soundness are trivial. For example, in an axiomatic system, proof of soundness amounts to verifying the validity of the axioms and the fact that the rules of inference preserve validity (or the weaker property, truth). Most axiomatic systems have only the rule of modus ponens (and sometimes substitution), so it requires only verifying the validity of the axioms and one rules of inference.
Soundness theorems come in two main varieties: weak and strong soundness, of which the former is a special case of the latter.
Contents |
[edit] Weak Soundness
The weak soundness theorem for a deductive system is the result that any sentence that is provable in that deductive system is a true on all interpretations or models of the semantic theory for the language upon which that theory is based. In symbols, where S is the deductive system and L the language together with its semantic theory, and P a sentence of L: ⊢S P, then also ⊨L P. In other words, a system is weakly sound if each of its theorems (i.e. formulas provable from the empty set) is valid.
[edit] Strong Soundness
The strong soundness theorem for a deductive system is the result 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. In symbols where Γ is a set of sentences of L: if Γ ⊢S P, then also Γ ⊨L P. Notice that in the statement of strong completeness, when Γ is empty, we have the statement of weak completeness.
[edit] Relation to Completeness
The converse of the soundness theorem is the semantic completeness theorem. In the strong form, it says for a deductive system and semantic theory that any sentence which is a semantic consequence of a set of sentences can be derived in the deduction system from that set. In symbols: Γ ⊨L P, then also Γ ⊢S P. This result was first explicitly established by Gödel, though some of the main results were contained in the antedated work of Skolem.
Informally, the soundness theorem for a deductive system tells you that everything you can prove in that deductive system is (universally) true. And thus, that undesirable falsehoods cannot be proved. Hence, derivation can be trusted with respect to the semantics. Completeness states that all truths are provable.
Gödel's first incompleteness theorem guarantees that for languages sufficient for doing a certain amount of arithmetic, there can be no effective deductive system that is complete with respect to the intended interpretation of the symbolism of that language. Thus, not all sound deductive systems are complete in this special sense of completeness, in which the class of models (up to isomorphism) is restricted to the intended one. The original completeness proof applies to all classical models, not some special proper subclass of intended ones.
[edit] See also
- Soundness in “informal logic”
[edit] Reference
- Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-568-81262-0.
