Vladimir Mikulik comments on Diagonalization Fixed Point Exercises

[Vladimir Mikulik]

I’m confused about Q9.

Given the way $Syn(A,B)$ is defined, it’s unclear to me how we ensure type correctness of $Syn(S_1\times S_1,S_0)$. In what sense is $S_1\times S_1$ a set of sentences (rather than a set of pairs of sentences)? What does an element of that set look like?

[Scott Garrabrant]

Yeah, it is just functions that take in two sentences and put both their Godel numbers into a fixed formula (with 2 inputs).