The semantic meaning of theories interprets the theories of different lambda calculi in different (sentence-theoretical, domain-theoretical, category-theoretical, game …) models. To let $ T $ Let the theory of such a Lambda calculus $ lambda _? $, If I understand correctly, a denotation semantics for $ lambda _? $ is therefore only a model for $ T $,

The question here is that the application of the tools and methods of model theory to the semantics of labels has yielded useful results. For example, what does LĂ¶wenheim-Skolem's theorem say about the semantics of naming various lambda stones?