Can Vopenka's principle be violated definably? One form of Vopenka's principle (a large cardinal axiom) states that no locally presentable category contains a full subcategory which is large (= a proper class) and discrete (= contains no nonidentity morphisms).  In terms of this definition, my question is:

Can one define a particular locally presentable category C and write down an explicit formula $\phi(x)$ in the first-order language of set theory such that if Vopenka's principle fails, then $\{ x | \phi(x) \}$ is a large discrete full subcategory of C?

But feel free to use any equivalent statement of Vopenka's principle and answer a suitably equivalent version of the question.
 A: Update. My new article grows out of and extends my 2010 answer to this question. The new part is the conservativity result, showing that the Vopěnka principle has the same first-order consequences as the strictly weaker Vopěnka scheme.


*

*Joel David Hamkins, The Vopěnka principle is inequivalent to but conservative over the Vopěnka scheme, manuscript under review. (arxiv)


Abstract. The Vopěnka principle, which asserts that every proper class of first-order structures in a common language admits an elementary embedding between two of its members, is not equivalent over GBC to the first-order Vopěnka scheme, which makes the Vopěnka assertion only for the first-order definable classes of structures. Nevertheless, the two Vopěnka axioms are equiconsistent and they have exactly the same first-order consequences in the language of set theory. Specifically, GBC plus the Vopěnka principle is conservative over ZFC plus the Vopěnka scheme for first-order assertions in the language of set theory.
The Vopěnka principle is the assertion that for every proper class $\mathcal{M}$ of first-order $\mathcal{L}$-structures, for a set-sized language $\mathcal{L}$, there are distinct members of the class $M,N\in\mathcal{M}$ with an elementary embedding $j:M\to N$ between them. In quantifying over classes, this principle is a single assertion in the language of second-order set theory, and it makes sense to consider the Vopěnka principle in the context of a second-order set theory, such as Godel-Bernays set theory GBC, whose language allows one to quantify over classes. In this article, GBC includes the global axiom of choice.
In contrast, the first-order Vopěnka scheme makes the Vopěnka assertion only for the first-order definable classes $\mathcal{M}$ (allowing parameters). This theory can be expressed as a scheme of first-order statements, one for each possible definition of a class, and it makes sense to consider the Vopěnka scheme in Zermelo-Frankael ZFC set theory with the axiom of choice.
Because the Vopěnka principle is a second-order assertion, it does not make sense to refer to it in the context of ZFC set theory, whose first-order language does not allow quantification over classes; one typically retreats to the Vopěnka scheme in that context. The theme of my article is to investigate the precise meta-mathematical interactions between these two treatments of Vopěnka's idea.
Main Theorems.


*
    
*If ZFC and the Vopěnka scheme holds, then there is a class forcing extension, adding classes but no sets, in which GBC and the Vopěnka scheme holds, but the Vopěnka principle fails.
    
*If ZFC and the Vopěnka scheme holds, then there is a class forcing extension, adding classes but no sets, in which GBC and the Vopěnka principle holds.


It follows that the Vopěnka principle VP and the Vopěnka scheme VS are not equivalent, but they are equiconsistent and indeed, they have the same first-order consequences.
Statement 1 is proved by class forcing to add a club class $C$ avoiding the regular cardinals. This destroys the assertion "Ord is Mahlo" and therefore destroys the Vopěnka principle, while preserving the Vopěnka scheme because it does not add sets. 
Statement 2 is proved by class forcing of the global axiom of choice. The difficult part is to show that the Vopěnka principle holds true with respect the new classes definable from the generic filter. The proof involves the concept of a stretchable set $g\subset\kappa$ for an $A$-extendible cardinal, one which has the property that for every cardinal $\lambda<\kappa$ and every extension $h\subset\lambda$ with $h\cap\kappa=g$, there is an elementary embedding $j:\langle V_\lambda,\in,A\cap V_\lambda\rangle\to\langle V_\theta,\in,A\cap V_\theta\rangle$ such that $j(g)\cap\lambda=h$. Thus, the set $g$ can be stretched by an $A$-extendibility embedding so as to agree with any given $h$. This stretchability property is the $A$-extendibility analogue of the master condition technique in other large cardinal contexts. 
Corollaries.


*
    
*Over GBC, the Vopěnka principle and the Vopěnka scheme, if consistent, are not equivalent.
    
*Nevertheless, the two Vopěnka axioms are equiconsistent over GBC.
    
*Indeed, the two Vopěnka axioms have exactly the same first-order consequences in the language of set theory. Specifically, GBC plus the Vopěnka principle is conservative over ZFC plus the Vopěnka scheme for assertions in the first-order language of set theory. $$\text{GBC}+\text{VP}\vdash\phi\qquad\text{if and only if}\qquad\text{ZFC}+\text{VS}\vdash\phi$$


See the edit history for my 2010 answer.
