形式體系Tで意味論的に恆眞な命題Aは證明できるT\vDash A\implies T\vdash A。恆眞な命題は定理である

證明と反證のどちらかが與へられる(T\vdash A)\lor(T\cancel\vDash A)

逆は健全性 (soundness)

意味論的完全性 (semantic completeness) を持たない論理を paracomplete logic と呼ぶ