A proof system gives you a game of symbols: axioms, inference rules, and the discipline to write one line after another until the thing you wanted sits at the bottom of the page. That game is purely syntactic — it never once mentions truth. Yet we cheerfully treat a completed derivation as if it had settled a question about what is actually the case. Why are we allowed to? And, going the other way, if some statement really is forced to be true by our assumptions, are we guaranteed a proof of it — or might a genuine truth sit forever beyond reach of the rules?

These two questions are answered by soundness and completeness. Together they are the bridge between two symbols that look almost the same but mean very different things: \vdash (there is a proof) and \vDash (it is true in every model). This one page is about that bridge — how it is built in both directions, and why crossing it lets us say, with a straight face, that proof and truth coincide.

Two turnstiles: \vdash vs \vDash

Fix a set of premises \Gamma and a formula \varphi. There are two completely different ways to say "\varphi follows from \Gamma", and keeping them apart is the whole point.

• Syntactic — \Gamma \vdash \varphi ("provable"): there exists a finite derivation of \varphi using the premises in \Gamma, the axioms, and the inference rules of the proof system. This is about symbol-pushing — a machine could check it. Truth is never mentioned.
• Semantic — \Gamma \vDash \varphi ("entails"): in every model (interpretation) that makes all of \Gamma true, \varphi is true as well. This is about meaning — it quantifies over all possible worlds.

A priori these have nothing to do with each other. One is a fact about pieces of a formal language; the other is a fact about a vast (often infinite) collection of structures. The miracle — and it genuinely is one — is that for first-order logic they turn out to be exactly the same relation.

Why soundness holds: rules preserve truth

Soundness is the direction you should insist on before trusting any proof system — a system that could prove a falsehood would be worse than useless. The good news is that it is the easier half, and the argument is a lovely one: induction on the length of the derivation.

The idea is that every ingredient of a proof preserves truth-in-a-model:

• Axioms are chosen to be logically valid — true in every model, full stop. So the first lines of any proof are safe.
• Each inference rule is truth-preserving: if its premises are true in a model, its conclusion is too. The workhorse example is modus ponens,

In any model where both P and P \to Q are true, the truth table for \to forces Q to be true as well — there is simply no room for Q to be false. Now walk down a derivation line by line: every line is either an axiom (valid) or follows from earlier lines by a rule (truth-preserving), so if the premises \Gamma hold in a model, every line holds — including the last one. That last line is \varphi. Since this works in any model of \Gamma, we have \Gamma \vDash \varphi. That is soundness, and it is exactly why a finished derivation earns your trust.

What completeness buys us

Completeness runs the other way and is far deeper. It says the proof system is strong enough: it has no blind spots. If \varphi is genuinely forced by \Gamma in every model, then a finite derivation of it exists — even though "true in every model" ranged over an unimaginable ocean of structures, some of them infinite. This is Gödel's Completeness Theorem (his 1929 doctoral thesis), and it is one of the pillars of first-order logic.

The usual proof is a beautiful piece of engineering (Henkin's method): to show \Gamma \vDash \varphi \Rightarrow \Gamma \vdash \varphi, you argue the contrapositive. If \varphi is not provable from \Gamma, then \Gamma \cup \{\lnot\varphi\} is consistent — and you build a model for it out of the very syntax itself (terms become the elements of the model). That model satisfies \Gamma but falsifies \varphi, so \Gamma \nvDash \varphi. Contrapositive done. The slogan worth remembering:

The payoff of putting both halves together is that you may freely switch tools. Want to show something is provable? It is often far easier to argue semantically — show it holds in every model — and let completeness hand you the proof. Want to show something is true in every model? Exhibit a derivation and let soundness do the rest. This is the everyday superpower of \vdash\ \equiv\ \vDash.

A corollary you get almost for free: compactness

Here is a striking consequence. A proof is a finite object — it can quote only finitely many premises, no matter how large \Gamma is. Feed that finiteness through the \vdash \equiv \vDash equivalence and out drops the Compactness Theorem.

One direction is trivial (a model of the whole set models each finite part). The other is the content: if every finite chunk is satisfiable, the whole infinite set is. The proof is a one-liner once you have completeness — if \Gamma had no model, then \Gamma \vDash \bot, so by completeness \Gamma \vdash \bot; but that derivation is finite and uses only finitely many sentences of \Gamma, so that finite subset already proves (hence entails) a contradiction and has no model — contradiction.

Why care? Compactness is a machine for building strange infinite models. It underwrites the existence of non-standard models of arithmetic (with "infinite" natural numbers) and the whole subject of non-standard analysis (rigorous infinitesimals), and it is a daily tool in model theory. All of that flows from the humble observation that proofs are finite.