1.5 Soundness and Completeness

Completeness of a Logical Calculus

• A logical calculus is (semantically) complete if every tautology can be proved within the system.
• A calculus is complete if the following holds for every formula φ: ⊨ φ always implies ⊢ φ.

Resolution Rule for Propositional Logic

• The resolution rule terminates (i.e., the while loop is never infinite) because there can only be 2^n different clauses.
• The algorithm stops when each of these clauses is combined with every other clause to form a resolvent.

Completeness of Logical Calculus for Propositional Logic

• The following logical calculi for propositional logic are complete:
  • The calculus of truth tables
  • The Hilbert calculus with axioms and laws of propositional logic
  • The resolution rule
• This theorem only holds for propositional logic and not for more complex areas of mathematics and logic.

Satisfiability Problem (SAT)

• The satisfiability problem (SAT) is a problem where the runtime of all known algorithms grows exponentially with the number of propositional variables.
• The SAT problem is one of the most famous NP-complete problems in complexity theory.

Propositional Logic

• Propositional logic is an important subfield of mathematical logic that studies the question of how to use the structure of statements in the simplest case propositions to derive new and valid statements.
• It forms the basis for the formulation and evaluation of conditions that play an important role in programming.

Logical Calculus

• There are several formal deduction systems to evaluate propositions, known as logical calculus.
• These include truth tables, the Hilbert calculus with axioms and deduction laws, and the resolution rule.
• All three logical systems are sound, which means that all formulas derived with the rules of the system are valid under all interpretations.
• Furthermore, these three logical calculi are also complete (i.e., every tautology can be derived within the system).

Soundness and Completeness

• A key property of the logical systems discussed is their soundness.
• A logical system (or calculus) has the soundness property if every formula that can be deduced in the system is a tautology, i.e., is true for every possible interpretation.
• If a logical system is not sound, then one can derive formulas that are not true for all interpretations, which is not useful for most applications.

Soundness of Logical Calculus for Propositional Logic

• Each of the following logical calculi for propositional logic is sound:
  • The calculus of truth tables
  • The Hilbert calculus with axioms and laws of propositional logic
  • The resolution rule