For the time being think of \(\simeq\) as something like “is defined to be”. This will be discussed further later. Think of \(E(x)\) as representing the ‘output’ relation. It is defined in terms \(O\), where \(O\) is defined in terms of \(E\). Mutual recursion is involved. Even at this informal stage it is not hard to see that \(\even\) defines the set of even numbers, in the sense that \(\even(x)\) evaluates to true for even \(x\) and to false for odd \(x\). Here is an informal calculation showing that \(\even(2)\) evaluates to true. In it we use \(\Leftarrow\) for reverse implication. Also we write members of the domain (numbers) directly into formulas, rather than using the machinery of valuations assigning numbers to free variables.