For the sake of comparison, the entirety of first-order logic can be summarized as follows:
The well formed formulas of first order logic are those generate by the grammar:
$$\begin{align} &\langle formula\rangle&\to&\qquad\neg\langle formula\rangle\\ &&&\qquad\mid(\langle formula\rangle\langle connective\rangle\langle formula\rangle)\\ &&&\qquad\mid\langle quantifier\rangle\langle variable\rangle(\langle formula\rangle)\\ &&&\qquad\mid\langle relation\rangle\langle args\rangle\\ &\langle relation\rangle&\to&\qquad\langle relation\rangle_\text{I}\mid R\\ &\langle args\rangle&\to&\qquad ^\text{I}\langle args\rangle\langle term\rangle\mid\varepsilon\\ &\langle term\rangle&\to&\qquad\langle variable\rangle\mid\langle function\rangle\langle args\rangle\\ &\langle function\rangle&\to&\qquad\langle function\rangle_\text{I}\mid F\\ &\langle variable\rangle&\to&\qquad\langle variable\rangle_\text{I}\mid v\\ &\langle quantifier\rangle&\to&\qquad\exists\mid\forall\mid\Finv \end{align}$$
The axiom schemas are:
$$\begin{align} \text{LT}1 & \quad(\phi\implies(\psi\implies\phi))\\ \text{LT}2 & \quad ((\phi\implies(\psi\implies\xi)))\implies((\phi\implies\psi)\implies(\phi\implies\xi)))\\ \text{LT}3 & \quad ((\neg\phi\implies\neg\psi)\implies(\psi\implies\phi))\\ \text{GH}1 & \quad (\forall v\phi\implies\phi(v\mapsto\tau))\\ \text{GH}2 & \quad (\Finv v\phi\implies(\forall v(\phi\implies\psi)\implies(\phi\implies\forall v\psi)))\\ \text{Ex}1,2 & \quad (\exists v\phi\iff\neg\forall v\neg\phi)\qquad(\text{combined}) \end{align}$$
Where $\phi,\psi,\xi$ are wffs, and $\tau$ is a term.
The inference rules are:
$$\begin{align} \text{MP} & \quad \phi\implies\psi,\phi\vdash\psi\\ \text{UGen} & \quad \phi\vdash\forall v \phi\\ \text{EGen} & \quad \phi\vdash\exists v\phi(\tau\mapsto v) \end{align}$$
Question: What is second order logic?
I am being vague because I actually have no idea what rules are needed to ensure that second order logic stays logical. For instance, do bound functions and relations have specific arities? If so, what production rules do I need in order to account for the added context-sensitivity? Does existential generalization for relations and functions extend to arbitrary formulas (e.g. $\forall x\exists y((P(x)\lor P^2(x,y))\implies P^3(y,x,y))\vdash\exists P^1\forall xP^1(x),\exists P^2\forall x\exists y P^2(x,y),$ etc.)? Is $\forall P\neg P$ consistent? What are the rules?
I'm hoping for a user's manual and syntax guide a la Principia Mathematica, or, barring that, a list of the 12 additional production rules, axioms, and or inference rules that I need in order to extend first order logic to second order logic.
Note: