Lesson 12

First-order expressions can be encoded as strings in an appropriate alphabet. Let us fix a vocabulary \(\Sigma = \langle \Phi, \Pi, r \rangle\). A possible encoding would use the symbols \(F\), \(R\), \(\ast\), \(0\), and \(1\) (for expressing functions, relations, and variables, all with binary indices), along with the logical symbols \(\land\), \(\lor\), \(\neg\), \(\exists\), and \(\forall\), and parentheses. The same alphabet can, of course, encode proofs (which after all are just sequences of expressions).

There is an algorithm for checking whether a string is a proof: Examine all expressions one by one, and determine for each whether it belongs to one of the groups of our axioms for first-order logic. This is not trivial, but not very hard. Then, for each expression that is not an axiom, test whether it follows from two of the previous expressions. There are some important computational questions one may ask here: Given an (encoding of an) expression \(\phi\), is it the case that \(\vdash \phi\), that is, \(\phi\) is a first-order theorem? We call this problem Theoremhood.

Lemma. Theoremhood is recursively enumerable. That is, there is an algorithm which, given an expression \(\phi\), finds a proof if \(\phi\) is a first-order theorem. If \(\phi\) is not a first-order theorem, then the algorithm runs forever.

Proof. The algorithm tries all possible proofs, in lexicographic order, and reports the proof if one of them is indeed a proof of the given expression.◼

Another problem asks: Given \(\phi\), is it valid? We call this problem Validity. The definition of this problem is computationally fearsome: It appears to require that all possible models of a sentence (of which there are uncountably many!) must be checked. At this point, we have no clue on whether Validity is recursively enumerable. We shall show in the next section that it is, by establishing a surprising fact: Validity coincides with Theoremhood; that is, \(\models \phi\) if and only if \(\vdash \phi\). In other words, our tedious and clumsy proof system turns out as powerful as it can be! This would be more than enough for our project of systematizing our search for mathematical truth, if validity in first-order logic were a satisfactory notion of mathematical truth.

But, of course, it is not. As mathematicians, we are really interested in discovering the properties of the universes spoken about in the various vocabularies: the whole numbers and their operations, the real numbers, the graphs. First-order logic is just a notation that allows us to study reasoning about all these interesting universes in a unified way. At any point we want to know whether a sentence is satisfied not by all models (this would be validity), but by our favorite model, whatever this may be at the time.

How can we bridge the gap between what we can do (systematize validity) and what we need (systematize truth in our favorite model)? A very natural way is the axiomatic method. To illustrate the method in an unreasonably favorable case, suppose that we are interested in all sentences that are satisfied by a particular model \(M_{0}\). Let us assume that we have discovered an expression \(\phi_{0}\) such that \(M_{0} \models \phi_{0}\), and, furthermore, the following is true: \(M_{0} \models \phi\) if and only if \(\models \phi_{0} \Rightarrow \phi\). Hence, in this case we could use validity in order to study truth in our “favorite model,” \(M_{0}\).