Can the axiom of choice or its weaker versions be (dis)proved using reflection principles? In On the Question of Absolute Undecidability, Peter Koellner investigates whether it is possible to prove or disprove $V = L$ using (EDIT: both first and second-order) reflection principles, ie. statements of the form*
$$V \vDash \varphi(A) \to \exists \alpha \ V_\alpha \vDash \varphi^\alpha(A^\alpha)$$
and shows that it cannot be done.
Starting from $ZF$, can these principles be used to prove or disprove the Axiom of choice or some of its weaker variants (eg. Dependent, Countable choice)?
* definition on page 13.
 A: The question seems to me asking if sufficiently large cardinals defined by indescribability properties will prove the axiom of choice or its weak variants hold below such cardinals. (Disproving is moot since these are consistent with $V=L$.)
The answer is negative, but more complicated. First of all, we can violate any sort of choice "on a small set", well below our large cardinal, and that will preserve the reflection properties. So the question now is if we can make the failure in some sense large. And indeed we can. With Yair Hayut we developed a basic method for lifting elementary embeddings to symmetric extensions and we showed that it's consistent relative to large cardinals that there is a critical point whose successor is singular.
It's not hard to check that this reflects down, and that indeed this critical point satisfies any reflection principle we wanted (it was previously a supercompact cardinal, after all).
We continue research in this direction, and I hope we will have new results to announce soon. 
