In sentential logic, we can use the truth-table method to decide the validity or invalidity of any argument. That was already perfectly well known at the beginning of the 20^th century, and it was also perfectly clear that the method was purely mechanical. In predicate logic, we can also use interpretations to investigate and often to establish the validity or invalidity of arguments.

The question remained whether there was any mechanical method for predicate logic that would allow the decision about the validity or invalidity of arguments in predicate logic. Hilbert, in particular, emphasized the significance of this Entscheidungsproblem or decision problem.

In contrast to sentential logic, however, it turns out that there is no mechanical or algorithmic method for deciding the validity of arguments in predicate logic. This fact was discovered by the logicians Alonzo Church and Alan Turing in 1936.

To give a negative answer to the decision problem, one has to characterize in a rigorous way the admissible mechanical or algorithmic methods. That was done (in different ways) by Church and Turing, and they thereby, unwittingly, introduced the basic theoretical notions of a subject that did not yet exist — namely, of Computer Science.

Let us return to the logical issue of establishing the validity of arguments. Thanks to Church and Turing, we know there is no mechanical method of deciding the question for predicate logic. The logician Kurt Gödel had, however, proved in 1929 that a predicate argument is valid if and only if there is a derivation from its premises to its conclusion (this is known as Gödel's Completeness Theorem).

In this module, we extend our derivation system for use in predicate logic—all we need to do is to add introduction and elimination rules for the quantifiers. We start with the very simple universal elimination and existential introduction rules, then finish up with the more complex existential elimination and universal introduction rules.

We have only the one objective in this chapter: learning to use the introduction and elimination rules for the quantifiers. Let's see, then, how we can gain the logical conviction of Socrates' mortality, given that he is human and that all humans are mortal.