Non-Henkin non-full semantics for second-order logic I'm interested in alternative semantics for second-order logic that still have a first-order flavor the way that Henkin semantics does.
Let's consider a version of second-order logic with a single first-order sort $D$ and some second-order sorts $D \to 2, D \times D \to 2, D^3 \to 2, \cdots$ and $D \to D, D \times D \to D, D^3 \to D \cdots$ .
I can think of four semantics for the syntax outlined above:

*

*weak semantics (haven't seen this in sources)

*Henkin semantics

*strictly definable semantics (haven't seen this in sources either)

*full semantics

I'm curious where I can read more about possible semantics that aren't 2 or 4.
We can consider a multi-sorted first-order theory given the above sorts.
If we let all the sorts be independent and impose no nonlogical axioms, we get weak semantics. If we restrict our attention to full models where $D \to 2$ looks like the true powerset of $D$, then we get the full semantics.
By starting with weak semantics and imposing the axiom schemas below we get choiceless Henkin semantics:
$$ \exists a : S \mathop. \forall \vec{x} \mathop. \varphi(\vec{p}, \vec{x}) \leftrightarrow x \in a \\ \text{promises us the existence of every definable relation} $$
$$ (\forall \vec{x} \exists! u \mathop. \varphi(\vec{p}, \vec{x}, u)) \to \exists a : S \mathop. \forall \vec{x} \mathop. \varphi(\vec{p}, \vec{x}, y) \leftrightarrow a(x) = y \\ \text{promises us the existence of every definable function} $$
By imposing an axiom schema similar to the axiom of choice we get Henkin semantics. This gives us the ability to convert $\forall x \exists X \mathop. \varphi$ to $\exists Y \forall x \mathop. \varphi'$ ... which is reminiscent of Skolemization.
However, we can also impose an alternative condition that is incompatible with choice, which cannot be expressed as an axiom schema:
For every function $f$ or relation $R$, there exists a formula-with-first-order-parameters $\varphi$ that is coextensive with it.
(I think that we need to restrict our attention to first-order parameters, or every function or relation could trivially serve as a witness for itself.)
Is there a place to read more about alternative Henkin-like semantics for second order logic?
 A: I've also found limited literature on this sort of topic. There definitely are serious results on fragments of second-order logic - cf. especially Shelah's classification of second-order quantifiers - but this doesn't really seem like it's what you're looking for, since the restrictions here are "structural" instead of "complexity-based." And even widening the net, so to speak, there are definitely many areas left to be explored (see e.g. here).
That said, I do have an overly-long (hence CW) comment to make around the subtleties of "definable quantification," which turns out to be a bit messier than one might expect (compare what follows with an early naive question of mine).

One thing we might reasonably want to do, given a "starting logic" $\mathcal{L}$, is form a new logic $\mathcal{L}^T$ (the "Tarski jump") which expands $\mathcal{L}$ by adding the ability to quantify over $\mathcal{L}$-definable sets. There is however a lot of flexibility around implementation here. Let me start with an obvious point:

Any reasonable extension $\hat{\mathcal{L}}$ of $\mathcal{L}$ which can quantify over parameter-freely-$\mathcal{L}$-definable sets is strictly stronger than $\mathcal{L}$.

(Wait, where do I get off droppping parameters? See below ...)
Proof: Let $\kappa=\vert\mathcal{L}[\{<\}]\vert$ be the number of $\mathcal{L}$-sentences in the language of order. Consider $\kappa^+$ as a linear order; then in the structure $\kappa^+$, the formula "the smallest non-parameter-freely-$\mathcal{L}$-definable element" is an $\hat{\mathcal{L}}$-definition not corresponding to any $\mathcal{L}$-definition. $\quad\Box$
(Note that this even applies to $\mathcal{L}=\mathsf{SOL}$, that is, second-order logic with full semantics! Sometimes an a priori bound on what a quantifier searches over can add strength.)
But there are indeed vicissitudes! Most obviously, note that naively-implemented quantification over definable sets is not "language-monotonic"! For example, "Every $\mathsf{FOL}$-definable set is eventually periodic" is true in $(\mathbb{N};+)$ but false in $(\mathbb{N};+,\times)$. Generally language-monotonicity is considered fundamental, so I think it's reasonable to try to get it back. The natural thing to do here is to somehow allow the new second-order quantification to take into account the intended language, so that even over $(\mathbb{N};+,\times)$ we can still talk about $\mathsf{FOL}$-definable sets in the sense of the restricted language with addition alone.
And at this point we start getting into rather messy waters, so I'm just going to jump to (what I currently think is) the end. Suppose I have a structure $\mathfrak{A}$, a logic $\mathcal{L}$, an $n$-ary relation $D$, a $2n$-ary equivalence relation $E$ on $D$, and a finite sequence of relations $$R_1(x_1,...,x_{k_1}; y^1_1,...,y^1_n, ..., y^{l_1}_1,...,y^{l_1}_n),..., R_c(x_1,...,x_{k_c};y^1_1,...,y^1_n, ..., y^{l_c}_1,...,y^{l_c}_n)$$ which are "locally $E$-invariant" in the sense that for each $1\le d\le c$ and each choice of $a_1,...,a_{k_c}\in\mathfrak{A}$ the induced relation on $D$ is $E$-invariant (here each relation comes equipped with a distinguished grouping of its inputs). Then I can define the new quantifier $${\bigtriangledown}^\mathcal{L,p}_{D,E,\overline{R}} X$$ to mean "For every $E$-invariant set $X\subseteq D^p$ whose $E$-quotient is $\mathcal{L}$-definable-without-parameters in the structure $\mathcal{X}$," where $$\mathcal{X}=(D/E; \{R_d(a_1,...,a_{k_d}; -): a_1,...,a_{k_d}\in\mathfrak{A}, 1\le d\le c\}).$$ Note that the language of this latter structure may be quite large: the relation $R_d$ gives rise not to a single primitive relation on $\mathcal{X}$, but rather a whole $\mathfrak{A}^{k_d}$-indexed family of them (this is how we can get definability with arbitrary parameters in this framework, even though a priori we're starting out with definability without parameters).
In my opinion, the right definition for $\mathcal{L}^T$ is the following:

Let $\mathcal{L}^T$ be the smallest logic $\mathcal{J}$ containing $\mathcal{L}$ and closed under the quantifier $$\bigtriangledown^{\mathcal{L},p}_{\delta, \eta,\overline{\rho}}$$ for all $p\in\mathbb{N}$ and all appropriate $\mathcal{J}$-formulas $\delta,\eta,\rho_1,...,\rho_c$.

This may appear to be massive overkill at first, but it guarantees that the result is a regular logic (namely: we have "good relativization") and more broadly ensures generally good behavior of the relevant notion of interpretations. And the above argument ensures that - at least for logics $\mathcal{L}$ with the finite use property - $\mathcal{L}^T$ is always strictly stronger than $\mathcal{L}$.
ANYwho, my contention at this point is that "definable second-order logic" should be $\mathsf{FOL}^T$. This might be a bit stronger than what you have in mind. (Incidentally, see this MO post re: a slightly-weaker construction iterated through the ordinals.)
