Decision Procedures
 

An important feature of the methods we have employed in the last two chapters is that they all provide what logicians call a decision procedure for determining a result. A decision procedure is a procedure which is guaranteed to produce a result in a finite number of steps.  All of the procedures we've set out for determining semantic properties - truth-tables, gappy truth-tables, and truth trees, all guarantee results. All we have to do is to follow the rules, and we will get an answer.

It might seem that all procedures in logic must be decision procedures, but it is an important result is that this is not the case. In fact, logicians have proved that there are undecidable propositions in logic, sentences for which there exists no decision procedure. We will return to the decidable/undecidable distinction a little later in this text.