I've been studying Vopenka's principle:
For any language $\mathcal{L}$ and a proper class $C$ of $\mathcal{L}$-structures, there exist distinct $M, N \in C$ and an elementary embedding $j: M \to N$.
A cardinal $\kappa$ is Vopenka if $V_\kappa$ satisfies Vopenka's principle.
Naturally arose in my head the problem of the existence of (an unbounded class of) Vopenka cardinals vs the actual truth of Vopenka's principle. By generalising this to arbitrary properties, my question is the following:
Let $\varphi$ be a formula in the language of MK set theory. Then, we define $\textrm{MK}_\varphi$ to be MK augmented by "$\varphi$ holds". Similarly, let's define $\textrm{MKL}_\varphi$ to be MK augmented by "there exists an unbounded class of cardinals $\kappa$ so that $(V_\kappa, V_{\kappa+1}, \in) \vDash \varphi$". Now, given some $\varphi$, which theory is proof-theoretically stronger: $\textrm{MK}_\varphi$ or $\textrm{MKL}_\varphi$?