 But the demands on the “correct” language for the formal mode of speech were exorbitant. Carnap had originally wanted to keep it weak and uncontroversial, but it had to be capable of expressing all the mathematics needed for physics. On the other hand, its arithmetized syntax had to be capable of expressing the basic concept of “analytic truth”, or it would be impossible to determine when a formal-mode statement “holds”. Before 1930, it had been assumed that provability was the standard of mathematical truth, but now Gödel had shown that for each consistent and recursively axiomatized system that included enough arithmetic, some true sentences are not provable in the system. So a different criterion was needed, but one that would still—like provability—pick out the logically true sentences solely by means of the formation and transformation rules of the language. Carnap did attempt such a criterion for “analyticity” in the first draft of his syntax book (entitled Metalogic), written in late 1931 and the spring of 1932. He sent the typescript to Gödel, who pointed out that the new criterion was defective. In fact, he added, it is impossible to define analyticity or logical truth in any metalanguage that can be faithfully represented in the object language (e.g., by arithmetization); this is now familiar to us as Tarski’s theorem on the indefinability of truth. So Carnap’s single-language approach fails after all (Awodey &amp; Carus 2007, 2009).