The list of representable sets and relations in your lecture notes is intended to produce an intuition that decidable relations are representable. In fact, this is stated in slide 11. I don't have the precise definition of "decidable" in your course, but by that I mean relations that can be precisely described by algorithms. In fact, can be considered as a programming language and formulas as programs that return true or false. In fact, using Gödel numbers as codes and arithmetical formulas is a remnant from the 1930s, when Gödel's incompleteness theorems were proved. It is more convenient to consider logics dealing with more complicated programming datatypes, like lists and trees.

However, not all formulas can be executed because of quantifiers. A quantifier corresponds to a loop in conventional programming languages, and an unbounded quantifier is an infinite loop. A paradigmatic example of an unbounded loop is a formula defining the relation . This set is definable (in the sense of slide 10 of lecture 11) by the formula where represents the relation "y is the code of a derivation in of the formula with code x." But evaluating for each concrete n requires trying an unbounded number of y's.

If a formula has only bounded quantifiers, then there are two ways to evaluate it. The first is to find if it is true in : we know how to evaluate closed atomic formulas and , and bounded quantifiers require considering only a finite number of cases. The second way is to search for a derivation of either the formula itself or its negation in . If a formula has only bounded quantifiers, then it is numeralwise determined, so one of the derivation exists. For such formulas, these two ways of evaluation are equivalent.

The definition of a substitutable term can be described by an algorithm. This description does not appeal to infinite loops. It just says that the a variable in not in the scope of some quantifiers. This can be described in the language of arithmetical formulas, but the result would be very long.