Soundness theorem

From Wikipedia, the free encyclopedia

Soundness theorems are among the most fundamental results in mathematical logic. They are relative to a particular semantic theory for a formal logical language and a formal deductive system for that language. Soundness theorems come in two main varieties: weak and strong 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

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 semantic 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

"Strong" and "weak" make sense here, as strong soundness considers arbitrary sets of sentences, and the empty set of sentences that is relevant to weak soundness is one such set. For most, but not all, deductive systems of interest, both strong and weak soundness hold.

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 the important case of first-order the completeness theorem is often called Gödel's completeness theorem.) In symbols: Γ ⊨_L P, then also Γ ⊢_S P

Informally, the soundness theorem for a deductive system tells you that everything you can derive or prove with that deductive system is something you would want to be able to derive or prove. And thus, nothing that you would not want to derive can be derived. Hence, derivation can be trusted, with respect to the semantics. Completeness tells you that everything you would want to be able to derive or prove can be derived.

Gödel's first incompleteness theorem guarantees that for sufficiently expressive languages, there can be no deductive system that is complete with respect to a classical semantics upon which every sentence is either true or false. Thus, not all sound deductive systems are complete.

However, a soundness theorem is generally considered a minimal requisite to have an interesting deductive system at all. This is because if a deductive system is unsound, that a sentence can be derived or proven in the deductive system does not tell you anything about the semantic properties of the sentence.