If you believe ACA is meaningful, then we can use ACA to express the question of whether ZFC has a model (but note that this is not what a set theorist would consider to be the same, since "model" in ACA is necessarily countable from the viewpoint of any 'stronger' set/type theory).
If we ignore the "countable" issue, since even ZFC proves that a countable theory that is consistent has a countable model, then we can state your question in ACA.
But what is its truth-value? If we believe ACA is meaningful, then we have to believe that your question has a definite truth-value.
The problem is that we can't prove it without at least proving Con(ZFC).
And ACA itself can easily prove that Con(ZFC) is stronger than Con of a lot of other things.
In particular, we have ACA |− Con(ZFC) ⇒ Con(ACA).
So by incompleteness theorem ACA cannot prove "ZFC has a model".
Yours is even stronger; you want "ZFC has an arithmetically definable model (namely its domain and membership relation are definable by arithmetical formulae)".
By the above argument ACA cannot prove that either.
So what extra do we need?
Well... I'm pretty sure ACA+Con(ZF) proves "ZF has an arithmetically definable model".
@LeakyNun AC disappeared in my claim because it is an existential axiom that is not equivalent to a unique existential.
@LeakyNun: Wait I realize that I'm being silly; if we're just interested in an arithmetically definable model, not a 'nice looking' model, then it suffices to use what I described here:
Nov 18 '17 at 4:57, by
user21820 @LeakyNun: I'll elaborate on my point that we can in fact perform that process using the first Turing jump H(1), also known as the halting oracle. There are many programs using H(1) that are proof verifiers for a complete consistent extension of any consistent formal system. You just use any computable enumeration of all sentences, and at each step you use H(1) to find out whether that current sentence is consistent with the previous ones and if so then add it but otherwise add its negation.
Take any consistent first-order theory S. Build a program that uses H(1) to decide a complete theory S' extending S. Then you can Skolemize S' using H(2), to obtain a complete theory S* with only universal axioms. Then you can obtain the term model of S* modulo provable equality using H(3). So you get an arithmetically definable model of S.
Does this make sense, or do you want me to elaborate? H(k) can be encoded as a Σ[k]-formula over PA, as sketched here:
2
Based on Gro-Tsen's answer, I believe that my proposed extension in my question should work in general, but needs $S$ to uniformly interpret PA. In contrast, I believe I have a way that only needs $S$ to interpret PA$^-$! (Note that PA$^-$ interprets TC, and the same holds for even weaker systems...
The reason I had omitted AC earlier is that I had been thinking of a nice presentation of ZF where we do not just have the "∈" relation but also have a set-union symbol and set-builder notation that would essentially act as Skolem functions for the pairing axiom and the specification and replacement schemas, and also a constant-symbol "ω" to witness the axiom of infinity. Then we would have a much nicer model, because we just need to take the term model.
AC does not fit simply because we don't have a Skolem function for it. If we add such, we effectively would have ZF + GC (global choice). All the other Skolem functions are conservative, for the reason I gave, namely all those axioms are equivalent to unique existentials by extensionality. AC is different, because it is not equivalent to a unique existential over ZF.
@LeakyNun: Do you get what I'm saying?
