Editing Soundness (section)

=== Logical systems ===
In [[mathematical logic]], a [[logical system]] has the soundness property if every [[formula (mathematical logic)|formula]] that can be proved in the system is logically valid with respect to the [[Formal semantics (logic)|semantics]] of the system.
In most cases, this comes down to its rules having the property of ''preserving [[truth]]''.<ref>{{Cite book|last=Mindus|first=Patricia|url=https://books.google.com/books?id=JJe_AW4jhKMC&dq=a+logical+system+has+the+soundness+property&pg=PA36|title=A Real Mind: The Life and Work of Axel Hägerström|date=2009-09-18|publisher=Springer Science & Business Media|isbn=978-90-481-2895-2|language=en}}</ref> The [[Converse (logic)#Categorical converse|converse]] of soundness is known as [[Completeness (logic)|completeness]]. 

A logical system with [[Logical consequence#Syntactic consequence|syntactic entailment]] <math>\vdash</math> and [[Logical consequence#Semantic consequence|semantic entailment]] <math>\models</math> is '''sound''' if for any [[sequence]] <math>A_1, A_2, ..., A_n</math> of [[Sentence (mathematical logic)|sentences]] in its language, if <math>A_1, A_2, ..., A_n\vdash C</math>, then <math>A_1, A_2, ..., A_n\models C</math>. In other words, a system is sound when all of its [[theorem]]s are [[Validity (logic)|validities]].

Soundness is among the most fundamental properties of mathematical logic. The soundness property provides the initial reason for counting a logical system as desirable. The [[completeness (logic)|completeness]] property means that every validity (truth) is provable. Together they imply that all and only validities are provable.

Most proofs of soundness are trivial.{{Citation needed|date=June 2008}} 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 deductive system|Hilbert-style deduction]], it requires only verifying the validity of the axioms and one rule of inference, namely [[modus ponens]] (and sometimes substitution).

Soundness properties come in two main varieties: weak and strong soundness, of which the former is a restricted form of the latter.

====Weak soundness====

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 ⊢<sub>''S''</sub>&nbsp;''P'', then also ⊨<sub>''L''</sub>&nbsp;''P''.

====Strong soundness====

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. In symbols, where Γ is a set of sentences of ''L'': if Γ&nbsp;⊢<sub>''S''</sub>&nbsp;''P'', then also Γ&nbsp;⊨<sub>''L''</sub>&nbsp;''P''. Notice that in the statement of strong soundness, when Γ is empty, we have the statement of weak soundness.

====Arithmetic soundness====

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.  For further information, see [[ω-consistent theory]].