Suppose you have 1. a grammar for terms of a language; 2. type-assignment rules, 3. a set of reduction rules. You want to prove that your language is adequate for mathematical reasoning. If I understand correctly, the right way to do it is to develop a semantics for it, and then prove certain desirable properties such as soundness and consistency.
I've seen different approaches to this. Usually, a model in set theory is involved. But I believe that is not the only way to do it. Wouldn't, for example, an interpreter for that language on the untyped λ-calculus count as a semantics? So, my question is: what are the different ways to provide a semantics to language?