Soundness vs completeness, am I understanding? And proving soundness?

Soundness: $a \vdash b \implies a \vDash b$, i.e. if we can prove something, it will also be true. We don't want a system where we start out with something true and dedice something false. However it is conceivable that even if our system is sound, maybe it's quite incomplete/limited regarding what we can express, which is why we also would like...

Completeness: $a \vDash b \implies a \vdash b$, i.e. if we can show something is true, it's also provable. We want to be able to prove all true statements. However it is conceivable that even though we can prove all true statements, maybe it also proves false ones as well, which is why we'd also like the soundness property from before.

Do I have the right idea?

If so, how would I begin to prove soundness? If we are already given $a \vdash b$ I'm not sure what all we must iterate over in e.g. propositional logic to show that we always get true statements. Especially since it seems possible I could pick a false $b$ that contradicts.


You have the right understanding of what soundness and completeness are. As to how to prove soundness, the right tool is induction - specifically, by induction on proof complexity, you show that there is no witness to "$a\vdash b$" unless in fact $a\models b$.

Exactly what this looks like will depend on the specific proof system you use. In the case of sequent calculus, it amounts to showing that the "basic sequent rules" are soundness-preserving: each rule only deduces sound sequents from sound sequents. Since every proof is well-founded, this means that no unsound sequent can every "creep in."

For example, consider the rule which takes in the sequents $\Gamma\vdash\varphi$ and $\Gamma\vdash\psi$ and outputs the sequent $\Gamma\vdash\varphi\wedge\psi$. Supposing that our "input sequents" are sound, in any model $\mathcal{M}$ of $\Gamma$, $\varphi$ is true (by the first sequent's soundness) and $\psi$ is true (by the second sequent's soundness). But then by the definition of satisfaction, $\varphi\wedge\psi$ is true in $\mathcal{M}$.

That is, from the assumption that $\Gamma\vdash\varphi$ and $\Gamma\vdash\psi$ are each sound, we've concluded "every model of $\Gamma$ satisfies $\varphi\wedge\psi$;" but this latter statement is exactly the soundness of the sequent $\Gamma\vdash\varphi\wedge\psi$!