Notes
7
Hodges (1983, p. 94).
8
Actually, Hilbert did not put the Entscheidungsproblem in quite that way:
he asked for a procedure to determine whether a given expression of first-order
logic is valid in every possible interpretation. However, after G¨odel had proved
his completeness theorem, it became clear that the form in which the problem is
stated here is equivalent to Hilbert’s formulation.
9
Work on the Entscheidungsproblem mainly dealt with expressions called
prenex formulas. These are expressions involving the logical symbols ¬⊃
∧∨∃∀with the property that all occurrences of the so-called existential
and universal quantifiers, (∃..)(∀..), are at the beginning of the expression (read-
ing left to right) preceding all other symbols. It was not difficult ...