7.1.5 Properties of Calculi (Theoretical Logic)

Relations of provability and validity.

Correctness

(provable implies valid ) A calculus is called correct or sound , iff implies .

Completeness

(valid implies provable ) A calculus is called complete , iff implies .

In this section we will examine the relation between provability () and validity () (and more generally between derivability and logical consequence). Both are relations on formulae. Ideally, they would co-incide, but there is no a-priori guarantee for that. The two key notions with respect to this are:

Correctness

(provable implies valid ) A calculus is called correct or sound , iff implies .

Completeness

(valid implies provable ) A calculus is called complete , iff implies .

If a calculus is correct and complete, provability and validity coincide ( iff ). As a consequence, syntactic formula manipulation can totally replace semantic considerations.

The calculus presented in Section 7.1.3 is in fact correct and complete. Correctness is easy to determine with the methods from Section 1.1.2. We just need to establish that the succedent is a logical consequence of the antecedents for each inference rule. For the axioms and this means that they have to be valid formulae (for all ), and and that all interpretations that make the antecedents true also make the succedent true. In fact, this is the case. Establishing completeness is much more involved, and is beyond the scope of this course.


Aljoscha Burchardt, Stephan Walter, Alexander Koller, Michael Kohlhase, Patrick Blackburn and Johan Bos
Version 1.2.5 (20030212)