In a word, the metalanguage, which we may call “LGTC+”, is LGTC plus a theory of the syntax of LGTC. The question that Tarski poses is, then, whether there is a predicate constructible in LGTC+ which verifies the convention T for sentences of LGTC. Tarski solves it negatively by proving the following theorem: