I would like to have something like a linear order on classes, such that every instantiated predicate of classes has a minimal instance in that order. For my purposes, it is fine to assume V=L for sets.

1$\begingroup$ I'm not quite clear as to what you mean. If you assume $V=L$ then you have a definable wellordering of the sets, therefore every nonempty class must have a least element. $\endgroup$– Asaf Karagila ♦Jan 7, 2015 at 19:32

4$\begingroup$ @AsafKaragila I want well ordering not in classes, but of classes. $\endgroup$– Colin McLartyJan 7, 2015 at 20:06
1 Answer
In the context of models of secondorder arithmetic, Mostowski showed that starting with the theory $Z_2$ (the secondorder arithmetic analogue of KelleyMorse) together with the scheme of dependent choices, one can use forcing to add a wellordering relation on classes so that the full secondorder comprehension scheme continues to hold in the language with the new relation. The argument appeared in his paper "Models of second order arithmetic with definable Skolem functions" [Fund. Math. 75 (1972), 223–234] and was later corrected in "Erratum to the paper `Models of second order arithmetic with definable Skolem functions'" [Fund. Math. 84 (1974), 173]. Initially, Mostowski used only the choice scheme to prove the result.
Mostowski's argument generalizes to the theory KelleyMorse together with the scheme of dependent choices. The scheme of dependent choices states that if a secondorder definable relation has no terminal nodes, then it has an $\omega$chain. The forcing is supposed to be akin to the forcing argument that a global wellordering class can be added to a model of ZFC, but in this case the condition are classes, and so we have a hyperclass forcing (in Sy Friedman's terminology). I only know about this construction from conversations with Ali Enayat, who will probably give many more details when he is around.

$\begingroup$ Terrific. I will take some time to absorb this. Since I really want this in a weak fragment of ZFC, the use of $Z_2$ is very encouraging. $\endgroup$ Jan 7, 2015 at 20:25

$\begingroup$ @ColinMcLarty I think the key to making the argument work is having full secondorder comprehension (which GB doesn't have) plus the dependent choice scheme for classes. This is, I think, what is needed for hyperclass forcing to preserve comprehension in the extended language. But I am hoping Ali will be here to say more. $\endgroup$ Jan 7, 2015 at 22:08

$\begingroup$ A beautiful result. I fear it sinks my strategy for the problem that led to this question, but maybe that failure points the way to what will work. $\endgroup$ Jan 9, 2015 at 20:26