Weaker forms of Vopěnka's principle (using Indiscernables and other forms of Elementarity): How weak are they?

Question

Vopěnka's principle is commonly used (or at least it was for me) as an intuitionistic approach to large cardinal axioms; that is, there is much intuition to it. This intuition is that for any proper class, there are two distinct elements which are very similar to each other.

At this point, I did not yet understand elementarity and had not yet studied any model theory other than was required for elementary set theory. Whilst learning model theory, I had conjectured what Vopěnka's principle was (before learning its true meaning) about indiscernability.

I had then finally gotten to the point where I understood Vopěnka's principle, but I had already conjectured the following principles (quite a long time ago actually, just found these in my notebook before writing this):

1. For any proper class $W$, there are $X\neq Y$ in $W$ such that for any first-order formula $\varphi$, $\varphi(X)$ iff $\varphi(Y)$.

This was the first iteration, which was before I had learned anything more than first-order induction on formulas. Of course, this is not provable from NBG. In any pointwise definable models of NBG, there are no indiscernables. In any of these, $ORD$ is an example of a proper class for which this does not hold. So, is it consistent?

2. For any proper class $W$ and signature $\sigma$, there are $X\neq Y$ (sets) which are subclasses of $W$ such that $\langle X,\sigma\rangle\prec\langle Y,\sigma\rangle$.

This one I'm not sure about at all. It doesn't really seem to imply anything strange or contradictory or even imply the existence of any large cardinals.

There are other ones which I have since shown inconsistent. These two, however, I have not.

Answer 1

Statement 1 is very nice, it says that in any proper class, there are two distinct objects $X$ and $Y$ that are indiscernible with respect to assertions in the ambiant theory (I assume the language of set theory); they exhibit exactly the same pattern of truths: $\varphi(X)$ if and only if $\varphi(Y)$ for every assertion $\varphi$.

This assertion is not directly expressible in ZFC or GBC, even as a scheme, since you are making explicit reference to the truth of an arbitrary formula $\varphi$. So you need a truth predicate to express the axiom.

But if you do have a truth predicate for first-order truth, then I claim statement 1 is provable. That is, it is both expressible and provable in the theory GBC + $T$ is a first-order truth predicate.

To see this, suppose that $W$ is a proper class or even any class of size more than continuum. Since there are only continuum many different 1-types in the language of set theory, it follows that there must be at least two distinct elements $X$ and $Y$ in $W$ with the same 1-type, that is, with the same pattern of truths for all the various formulas $\varphi$. In other words, $\varphi(X)$ if and only if $\varphi(Y)$ for these two objects.

Unless I have misunderstood, statement 2 seems to be provable in ZFC. If $W$ is a proper class structure with signature $\sigma$. Let $Y$ be any substructure of $W$ of size larger than $|\sigma|$, and by Löwenheim-Skolem, let $X$ be any elementary substructure of $Y$ of size $|\sigma|$. So $(X,\sigma)\prec (Y,\sigma)$, as desired.