There is a question on MathOverflow that has been open for a day or two now that someone on FOM might be able to give a clean answer to: https://mathoverflow.net/questions/272982/how-do-we-construct-the-g%c3%b6del-s-sentence-in-martin-l%c3%b6f-type-theory Tim