Skip to content
Axiomatic Wiki
Theorem·T50

Soundness

Whatever a theory proves, it also semantically entails: nothing false in a model of the theory is ever provable from it.

For a language , , and :
In words
For any formula, provability from a theory implies semantic entailment by it: provable consequences are always true consequences.
Rests onF02F03F04F06F08F09F11F12F14A01A02A06A07A08
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A09 (computed from the citation graph, not asserted).

Proof

  1. 1
    Suppose , witnessed by a proof of from : , , , and every entry is justified by one of D104's four clauses. We show, by strong induction on (modus ponens and generalization may reach back to any earlier entry, not just the immediately preceding one): for every L-structure with : .
  2. 2
    Logical axiom. If is a logical axiom: by T47, T48, or T49 (whichever of the three kinds it is, D103): for *every* structure and assignment , not just models of ; in particular for any , with no need for the induction hypothesis.
  3. 3
    Assumption. If : directly from and the theory clause of D095, .
  4. 4
    Modus ponens. If : fix with and an assignment into . By the induction hypothesis at and (both ): and , so in particular and (the form clause of D095, unfolded at ). By the implies clause of D091: . As was an arbitrary assignment into , .
  5. 5
    Generalization. If : fix with and an assignment into . By the induction hypothesis at : , i.e. for *every* assignment into (form clause of D095). In particular, for every : is an assignment into (D087), so . By the forall clause of D091: , i.e. . As was arbitrary, .
  6. 6
    Every clause of D104 preserves the claim from the induction hypothesis, so T08 gives it for every ; in particular at : for every , . This is exactly (D096).
∎

Remarks

Soundness confirms the deduction system never proves anything false - every provable formula holds in every model of the assumptions used to prove it. The converse, that every semantically entailed formula is provable, is Gödel's completeness theorem, built next via the Henkin construction: consistency, Lindenbaum's lemma extending any consistent theory to a maximal one, Henkin witnesses for existential claims, and a model built directly from the syntax of a maximal consistent theory containing them.
Wikipedia ↗FirstOrder.Language.Theory.models_of_provable ↗
Propose an edit1 published revision