Can $\mathsf{Ord}$ be weakly compact from a second-order perspective?

Question

Working in $\mathsf{ZFC}$ + "There is a weakly compact cardinal" and letting $\kappa$ be the least weakly compact cardinal, say that a logic $\mathcal{L}$ is loraxian iff every $\mathcal{L}$-definable-over-$V_\kappa$ subtree of $2^{<\kappa}$ has an $\mathcal{L}$-definable-over-$V_\kappa$ branch. Enayat and Hamkins showed (among other things) in $\mathsf{ZFC}$ that first-order logic is not loraxian, but I don't see how to use their techniques to address other logics - the key point being that everything leading up to case $2$ of Theorem $2.6$ is highly $\mathsf{FOL}$-specific.

As is my wont, I'm specifically curious about the situation with respect to second-order logic:

Is second-order logic consistently loraxian?

All I've been able to see is the following two basic observations:

• In contrast with case $2$, case $1$ of E/H's Theorem $2.6$ is fairly coarse: roughly speaking, by considering a tree whose nodes code choice functions for the $V_\alpha$s with $\alpha<\kappa$, we have that $\mathcal{L}$ is loraxian only if there is some weakly compact $\kappa$ such that $V_\kappa$ has an $\mathcal{L}$-definable-over-$V_\kappa$ well-ordering.

• Meanwhile, there is a silly red herring here. My initial guess was that $\mathsf{SOL}$ would obviously be loraxian since we can define the nodes which belong to some path. However, since $\kappa$ is weakly compact in reality this is actually no power whatsoever. What posed a problem for $\mathsf{FOL}$ isn't an inability to detect when a node should extend to a path, but rather (very roughly) the issue of piecing together a single path in a consistent way - and I don't see that this goes away for $\mathsf{SOL}$.

More generally I'm interested in anything on loraxian logics, but $\mathsf{SOL}$ seems like a natural starting point.

Answer 1

If $\kappa$ is weakly compact and there is a wellorder of $V_{\kappa+1}$ definable over $V_{\kappa+1}$ without parameters, then second order logic is Loraxian for $V_\kappa$: the least branch through a definable tree is definable. In $L$ (or in fact any of the known canonical inner models), there is such a wellorder.

You didn't ask, but I think it is consistent for second order logic to fail to be Loraxian. After a preparatory forcing, one can add a Cohen subset $G$ of $\kappa$ without destroying its weak compactness. The forcing can be factored as adding a Suslin tree $T$ and then adding $G$ as a branch through $T$. I am not an expert here, but I think one can probably force over $V[G]$ to make $T$ definable over $V_{\kappa+1}$, arranging that $G$ remains undefinable and $\kappa$ remains weakly compact. Probably one can arrange that any subset of $V_\kappa$ definable over $V_{\kappa+1}^{V[G,H]}$ is in fact be definable over $V_{\kappa+1}^{V[T]}$ from $T$. This is an (admittedly sketchy) local version of the arguments from Cheng-Friedman-Hamkins's "Large cardinals need not be large in HOD."