Soundness & Completeness

Soundness and completeness are properties of proof systems#todo

Definition §

Soundness ^definition-soundness

Let $P_{\Sigma }$ be a set of formulae, and $C$ be a formula. A proof system, $\psi$ is sound if a proof that $P_{\Sigma }$ concludes $C$ implies $P_{\Sigma }$ logically entails $C$:

$$\text{ψ is sound iff }{P}_{\Sigma }{⊢}_{\psi }C⟹P_{\Sigma }\models C$$

• $P_{\Sigma }{⊢}_{\psi }C$: There exists a proof that $P_{\Sigma }$ concludes $C$, in the proof system $\psi$
• $P_{\Sigma }\models C$: See semantic consequences

Completeness ^definition-soundness

Let $P_{\Sigma }$ be a set of formulae, and $C$ be a formula. A proof system, $\psi$ is complete any logical entailment of $P_{\Sigma }$ to $C$ can be proven in $R$:

$$\text{ψ is complete iff }{P}_{\Sigma }\models C⟹P_{\Sigma }{⊢}_{\psi }C$$

• $P_{\Sigma }\models C$: See semantic consequences
• $P_{\Sigma }{⊢}_{\psi }C$: There exists a proof that $P_{\Sigma }$ concludes $C$, in the proof system $\psi$

Casually §

• Soundness means that you cannot prove anything that’s wrong.
  • Obtained by taking the contrapositive of the implication: If $P_{\Sigma }/\models C$ then, $P_{\Sigma }/{⊢}_{\psi }C$
• Completeness means that you can prove anything that’s right.