Soundness

Soundness is a property of arguments and formal proof systems in logic. In deductive reasoning, an argument is sound when it is logically valid and all its premises are true. In mathematical logic, a proof system is sound when everything derivable using its rules is a semantic consequence of the assumptions. These related meanings distinguish the correctness of particular reasoning from the reliability of a general method of derivation. (iep.utm.edu)

Soundness of arguments

An argument consists of premises offered as grounds for a conclusion. Logical validity means that the premises cannot all be true while the conclusion is false. Validity therefore concerns the relationship between premises and conclusion, rather than whether the premises actually hold. Soundness adds the requirement of true premises, so every sound deductive argument has a true conclusion. (iep.utm.edu)

For example, consider this argument in ordinary arithmetic:

1. Every integer divisible by four is even.
2. Eight is divisible by four.
3. Therefore, eight is even.

The argument is valid, and its premises are true, making it sound. By contrast, replacing the second premise with “six is divisible by four” produces a valid but unsound argument. Its conclusion, “six is even,” remains true. This illustrates why an unsound argument need not have a false conclusion: unsoundness identifies a defect in the argument, not necessarily in what it concludes. (iep.utm.edu)

Soundness is principally a deductive standard. Inductive reasoning instead offers support that may make a conclusion probable without guaranteeing it. Such arguments are commonly evaluated in terms of strength and cogency rather than deductive validity and soundness. (iep.utm.edu)

Soundness of formal systems

A formal system specifies expressions and permissible derivations. Its syntax determines which expressions and proofs are well formed; its semantics supplies interpretations under which expressions can be evaluated. Soundness connects these syntactic and semantic aspects. For a set of assumptions $\Gamma$ and a formula $\varphi$, the standard statement is:

Here, $\Gamma\vdash\varphi$ means that a formal proof of $\varphi$ from $\Gamma$ exists. The expression $\Gamma\models\varphi$ means that $\varphi$ is a semantic consequence of $\Gamma$: every admissible interpretation satisfying the assumptions also satisfies the conclusion. In first-order logic, these interpretations are mathematical structures assigning meanings to the language’s symbols. (builds.openlogicproject.org)

Crucially, a sound calculus does not require every assumption used in a derivation to be true. It guarantees that the conclusion holds if the assumptions hold in the relevant interpretation. A sound system may therefore contain correct derivations from false assumptions without establishing their conclusions as unconditional truths. (forallx.openlogicproject.org)

With no assumptions, soundness says that every theorem of the logical calculus is valid. For classical propositional logic, this means every theorem is a tautology, true under every assignment of truth values. When additional, nonlogical axioms are assumed, derived conclusions are instead guaranteed in interpretations satisfying those axioms. (iep.utm.edu)

Proving soundness

A soundness theorem concerns every possible derivation, not merely a sample of successful proofs. Its proof typically uses mathematical induction on the length or structure of derivations. One first establishes the semantic correctness of initial steps, then shows that each rule of inference preserves the required relationship between assumptions and conclusions. This is a standard method in proof theory. (forallx.openlogicproject.org)

For modus ponens, the argument is straightforward: if $P$ and $P\to Q$ are true under a valuation, $Q$ must also be true. In an axiomatic propositional calculus, soundness follows by verifying that every logical axiom is valid and that every permitted inference preserves validity. A truth table can verify the relevant propositional cases. (iep.utm.edu)

In natural deduction, proofs also involve temporary assumptions. The soundness argument must track which assumptions remain open at each line and how rules discharge them. For example, deriving $Q$ under an assumption $P$ can justify $P\to Q$ after that assumption is discharged. The appropriate invariant is that each line follows semantically from the assumptions on which it depends. (forallx.openlogicproject.org)

Completeness and consistency

Semantic completeness is the converse property:

Soundness excludes derivations of invalid consequences; completeness ensures that valid consequences are derivable. A system can be sound but incomplete because its rules establish only some of the consequences licensed by its semantics. When both properties hold, derivability and semantic consequence coincide. (forallx.openlogicproject.org)

Standard calculi for classical first-order logic have both properties. Gödel’s completeness theorem establishes the completeness side of this correspondence. Within model theory, the correspondence also connects consistency with the existence of models. (builds.openlogicproject.org)

Consistency is distinct from soundness. In a classical propositional calculus, soundness ensures that a formula and its negation cannot both be theorems, since they cannot both be true under the same valuation. More generally, if assumptions have a model, a sound system cannot derive a contradiction from them. Soundness does not, however, make contradictory assumptions jointly satisfiable; its guarantee remains conditional on the truth of the assumptions. (iep.utm.edu)

References

1. Validity and Soundnessiep.utm.edu
2. Deductive and Inductive Argumentsiep.utm.edu
3. First-Order Logic — Open Logic Projectbuilds.openlogicproject.org
4. Chapter 22 Soundness and completeness — forall x: Calgaryforallx.openlogicproject.org
5. Chapter 48 Soundness — forall x: Calgaryforallx.openlogicproject.org
6. Propositional Logiciep.utm.edu