There is another path that can be used to justify the existence of very large cardinals. Consider, for example, the abstract to Magidor's paper, "On the Role of Supercompact and Extendible Cardinals in Logic" (Israel Journal of Mathematics, Vol. 10, 1971, pp. 147-157) :
It is proved that the existence of supercompact cardinals is equivalent to a certain Lowenheim-Skolem Theorem for second order logic, whereas the existence of [an] extendible cardinal is equivalent to a certain compactness theorem for that logic. It is also proved that a certain axiom schema related to model theory implies the existence of many extendible cardinals.
Here the theorems:
Theorem 1. There exists a supercompact cardinal iff there is a $\mu_0$ such that for all $R({\beta})$, $\beta$$\ge$$\mu_o$there is an $\alpha$$\lt$$\beta$ such that $<$$R({\alpha})$, $\epsilon$$>$ can be elementarily embedded in $<$$R({\beta})$, $\epsilon$$>$. The least such $\mu_0$ is the first supercompact cardinal.
Theorem 2. The first supercompact cardinal is the first $\mu_0$ such that for every structure $A$ = $<$$M$, $R_1$,...,$R_n$ $>$ $|$$M$$|$$\ge$$\mu_0$ and every $\Pi^{1}_1$ sentence $\varphi$, such that $A$$\vDash$$\varphi$, there exists a substructure $A^{'}$ = $<$ $M^{'}$, $R_1$$|$$M$,..., $R_n$$|$$M$$>$ of $A$ with $|$$M^{'}$$|$$\lt$$|$$M$$|$ and $A^{'}$$\vDash$$\varphi$ [this is the "Lowenheim-Skolem Theorem" Magidor refers to in his abstract--my comment].
Definition. Logic is called $\kappa$-compact iff for every set of formulae $A$ in this logic, if every subset of $A$ of cardinality $\lt$$\kappa$ has a model, then $A$ has a model. The $\mathrm L^{n}_{\kappa}$ logic is like the $n$-th order logic, except that we allow conjunction and disjunction of less than $\kappa$ formulae. The usual second order logic is of course $L^{2}_{\omega}$.
Theorem 4. $\kappa$ is extendible iff $L^{2}_{\kappa}$ is $\kappa$-compact. $\kappa$ is the first extendible iff it is the first $\alpha$ such that second-order logic [$L^{2}_{\alpha}$--my comment] is $\alpha$-compact.
...We shall now show that a certain axiom schema is a very strong axiom of infinity, namely, it implies the existence of many supercompact cardinals. The axiom schema is:
($V$) If $\varphi$(x) defines a proper class of structures in the same language, then there exist two members of the class that one can be elementary embedded in the second...This axiom schema is called Vopenka's principle.
Let $V^{'}$ be the following axiom schema: ($V^{'}$) if the formula $\tau$(x) defines a closed unbounded set of ordinals, then there is an extendible cardinal in this class (i.e. "the class of all extendable cardinals is 'stationary' ").
Theorem 3. ($V$) implies ($V^{'}$) but is not equivalent to it.
Note that the forward implication '$\Rightarrow$' of Theorems 1, 2, and 4 show that if the required large cardinal exists, the logic in question will have the required property. This suggests to me the following 'formalist' justification of the existence of large cardinals:
If you want second-order logic to have certain model-theoretic properties, hypothesize the appropriate large cardinals.
This also suggests the following research program:
Discover what model-theoretic properties of n'th-order logic the existence of large cardinals imply (from $I0$ on down the large cardinal hierarchy), if any.
Similarly, one can hypothesize the existence of certain Lowenheim-Skolem-Tarski numbers, as V$\ddot a$$\ddot a$n$\ddot a$nen shows in his paper, "Sort Logic and Foundations of Mathematics" ("Sort Logic...is a many-sorted extension of second-order logic."):
The canonical hierarchy $\Delta_n$ ($n$$\lt$$\omega$) inside sort logic climbs up the large cardinal hierarchy by reference to Hanf-, Lowenheim-, and [Lowenheim-Skolem-Tarski]-numbers, reaching all the way up to Vopenka's Principle [pg. 185].
