Definitions of first-order, second-order, nth-order languages, theories, and logics?

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).

• Can you explain how, e.g. the jump from first-order to second-order, and the jump from second-order to third-order are analogous? Also, what do meta-predicates or meta-functions look like? Aug 3, 2017 at 0:18
• Sorry, but I must ask: Is this your opinion or a widely accepted consensus? Opinions seem to vary as the OP seems to have discovered for him or herself. Aug 3, 2017 at 1:41
• @DanChristensen - This is the widely accepted meaning of what an $n$-th order logic is, yes. Aug 3, 2017 at 3:12
• @DylanPizzo: At each level you're allowed to quantify over predicates/functions that take as arguments anything you could quantify over on the previous level. Aug 3, 2017 at 12:11
• @hmakholm: Sometimes second-order logic is defined as quantify over sets of sets. Other times (as you do) as quantify over predicates. What is the right one? You said "In ZFC, you can quantify over sets, which looks a lot like quantifying over predicates". Why for some sets is equivalent quantify over them and over predicates? Jun 9, 2020 at 10:50