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](https://arxiv.org/pdf/1610.02729.pdf) (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.



Can $\mathsf{Ord}$ be weakly compact from a second-order perspective?
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."](https://arxiv.org/abs/1407.6335)


