<pre><code>ω (\h \lst. (isempty lst) zero (add one ((h h) (extract-tail lst))))
</code></pre>
-
and this will indeed implement the recursive function we couldn't earlier figure out how to define.
In broad brush-strokes, `H` is half of the `get_length` function we're seeking, and `H` has the form:
the identity function. Here's a fixed point for the identity
function:
-<pre>
- Y I
- (\f. (\h. f (h h)) (\h. f (h h))) I
- (\h. I (h h)) (\h. I (h h)))
- (\h. (h h)) (\h. (h h)))
- ω ω
- &Omega
-</pre>
+<pre><code>Y I
+(\f. (\h. f (h h)) (\h. f (h h))) I
+(\h. I (h h)) (\h. I (h h)))
+(\h. (h h)) (\h. (h h)))
+ω ω
+&Omega
+</code></pre>
Oh. Well! That feels right. The meaning of *This sentence is true*
in a context in which *this sentence* refers to the sentence in which
-it occurs is Ω, our prototypical infinite loop...
+it occurs is <code>Ω</code>, our prototypical infinite loop...
What about the liar paradox?