The logic of soundness and completeness
The logic of soundness and completeness is to check whether a formula φ is valid or not. To prove a given formula φ, there are two methods in logic. One is the syntactic method and the other semantic method.
Syntactic method (⊢ φ): Prove the validity of formula φ through natural deduction rules or proof system.
Semantic method (⊨φ): Prove the validity of formula φ through the truth table.
Soundness
Soundness is the property of only being able to prove things “true” or if the system (claims to) prove something is true then it is true.
Let φ1, φ2,…,φn and ψ be formulas of propositional logic. If φ1, φ2,…,φn ⊢ ψ is valid, then φ1, φ2,…,φn ⊨ ψ holds.
The soundness of propositional logic is useful in ensuring the non-existence of proof for any given sequent. A logical system is sound if and only if the inference rules of the system admit only and only valid formulas.
The soundness of logic means that provability implies the satisfiability. So soundness tells us that if we can deduce some formula α from a set of formulas X and the basic rules of natural deduction, then the set of formulas X must imply that the formula α is true.
It is mentioned as:
X⊢α ⟹ X⊨α
Completeness
Completeness is the property of being able to prove all true things or if something is true then the system is capable of proving it. A system is complete if and only if all valid formula can be derived from axioms and the inference rules.
Completeness says that φ1, φ2,…,φn ⊢ ψ is valid iff φ1, φ2,…,φn ⊨ ψ holds.
Assuming that φ1, φ2,…,φn ⊨ ψ holds, the argument proceeds in three steps:
Step 1: We show that ⊨ φ1 → (φ2 → (φ3 → (…(φn → ψ)…))) holds.
Step 2: We show that ⊢ φ1 → (φ2 → (φ3 → (…(φn → ψ)…))) is valid.
Step 3: Finally, we show that φ1, φ2,…,φn ⊢ ψ is valid.
The first and third steps are quite easy; all the real work is done in the second step.
Completeness tells us that if some set of formulas X implies that a formula α is true, then we can prove the formula α from the set of formulas X and the basic rules of natural deduction.
It is mentioned as:
X⊨α ⟹ X⊢α
