Internal language proof of Lawvere's fixed point theorem for cartesian closed categories

Question

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?

Answer 1

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.