Soundness

Definition

A logical system is sound if every derivable formula is semantically valid. Formally: $\Gamma ⊢\varphi ⟹\Gamma \models \varphi$

This states that if $\varphi$ is derivable from $\Gamma$ using the proof rules, then $\varphi$ is true in all models that satisfy $\Gamma$.

Relationship to Completeness

Soundness is the converse of completeness. Together they establish: $\Gamma \models \varphi \text{ if and only if }\Gamma ⊢\varphi$

This equivalence shows that syntactic derivability perfectly matches semantic validity.

Importance

Soundness is a fundamental requirement for any useful logical system. Without soundness, the proof system could derive false statements from true premises, making the logic unreliable for reasoning.

Most standard logical systems are sound:

• Classical propositional and first-order logic
• Intuitionistic logic
• Modal logics with respect to their intended semantics
• Type theories with respect to their categorical semantics

Related Concepts

• Completeness (Logic)
• Consistency (Logic)
• Model Theory
• Proof Theory

References

enderton2001-mathematical-logic vanDalen2013-logic-structure troelstra-schwichtenberg2000-basic-proof-theory