 The other strand starts from research in meta-mathematics: what can mathematical theories say about themselves by encoding interesting properties? In 1952, L. Henkin posed a deceptively simple question inspired by  Gödel’s incompleteness theorems.  In order to formulate Henkin’s question, some more background is needed. As a reminder, Gödel’s first incompleteness theorem states that, for a sufficiently strong formal theory like Peano Arithmetic, any sentence asserting its own unprovability is in fact unprovable. On the other hand, from “outside” the formal theory, one can see that such a sentence is true in the standard model, pointing to an important distinction between truth and provability.