 Given these essential obstacles, Tarski provides a structural definition of the basic semantical notions, i.e., one that relies only on the logical form of an expression and the fact that expressions are recursively defined. But this route is only viable for a language which is structurally described, e.g., a formalized language. For such languages, which are usually closed under quantification and contain formulas with free variables, Tarski elaborates an appropriate notion of satisfaction, which allows him to introduce the notions of definability, denotation, truth, logical consequence. It is then possible to give a precise version and a proof of the adequacy condition (T) in a meta-science, whose principles comprise: (i) general logical axioms, (ii) special axioms that depend upon the object theory we consider, and (iii) axioms for dealing with the fundamental properties of the structural notions, i.e., principles of proof and definition by induction. Given this semantical machinery, Tarski can solve in the negative the problem of the existence of (a formal counterpart of) a universal language, i.e., one where it is possible to define an adequate notion of truth for the same language. Although the theory of simple types, (where the type 0 is the type of individuals; the type \(n+1\) is the collection of all classes of type \(n\) objects) with the axiom of infinity and extensionality is apparently a good candidate as a general metatheory, it is shown that whichever definition we choose in the theory of types for the term “true”, then it is possible to deduce in the same theory the negation of some instance of the adequacy schema (T). In the proof of this theorem, Tarski applies arithmetization and diagonalization, hence following the Gödelian pattern. On the positive side, the concept of truth can be adequately defined for any formalized language L in a language (the so-called metalanguage), provided it is of higher order than L. Also, Tarski’s semantics makes precise Gödel’s remark (1931, footnote 48) that “the true reason of the incompleteness is that the formation of ever higher types can be continued into the transfinite[…], while in any formal system at most denumerably many of them are available”. Tarskian semantical notions play the role of the higher types hinted at by Gödel. To sum up, the outcome of Tarski’s work is that the semantical notions are eliminated in favor of the (extensional) notions of type or set, and a theoretical explanation of semantical paradoxes is finally achieved.