I am trying to understand the Henkin Semantics for Second Order logic and, and I’m confused on the following point.
The Comprehension Axioms are typically defined as follows: for every second order formula $\phi(\bar{x})$ with free variables in $\bar{x}$, we have the axiom: $$ \exists R \:\forall \bar{x} \: R(\bar{x}) \leftrightarrow \phi(\bar{x}) \tag{1}\label{3} $$
However in some treatments of the topic (for example Section 9 of https://plato.stanford.edu/entries/logic-higher-order/) it seems that $\phi$ is allowed to have free second order variables other than $R$. Say for example $\phi$ contains some predicate symbol $P$, and consider the associated comphrehension axiom $$ \exists R \: \forall \bar{x} \: R(\bar{x}) \leftrightarrow \phi(\bar{x}, P) $$
in particular lets just focus on this concrete case where $R,P$ are both unary and $\phi$ is a very simple sentence: \begin{gather} \exists R \: \forall x \: R(x) \leftrightarrow \lnot P(x) \tag{2}\label{1} \end{gather}
Is it correct that in such an axiom, $P$ is being implicitly universally quantified as a second order variable? In particular is the following a valid comprehension axiom for the Henkin Models: $$ \forall P \: \exists R \: \forall x \: R(x) \leftrightarrow \lnot P(x) \tag{3}\label{2} $$
I do not see any way to interpret \ref{1} other than \ref{2}, however I have sometimes seen the axioms presented in the form of \ref{1} rather than \ref{2}.
The reason I ask is that it also seems reasonable to define the Henkin semantics so that comprehension (i.e. \ref{3}) only holds for formulas $\phi(\bar{x})$ which contain no free second order variables. In this case there seems to be no reason that a Henkin model would have to satisfy a sentence like \ref{2}.
First of all, note that you are confusing 2 concepts, you have the semantics, and you have the deductive systems (axioms).
Semantics is how you define the meta relation "satisfy".
Deductive system defines what is a "legal" proof.
Your question is about the deductive system of second order logic. It is agnostic to the semantics you choose to use (Henkin/full).
In the site you linked, they define Henkin semantics at 9.1 (they call it Henkin models) while in chapter 3 they defined the standard semantics (which is also called full semantics, or full models).
Now for the question, I believe it should be the first case, there can be other free variables, the only restriction is that $R$ is not free