5.1.9 Calculi

Validity and valid arguments are the fundamental logical concepts underlying the notion of inference. Both concepts are semantically defined, that is, they are defined in terms of models and variable assignments. But from a computational perspective, using models to actually compute what follows from a sentence is impossible. First of all, models may be infinite. But even if we restrict ourselves to using finite models, the fact that the semantic notion of logical consequence (as well as that of validity) is defined with respect to all models makes computation intractable.

Proof Theory

It is the subject of proof theory to capture the notion of inference in terms of syntax. This is done by defining a so-called calculus . A calculus is a set of rules that transform formulas into other formulas by considering only their syntactic structure. This transformation process starts from an input formula. Under certain conditions, a resulting sequence of rule applications is then regarded as a proof for the input formula. If such a proof can be generated for a formula (in a calculus ), is called provable or a theorem (in ). One writes (or just if it is clear what calculus one is talking about).

For a calculus to count as a syntactic counterpart of the semantic notion of inference, provability in that calculus () and validity must co-incide. This is shown by establishing two properties of that calculus.

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 other words, if a calculus is correct and complete, all formulas that are provable in it are also valid, and all formulas that are valid are provable. Of course not every arbitrary set of rules will be a correct and complete calculus - the rules of the calculus have to be the right ones. But if a calculus is correct and complete, syntactic formula manipulation can totally replace semantic considerations. Calculi may even be employed in computational implementation: Various automatic theorem provers have been developed.

In what follows, we will look at a so called tableaux calculus for propositional logic, which is in fact correct and complete. We will use the calculus to prove valid formulae and to verify valid arguments, and in the next chapter we will give it an implementation.