 (“S” and “T” here are mnemonic for “Source” and “Target” respectively; note that we do not require S ∩ T = ∅, or even that S ≠ T.) Suppose we consider, not the sentential languages of our opening paragraph but rather first-order languages, and take S as the set of closed formulas of such a language and T as the set of models (interpretations, structures,…) for that language, then with R as the relation holding between a closed formula φ and a structure M when M ⊨ φ, fR(S0) and gR(T0) are usually denoted by Mod(S0) and Th(T0). (The labels are intended to suggest “class of all models of” and “theory of”, respectively.) In this case the derived closure operations Th ○ Mod (mapping S0 to Th(Mod(S0))) and Mod ○ Th (understood analogously) on S and T respectively deliver the set of first-order consequences of S0 and the set of all models verifying all the sentences verified by every M ∈ T0. When there is only one such M in the latter case, what is delivered is the class of structures elementarily equivalent to M. (Here we are thinking of classical first-order model theory.)