Let $L_3$ be the third-order language of set theory with identity on the first sort. Variables $x$ are first-order, $y$ are second-order, and $z$ are third-order. In the style of Lévy and Bernays, we can extend the third-order theory $\mathrm{ZFC3}$ by reflection axioms of the form $\phi \rightarrow \exists x [\mathrm{Trans}(x) \wedge \mathrm{Rel}(\phi,x)]$ for each $L_3$ formula $\phi$ without free third-order variables, where $\mathrm{Trans}(x)$ says that $x$ is transitive and $\mathrm{Rel}(\phi,x)$ is the relativization of $\phi$ to $x$. Tharp's methods show both that the resulting theory $\mathrm{BL3}$ is consistent as long as first-order $\mathrm{ZF}$ is for each $n$ consistent with the existence of a $\Pi^2_n$-indescribable cardinal, and moreover that $\mathrm{BL3}$ proves that the $\Pi^2_n$-indescribable cardinals are stationary.

Does the latter fact have any

significant applicationsthat aren't already covered by weaker large-cardinal hypotheses, e.g. the unboundedness of the weakly compact cardinals?

We know that $\mathrm{BL3}$ becomes inconsistent if we drop the restriction that reflected formulas $\phi$ lack free third-order variables. On the other hand, work of Peter Koellner implies that $\mathrm{BL3}$ remains consistent relative to $\kappa(\omega)$ if we add reflection axioms in which $\phi$ has the form $\forall y_1 \exists u_1 \dots \forall y_k \exists u_k \psi$ where $\psi$ is a positive $L_3$ formula without higher-order quantifiers and each $u_i$ is an $L_3$ variable. Here an $L_3$ formula is said to be *positive* iff it is built using $\vee$, $\wedge$, $\exists$, and $\forall$ from atoms of the forms $x_n = x_k$, $x_n \neq x_k$, $x_n \in x_k$, $x_n \notin x_k$, $x \in y$, $x \notin y$, and $y \in z$.

Does the resulting theory $\mathrm{BL3}\prime$ prove anything significant not already proved by $\mathrm{BL3}$ or by $\mathrm{ZF}$ with unboundedly many weakly compacts?

Now get $\mathrm{BL3}^\ast$ from $\mathrm{BL3}\prime$ by adding reflection axioms in which $\phi$ can be any positive $L_3$ formula. It is not hard to show that $\mathrm{BL3}^\ast$ is consistent relative to a $2$-strong cardinal. But is there any reason to care about this theory?

Does $\mathrm{BL3}^\ast$ prove anything significant not already proved by $\mathrm{BL3}\prime$, by $\mathrm{BL3}$, or by $\mathrm{ZF}$ with unboundedly many weakly compacts?

Using a result of Rupert McCallum, I could continue asking such questions about extensions of the higher-order analogs of $\mathrm{BL3}$. But I fear I've bored you already.