Explicit example of countable transitive model of $\sf ZF$

Question

Do we know any explicit example of a countable transitive model for $\sf ZF$ or $\sf ZFC$?

Answer 1

No. And yes.

$\sf ZF$, and by extension $\sf ZFC$, cannot prove their own consistency. Therefore within the confines of $\sf ZF(C)$ we cannot even prove that there are models of $\sf ZF$ to begin with.

Not only that. The statement "$\sf ZF(C)$ is consistent" is absolute between the universe and transitive models, so if there is a transitive model, not only that $\sf ZF(C)$, but also models of $\sf ZF+\operatorname{Con}(ZF)$ and much stronger theories.

So even if we assume the consistency of $\sf ZF$, we cannot prove that there are transitive models.

However! Just like $\Bbb N$ cannot be proved to exist just in $\sf PA$, we might as well take stronger theories instead of just $\sf ZFC$. And once a theory $T$, extending $\sf ZF$, proves that there exists a transitive model, then we know that there is a least $\alpha$ such that $L_\alpha$ is a model of $\sf ZFC$, and that $\alpha$ is countable. As far as explicit go, this is pretty damn explicit.

Answer 2

Asaf has given a great answer - let me give another answer which shows a sense in which the answer is no.

Given a theory $T$ (in a finite language to avoid silliness), we can ask if it has a computable model - that is, if there is a $\mathcal{A}$ which

• is a model of $T$,

• has domain $\mathbb{N}$ (or a computable subset of $\mathbb{N}$), and

• all the relations and functions in the language are interpreted as computable relations and functions.

It turns out that ${\sf ZF}$ (indeed, much weaker than ${\sf ZF}$) has no computable models; see https://mathoverflow.net/questions/12426/is-there-a-computable-model-of-zfc.

The situation gets even worse for well-founded models: ${\sf ZF}$ has no hyperarithmetic well-founded models! "Hyperarithmetic" is a slightly technical definition, but basically anything you can define without using second-order logic is hyperarithmetic.

So I'd consider both these facts as good evidence that ${\sf ZF}$ (and, equally, ${\sf ZFC}$) has no "explicit" model.