 Clearly an evaluation attempt of the sort shown above will not terminate. A solution to non-termination is familiar from classical recursion theory, and also from work on the theory of truth: allow the relations defined by our formal machinery to be partial. Not all instances of a relation have to receive a truth value. But these are semantic issues and before getting to them we need to give a proper syntactic definition of the language within which our formulas will be written.