feat(model_theory/*): Background for realized types (#17847)
Sets up a future PR on realized types (in model theory):
Creates a bijection `first_order.language.formula.equiv_sentence` between formulas and sentences in a language with extra constants.
Also a few facts about complete theories.
