@John

> By the way, Keith, you're writing \\(g \circ h\\) to mean "do first \\(g\\) and then \\(h\\)", while most category theorists - and in particular me - use it to mean "do first \\(h\\) and then \\(g\\)", just as we do for functions, where

>

> \[ (g \circ h) (x) = g(h(x)) . \]

So... I have been trying to write up how to use Lawvere's fixed point theorem to prove Gödel's second incompleteness theorem as per our discussion.

In [Lawvere's 1969](http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf) paper I think he used the opposite convention for composition :

> Taking the case \\(X = 1\\), one has that every \\(f : A \to Y\\) gives rise to a

unique \\( \ulcorner f \urcorner : 1\to Y^A\\) and that every \\(1 \to Y^A\\) is of that form for a unique \\(f\\).

> Since for every \\(a : 1\to A\\) one has (dropping the indices \\(A\\), \\(Y\\) on \\(\epsilon\\) when they are clear)

> \\[ \langle a, \ulcorner f\urcorner \rangle = a.f \\]

> one calls the “evaluation” natural transformation; note however that we do not assume

> in general that \\( f\\) is determined by the knowledge of all its “values” \\(a.f\\)

(the above is from page 4)

It's confusing!

> By the way, Keith, you're writing \\(g \circ h\\) to mean "do first \\(g\\) and then \\(h\\)", while most category theorists - and in particular me - use it to mean "do first \\(h\\) and then \\(g\\)", just as we do for functions, where

>

> \[ (g \circ h) (x) = g(h(x)) . \]

So... I have been trying to write up how to use Lawvere's fixed point theorem to prove Gödel's second incompleteness theorem as per our discussion.

In [Lawvere's 1969](http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf) paper I think he used the opposite convention for composition :

> Taking the case \\(X = 1\\), one has that every \\(f : A \to Y\\) gives rise to a

unique \\( \ulcorner f \urcorner : 1\to Y^A\\) and that every \\(1 \to Y^A\\) is of that form for a unique \\(f\\).

> Since for every \\(a : 1\to A\\) one has (dropping the indices \\(A\\), \\(Y\\) on \\(\epsilon\\) when they are clear)

> \\[ \langle a, \ulcorner f\urcorner \rangle = a.f \\]

> one calls the “evaluation” natural transformation; note however that we do not assume

> in general that \\( f\\) is determined by the knowledge of all its “values” \\(a.f\\)

(the above is from page 4)

It's confusing!