I've heard the terms first-order language, first-order logic, first-order theory, etc., and I'm trying to understand exactly what the definition of an nth-order language, logic, or theory is; and also, what the formal definition of a logic is.
Searching the internet, I've had very little success in finding such definitions, so I'm asking here, in hopes of receiving some clarifying information.
Follow up question: where do, for example, ZFC, and PA fit in all this?
(My motivation for asking: I'm trying to self-study foundations of mathematics, and several theorems, for example, the completeness theorem, or Lowenheim Skolem applies only to first-order theories, as I understand it; but I don't know what a first-order theory is)
In first-order logic you can quantify over individuals (that is, elements of the universe of a structure).
In second-order logic you can additionally quantify over predicates and functions that take individuals as arguments. For example you can write things like $\forall x \forall y \exists P : P(x) \land \neg P(y)$. The $\exists P$ is not allowed in first-order logic.
In third-order logic you can also quantify over meta-predicates (and meta-functions) that take ordinary predicates/functions as arguments.
And so forth.
Generally, higher-order logic allows you to take this to any depth, and you get an entire type theory to play with.
ZFC and PA are both first-order theories. (In ZFC, of course, you can quantify over sets, which looks a lot like quantifying over predicates -- but with the caveat that only some of the possible predicates correspond to sets).