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 applications* that 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.



Applications of higher-order reflection principles
I view these kinds of hypotheses as on a continuum stretching from
weak compactness up through all the levels of the indescribability
hierarchy, second order, third order and so on. This hierarchy of
indescribability continues transfinitely via the strongly
unfoldable cardinals, which can be thought of simply as the
transfinite-order indescribable cardinals.


The basic phenomenon here is that as you rise in this hierarchy, you can prove the consistency of
stronger and stronger fragments of the proper forcing axiom. The
situation is that, although one seems to need a supercompact
cardinal to get the consistency of the full proper forcing axiom,
nevertheless weaker versions of PFA can be shown consistent from
these much weaker large cardinals in the vicinity of your
hypotheses.


For example, in my article [J. D. Hamkins, T. Johnstone, The proper and
semi-proper forcing axioms for forcing notions that preserve $\aleph\_2$ or $\aleph\_3$](http://jdh.hamkins.org/pfa-aleph_2-preserving/),
we prove the following:


**Theorem.** The following are equiconsistent over ZFC:


1. There is an unfoldable cardinal.
2. PFA($\aleph\_2$-preserving) + PFA($\aleph\_3$-preserving) + $\text{PFA}\_{\aleph\_2}$ + $2^\omega=\aleph\_2$.
3. $\text{PFA}\_{\frak{c}}$.


A more local version of this result is:


**Theorem.** If $\kappa$ is $(\theta+1)$-strongly unfoldable, with
$\kappa\leq\theta$, and $0^\sharp$ does not exist, then the PFA
lottery preparation of $\kappa$ forces the principles
PFA($\aleph\_2$-preserving$\cap V\_\theta$),
PFA($\aleph\_3$-preserving$\cap V\_\theta$) and $PFA\_{\frak{c}}(V\_\theta)$.


This is very close to your third-order situation, if you take
$\theta=\kappa+1$ or $\theta=\kappa+2$; the cases of $\theta=\kappa+n$ are essentially the finite order indescribibility hypotheses. The point is that as you
rise to higher orders here, you can get the consistency of greater
fragments of the PFA axiom, applying it to larger partial orders.


Since $\kappa$ is totally indescribable if and only if it is
$(\kappa+m)$-strongly unfoldable for every ﬁnite $m$, we similarly
obtained the following:


**Corollary.** If $\kappa$ is totally indescribable and $0^\sharp$
does not exist, then the PFA lottery preparation of $\kappa$
forces PFA(size$\lt\beth\_\omega$ +$\aleph\_2$-preserving) and
PFA(size$\lt\beth\_\omega$ + $\aleph\_3$-preserving).


In addition, Neeman and Neeman and Schimmerling established the
following theorem:


**Theorem.**(Neeman, Neeman+Schimmerling)


1. PFA(c-linked) is equiconsistent over ZFC with the
existence of a $\Sigma^2\_1$-indescribable cardinal.
2. If the existence of a $\Sigma^2\_1$-indescribable cardinal is consistent with
ZFC, then so is PFA($\mathfrak{c}^+$-c.c.).


Our paper has further references and similar results.


