completeness

A formal system is complete if we can prove all things right. This is in contrast with soundness, which is the property that you can prove all things wrong.

More formally, a proof system is complete if and only if every logical conclusion is provable. In other words, if , then .

Forms of Completeness

Refutation-completeness

A formal system is refutation-complete if it is able to derive false from every unsatisfiable set of formulas:

Every complete system is refutation-complete, but the opposite is not true. However, we can change the system slightly to prove other logical properties. if we have a set of premises and we want to prove that it entails , we can instead prove that is a contradiction.

Resolution proofs are an example where we only have a refutation-complete system, but we can use this kind of proof by contradiction to prove logical consequences.