I am having a hard time in trying to find a formal and explicit definition for the syntax of the second-order logic. I understand there may be small differences in one formalization w.r.t. another (just like, in the formalization of a first-order language, the set of connectives is often different - just because you can build the missing ones from the others), but there are some gaps that I am unable to fill in myself.
In particular, I was wondering what should be considered the set of second-order terms and I would like to be pointed to some reference book which states this (sufficiently) explicitly.
Let me elaborate a bit more on what I found:
in van Dalen's "Logic and Structure" (5 ed, ch. 5) the author first introduces the symbols of a second-order alphabet, and then defines the set of second-order formulas. However, there's no equality among the symbols, and it's not explicitly mentioned what are the terms he uses for building the formulas. If terms were just the first-order terms they would require a symbol which is not in the alphabet.
in Libkin's "Elements of finite model theory" (https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf, ch. 7), a second-order language is explicitly described as an extension of a FO language. He describes what are first-order terms and then...he just forgets to say what the SO terms are, and few lines below just says that $t$ and $t'$ are "terms", without mentioning their order. Should I assume SO terms are exactly FO terms? I feel this would somehow be against the next reference I am mentioning.
in Enderton's "A mathematical introduction to logic" (ch. 4) the author introduces two sorts of second order variables (one for predicate variables and one for function variables). It seems that the SO terms should be the FO terms plus the ones obtained by applying a function variable to the FO terms). This is a bit confusing though, as in other books I didn't find the possibility to quantify explicitly on two different sorts of second-order variables. I know you can always consider a function as a set (with certain properties), but formally this changes the set of what we should call "second-order terms".
I guess this may not be extremely relevant for the development of the theory, but honestly I feel that this is not a good reason for not having a formal definition to start with. I took a look a several other books I'm not mentioning here (for brevity), so please point to some reference only if you are certain that it solves my doubts.