Category Theory – Internal Language Proof of Lawvere’s Fixed Point Theorem for Cartesian Closed Categories

categorical-logicct.category-theorylambda-calculuslo.logic

This proof of Lawvere's fixed point theorem suggests (since it uses $\lambda$ notation) that it is written in the internal language of cartesian closed categories (which is the $\lambda$-calculus, as explained e.g. in Part I of Lambek and Scott's book Introduction to higher order categorical logic). However, one needs quantifiers in order to formulate the notion of point-surjective and the existence of a fixed point $s\colon 1\to B$. So strictly speaking, the proof can't take place in the internal language, since the $\lambda$-calculus doesn't have quantifiers and assumptions. (Higher-order logic admits quantifiers, but that is only available in elementary toposes and not in cartesian closed categories in general.)

Question: Is there some way of making the proof formally work in some "internal language" of cartesian closed categories? Or is the $\lambda$ notation used in the proof just an informal explanation of the proof rather than an indication for the use of the internal language?

Best Answer

You're right that the statement of the theorem, and the entirety of the proof, don't fit inside the internal logic of a CCC. However, once given $f:B\to B$, the definition of $q$ and the proof that it is a fixed point of $f$ can take place inside that internal language.

Related Question