Completeness, Axiomatizability, and Decidability

Logical Implication and Soundness

A set of statements T logically implies a statement P if and only if every interpretation and variable assignment that satisfies the sentences in T also satisfies P.

2 Completeness

A logical system of inference procedures and database of statements T is complete if it is possible to derive either P or (NOT P) from the database for every logical sentence P that is implied from the database. Most mathematical theories are sound but not complete, in the sense that it is not possible to give a list of axioms of the theory from which all other true statements of the theory may be derived. For example, Gödel in 1931 proved that the elementary theory of positive integers and any theory including elementary number theory is incomplete in this sense. Gödel's theorem on the incompleteness of elementary number theory was quite a shock when it was published. Years earlier (around 1900) the distinguished German mathematician David Hilbert had issued the challenge to mathematicians world wide to demonstrate rigorously that every true statement of number theory could be derived within the framework of number theory. He said that mathematicians should define a complete set of consistent axioms for mathematics.

Gödel's Incompleteness Theorem dashed all hopes of meeting this challenge. Most computer-based logic systems and rule-based expert systems are also not complete (e.g., MRS [Russell: 1985]). Some resolution-based logic systems are complete. This will be covered in more detail in the next set of notes.

3 Decidability

A question is decidable for some set of objects if there is a procedure that will stop in a finite period of time and determine whether a logical sentence can be proven from the data base. Most systems are semidecidable in the sense that there is a procedure that will stop in a finite period of time if a proof exists, but may not stop at all if the logical sentence is untrue or undecidable.