That a definition is “formally correct” means, roughly, that it will be constructed out of non-suspicious vocabulary following non-controversial rules for defining new expressions. But why should one think that a predicate verifying convention T should be, besides, coextensional with the intuitive predicate of truth for LCC?  The reason can be given by an intuitive argument relating both predicates, such as the following (cf. Tarski 1944, pp. 353–4):