Return to Answer

The answer to your main question is that in ZFC there is always such a proper-class elementary-extension.

Theorem. In ZFC, every set-sized model in a set-sized first-order language has a proper-class elementary extension.

Proof. This is easiest to see in the case that the global axiom of choice holds, in other words if there is a class well-ordering of the universe. So let me first explain that case. Fix the global well-order and consider any fixed model $M_0$ in a set-sized first-order language. Using the upward Löwenheim-Skolem theorem, there is a proper elementary end-extension of $M_0$, and we may let $M_1$ be the least such model arising in the well-order. Continuing transfinitely, picking the least elementary-extension at each stage and unions at limit stages, we may build up an elementary chain $$M_0\prec M_1\prec\cdots\prec M_\alpha\prec\cdots$$ by a definable procedure whose union will be a proper-class elementary extension of each of them and in particular of $M_0$, as desired.

But my next observation is that in ZFC you don't actually need global choice. If we fix $M_0$, then by the axiom of choice, we may code $M_0$ by a set of ordinals $A$. Consider the inner model $L[A]$, which satisfies ZFC and global choice. Since $A$ codes $M_0$, we may undertake the argument of the previous paragraph inside $L[A]$ to get a proper-class elementary extension of $M_0$. In the original universe $V$, then, we get an $A$-definable proper class elementary-extension of $M_0$, as desired. QED

Your second question, however, can fail in some models. I claim that it is possible to have a definable proper-class-sized theory $T$ in a model of ZFC, such that every subset of $T$ has a model, and so in particular the theory is consistent, but there is no definable (allowing parameters) model of all of $T$. For example, assume we are working in a model of ZFC in which there is no definable linear order. (I explained how to construct such a model in my answer to Asaf Karagila's question, Does ZFC prove the universe is linearly orderable?.) Let $T$ be the theory of a linear order $<$, with a constant symbol $\hat a$ for every object $a$. Every restriction of $T$ to only set-many constants will have a model, since in ZFC every set is linearly orderable, but in this model there is no definable model of all of $T$, since there is no definable linear ordering of the universe.

The answer to your main question is that in ZFC there is always such a proper-class elementary-extension.

Theorem. In ZFC, every set-sized model in a set-sized first-order language has a proper-class elementary extension.

Proof. This is easiest to see in the case that the global axiom of choice holds, in other words if there is a class well-ordering of the universe. So let me first explain that case. Fix the global well-order and consider any fixed model $M_0$ in a set-sized first-order language. Using the upward Löwenheim-Skolem theorem, there is a proper elementary end-extension of $M_0$, and we may let $M_1$ be the least such model arising in the well-order. Continuing transfinitely, picking the least elementary-extension at each stage and unions at limit stages, we may build up an elementary chain $$M_0\prec M_1\prec\cdots\prec M_\alpha\prec\cdots$$ by a definable procedure whose union will be a proper-class elementary extension of each of them and in particular of $M_0$, as desired.

But my next observation is that in ZFC you don't actually need global choice. If we fix $M_0$, then by the axiom of choice, we may code $M_0$ by a set of ordinals $A$. Consider the inner model $L[A]$, which satisfies ZFC and global choice. Since $A$ codes $M_0$, we may undertake the argument of the previous paragraph inside $L[A]$ to get a proper-class elementary extension of $M_0$. In the original universe $V$, then, we get an $A$-definable proper class elementary-extension of $M_0$, as desired. QED

Your second question, however, can fail in some models. I claim that it is possible to have a definable proper-class-sized theory $T$ in a model of ZFC, such that every subset of $T$ has a model, and so in particular the theory is consistent, but there is no definable (allowing parameters) model of all of $T$. For example, assume we are working in a model of ZFC in which there is no definable linear order. (I explained how to construct such a model in my answer to Asaf Karagila's question, Does ZFC prove the universe is linearly orderable?.) Let $T$ be the theory of a linear order $<$, with a constant symbol $\hat a$ for every object $a$. Every restriction of $T$ to only set-many constants will have a model, since in ZFC every set is linearly orderable, but in this model there is no definable model of all of $T$, since there is no definable linear ordering of the universe.

The answer to your main question is that there is always such a proper-class extension.

Theorem. In ZFC, every set-sized model in a set-sized first-order language has a proper-class elementary extension.

Proof. This is easiest to see in the case that the global axiom of choice holds, in other words if there is a class well-ordering of the universe. So let me first explain that case. Fix the global well-order and consider any fixed model $M_0$ in a set-sized first-order language. Using the upward Löwenheim-Skolem theorem, there is a proper elementary end-extension of $M_0$, and we may let $M_1$ be the least such model arising in the well-order. Continuing transfinitely, picking the least elementary-extension at each stage and unions at limit stages, we may build up an elementary chain $$M_0\prec M_1\prec\cdots\prec M_\alpha\prec\cdots$$ by a definable procedure whose union will be a proper-class elementary extension of each of them and in particular of $M_0$, as desired.

But my next observation is that in ZFC you don't actually need global choice. If we fix $M_0$, then by the axiom of choice, we may code $M_0$ by a set of ordinals $A$. Consider the inner model $L[A]$, which satisfies ZFC and global choice. Since $A$ codes $M_0$, we may undertake the argument of the previous paragraph inside $L[A]$ to get a proper-class elementary extension of $M_0$. In the original universe $V$, then, we get an $A$-definable proper class elementary-extension of $M_0$, as desired. QED

Your second question, however, can fail in some models. I claim that it is possible to have a definable proper-class-sized theory $T$ in a model of ZFC, such that every subset of $T$ has a model, and so in particular the theory is consistent, but there is no definable (allowing parameters) model of all of $T$. For example, assume we are working in a model of ZFC in which there is no definable linear order. (I explained how to construct such a model in my answer to Asaf Karagila's question, Does ZFC prove the universe is linearly orderable?.) Let $T$ be the theory of a linear order $<$, with a constant symbol $\hat a$ for every object $a$. Every restriction of $T$ to only set-many constants will have a model, since in ZFC every set is linearly orderable, but in this model there is no definable model of all of $T$, since there is no definable linear ordering of the universe.

The answer to your main question is that in ZFC there is always such a proper-class elementary-extension.

Theorem. In ZFC, every set-sized model in a set-sized first-order language has a proper-class elementary extension.

Proof. This is easiest to see in the case that the global axiom of choice holds, in other words if there is a class well-ordering of the universe. So let me first explain that case. Fix the global well-order and consider any fixed model $M_0$ in a set-sized first-order language. Using the upward Löwenheim-Skolem theorem, there is a proper elementary end-extension of $M_0$, and we may let $M_1$ be the least such model arising in the well-order. Continuing transfinitely, picking the least elementary-extension at each stage and unions at limit stages, we may build up an elementary chain $$M_0\prec M_1\prec\cdots\prec M_\alpha\prec\cdots$$ by a definable procedure whose union will be a proper-class elementary extension of each of them and in particular of $M_0$, as desired.

But my next observation is that in ZFC you don't actually need global choice. If we fix $M_0$, then by the axiom of choice, we may code $M_0$ by a set of ordinals $A$. Consider the inner model $L[A]$, which satisfies ZFC and global choice. Since $A$ codes $M_0$, we may undertake the argument of the previous paragraph inside $L[A]$ to get a proper-class elementary extension of $M_0$. In the original universe $V$, then, we get an $A$-definable proper class elementary-extension of $M_0$, as desired. QED

Your second question, however, can fail in some models. I claim that it is possible to have a definable proper-class-sized theory $T$ in a model of ZFC, such that every subset of $T$ has a model, and so in particular the theory is consistent, but there is no definable (allowing parameters) model of all of $T$. For example, assume we are working in a model of ZFC in which there is no definable linear order. (I explained how to construct such a model in my answer to Asaf Karagila's question, Does ZFC prove the universe is linearly orderable?.) Let $T$ be the theory of a linear order $<$, with a constant symbol $\hat a$ for every object $a$. Every restriction of $T$ to only set-many constants will have a model, since in ZFC every set is linearly orderable, but in this model there is no definable model of all of $T$, since there is no definable linear ordering of the universe.

Here are a few interesting boundary cases.

If the global axiom of choice holds, in other words if there is a class well-ordering of the universe, then any consistent set-sized theory in a first-order language with infinite models has a proper-class sized model. One simply takes the first model $M_0$ of it with respect to the well-ordering, and then the first proper elementary extension of that model, using the upward Löwenheim-Skolem theorem, building up an elementary chain $$M_0\prec M_1\prec\cdots\prec M_\alpha\prec\cdots$$ whose union will be an elementary extension of each of them and hence a proper-class model of the theory.

In particular, since we can force to add a global well-ordering of the universe without adding any sets, this means that in any countable model of ZFC, there is a model of GBC with the same sets, such that every consistent set-sized theory has a proper-class sized model.

Meanwhile, it is possible to have a definable proper-class-sized theory $T$ in a model of ZFC, such that every subset of $T$ has a model, and so in particular the theory is consistent, but there is no definable (allowing parameters) model of all of $T$. For example, assume we are working in a model of ZFC in which there is no definable linear order. (I explained how to construct such a model in my answer to Asaf Karagila's question, Does ZFC prove the universe is linearly orderable?.) Let $T$ be the theory of a linear order $<$, with a constant symbol $\hat a$ for every object $a$. Every restriction of $T$ to only set-many constants will have a model, since in ZFC every set is linearly orderable, but in this model there is no definable model of all of  $T$, since there is no definable linear ordering of the universe.

The answer to your main question is that there is always such a proper-class extension.

Theorem. In ZFC, every set-sized model in a set-sized first-order language has a proper-class elementary extension.

Proof. This is easiest to see in the case that the global axiom of choice holds, in other words if there is a class well-ordering of the universe. So let me first explain that case. Fix the global well-order and consider any fixed model $M_0$ in a set-sized first-order language. Using the upward Löwenheim-Skolem theorem, there is a proper elementary end-extension of $M_0$, and we may let $M_1$ be the least such model arising in the well-order. Continuing transfinitely, picking the least elementary-extension at each stage and unions at limit stages, we may build up an elementary chain $$M_0\prec M_1\prec\cdots\prec M_\alpha\prec\cdots$$ by a definable procedure whose union will be a proper-class elementary extension of each of them and in particular of $M_0$, as desired.

But my next observation is that in ZFC you don't actually need global choice. If we fix $M_0$, then by the axiom of choice, we may code $M_0$ by a set of ordinals $A$. Consider the inner model $L[A]$, which satisfies ZFC and global choice. Since $A$ codes $M_0$, we may undertake the argument of the previous paragraph inside $L[A]$ to get a proper-class elementary extension of $M_0$. In the original universe $V$, then, we get an $A$-definable proper  class elementary-extension of $M_0$, as desired. QED

Your second question, however, can fail in some models. I claim that it is possible to have a definable proper-class-sized theory $T$ in a model of ZFC, such that every subset of $T$ has a model, and so in particular the theory is consistent, but there is no definable (allowing parameters) model of all of $T$. For example, assume we are working in a model of ZFC in which there is no definable linear order. (I explained how to construct such a model in my answer to Asaf Karagila's question, Does ZFC prove the universe is linearly orderable?.) Let $T$ be the theory of a linear order $<$, with a constant symbol $\hat a$ for every object $a$. Every restriction of $T$ to only set-many constants will have a model, since in ZFC every set is linearly orderable, but in this model there is no definable model of all of  $T$, since there is no definable linear ordering of the universe.