soundness

Parent: soundness-and-completeness

Soundness

Γ ⊢ φ ⟹ Γ ⊨ φ — anything you can prove is true (in every model of Γ). The proof calculus tells no lies.

Proof — push truth through the rules (syntax → semantics)

This is the easy direction, and it goes by induction on the derivation — the bridge from syntax to semantics is local, rule by rule:

• Base — axioms: check that every axiom is valid (true in all models). (E.g. P → (Q → P) — verify its truth table, as in the example.)
• Step — inference rules preserve truth: for each rule, if the premises are true then the conclusion is. Modus ponens: if A is true and A → B is true in a model, then B is true there. Every line of a proof is thus true in every model of the premises; so the last line, φ, is. ∎

The whole content is: each rule is truth-preserving, so truth flows down the proof from valid axioms to the conclusion.

Non-negotiable — unlike completeness

The two properties are not on equal footing:

• Soundness is mandatory. A proof system that proves even one falsehood is worthless: once ⊢ can reach an untruth, it can (via that untruth) reach anything, so "⊢ φ" tells you nothing about φ. Soundness is the minimum for a proof system to deserve the name — it's what makes ⊢ mean something.
• Completeness is merely desirable. A sound-but-incomplete system is still perfectly usable — it never lies, it just can't reach every truth. Lots of good systems are deliberately sound-and-incomplete (weak theories, decidable fragments, most real proof assistants' automation).

The asymmetry in one line: lose soundness → garbage; lose completeness → merely limited. So you never trade away soundness; you often trade away completeness (for decidability, speed, or a weaker base).

Why it's the property you actually rely on

Soundness is what makes a checked proof trustworthy — the entire point of a small trusted proof kernel: it can only derive things that are true, so a type-checked term really is a proof. In certificate terms, soundness = "a certificate the verifier accepts is genuinely valid." Its contrapositive is a handy tool: ⊭ φ ⟹ ⊬ φ — a non-tautology like P → Q cannot be proved.