Soundness & Completeness

Provable equals valid — Gödel's bridge between syntax and semantics.

The idea

Soundness and completeness relate the two central relations of first-order logic: provability, $\Gamma \vdash \varphi$, which asserts that a formal proof of $\varphi$ from $\Gamma$ exists, and logical consequence, $\Gamma \models \varphi$, which asserts that $\varphi$ is true in every structure satisfying $\Gamma$.

Theorem (Soundness).

If $\Gamma \vdash \varphi$ then $\Gamma \models \varphi$.

Theorem (Completeness (Gödel, 1929)).

If $\Gamma \models \varphi$ then $\Gamma \vdash \varphi$.

The two relations are defined in different vocabularies. Provability is a claim about syntax: a proof is a finite arrangement of symbols assembled by the rules, checkable line by line with no reference to meaning. Consequence is a claim about semantics: it quantifies over every structure that makes $\Gamma$ true.

Soundness is the direction a proof system must have before we trust it at all: the rules never derive a non-consequence. Completeness is the surprising direction: a fixed, finite list of mechanical rules reaches every semantic consequence. Together the theorems say that $\vdash$ and $\models$, though defined entirely differently, hold of exactly the same pairs.

Ways to work on it

• Walkthrough. The two theorems, the consistency form, and their combination.
• Practice. Classify a statement as soundness or completeness.
• Hardest. Derive the compactness theorem from completeness.

Not sure where to start? Take the ten-question placement test.