What is semantics in the context of mathematical logic? I have been trying to familiarize myself with the foundations of mathematics, which led me to discussions about propositional, first-order, and second-order logic. I understand that semantics is related to model theory and the satisfiability of models; but I feel that I'm not taking away what I am supposed to.
I understand that in language, semantics defines the "meaning" of words and phrases. Is this analogous to the use of the term in mathematical logic? If so, how does one rigorously talk about the meaning of a statement in logic or math?
Additional insight, sources, and reading recommendations would be greatly appreciated.
 A: Syntax has to do with the formal structure of sentences, proofs, etc., as mere strings of symbols.  For example, a proof is a finite sequence $p$ of strings, each one of which either is an axiom or can be derived from earlier strings in $p$ using the rules of inference (these are syntactical conditions, depending only on the strings of characters involved, without reference to any meaning one might give them).
Semantics has to do with the meaning of these sentences—for example, as true or false in some particular model under some interpretation.
The fundamental theorem of first-order logic is the Completeness Theorem, which relates these two completely different ways of looking at languages:
Completeness Theorem: If $T$ is a first-order theory, then $T$ has a model iff $T$ is consistent.
Here, "$T$ has a model" is a statement of semantics, since it has to do with the truth or falsity of the members of $T$ in some model.
In contrast, "$T$ is consistent" is a syntactic statement, since it means merely that there is no proof of a contradiction using, as axioms, sentences of $T$ and the standard axioms of first-order logic. (A "proof" here is as defined in the first paragraph; a proof is a finite sequence of strings, with each string either an axiom or derivable from earlier strings by rules of inference—this is entirely syntactical, as it is a mere question of formal string manipulation.)
A: Mitchell Spector explained the basic ideas and the completeness (+soundness) theorem. But let me give you some more in-depth explanation of the model-theoretic perspective.
In model theory, usually${}^\dagger$, we only really care about semantics. I believe that for most model theorists, the true meaning of the completeness theorem is that we can use the familiar rules of inference to derive semantically true statements from other semantically true statements. This is (as far as I know) in contrast to non-first order logics, where we may have no (complete) rules of inference.
Consider the formulas $\varphi_1(x)= 0\leq x$ and $\varphi_2(x)=\exists y (y\cdot y=x)$ in the language of ordered rings $\{0,1,\leq,+,\cdot\}$. Syntactically, they are very different: the first one is quantifier-free, while the second one is not. The first one uses the symbol $\leq$, while the other one doesn't. However, if we consider them in the field of real numbers (or any real closed field), then they are equivalent: any real number satisfies $\varphi_1$ (in the real numbers) if and only if it satisfies $\varphi_2$.
More generally, if $T$ is any first-order theory in a language $L$, while $\varphi_1(x)$ and $\varphi_2(x)$ are arbitrary $L$-formulas with the same free variables, then we say that $\varphi_1$ is equivalent to $\varphi_2$ under $T$ if $T\vdash \varphi_1\leftrightarrow \varphi_2$, that is, $T$ proves that $\varphi_1$ and $\varphi_2$ are equivalent.
Essentially by completeness, this is exactly equivalent to saying that in any model of $T$, the interpretations of $\varphi_1$ and $\varphi_2$ (i.e. the sets of elements satisfying them) are exactly the same. It follows that equivalence under $T$ is an equivalence relation on the set of all $L$-formulas in variable $x$ (or any other prescribed set of free variables), and that (in models of $T$), all the semantic content of a formula is expressed by its equivalence class. For example, if we are in a real closed field, then $\varphi_1(x)$ and $\varphi_2(x)$ express the same thing, so if we only care about the meaning of the formulas, there is no need to distinguish between them. This idea gives rise to the notion of the Lindenbaum-Tarski algebra, i.e. the Boolean algebra of all equivalence classes of formulas with prescribed free variables.
In fact, we can (and do) go one step further. One can show that if we have any model $M$ of a complete theory $T$, then we can find a larger $L$-structure $N$ (a so-called elementary extension, which means, intuitively, that $M\subseteq N$ and anything we can say about an element of $M$ is true in $N$ if and only if it is true in $M$) which has the property that two elements of $N$ satisfy the same $L$-formulas if and only if there is an automorphism of $N$ which takes one of them to the other (we say that $N$ is strongly homogeneous). This reduces the problem of checking which formulas a given element satisfies to the problem of checking which orbit of $\operatorname{Aut}(N)$ it belongs to.
Moreover, if we pick $N$ to be sufficiently rich (whence it is called a monster model), virtually all interesting properties of $T$ are captured by $N$, its automorphism group, and the various Lindenbaum-Tarski algebras, or rather, their interpretations in $N$ (which we call definable sets).

$\dagger$ sometimes we do care about syntax because it tells us something about semantics, or makes it easier to understand them. For example, the theory of the real field in the language of ordered rings has quantifier elimination. This is a syntactic property, but it implies that the theory of real closed fields (in any equivalent language, for example the language of rings) is model complete, which is an important semantic property.
