Infinity in ZFC vs infinity in the metatheory

Question

I was reading about different ways to formalize the notion of infinity in ZFC. The classic axiom is of course to have the existence of an inductive set, but you can also assert the existence of a Dedekind infinite set, and it turns out it is equivalent. (This question shows this: How can I define $\mathbb{N}$ if I postulate existence of a Dedekind-infinite set rather than existence of an inductive set?)

They both give a notion of infinity internal to the theory. However, I am not quite sure how much this coincides with a "metatheoretic" understanding of infinity. For instance, let $L=\{=,\in\}$ and let $T$ be the $L$-theory consisting of all axioms of ZFC except for the axiom of infinity. Define a new language $L'=L\cup\{c\}$ with a single additional constant symbol, and define a new theory $$T'=T\cup\{\exists x_1\dots\exists x_n\bigwedge_{1\leq i<j\leq n}x_i\neq x_j\wedge\bigwedge_{i=1}^n x_i\in c:n\in\mathbb{N}\}.$$ This seems to be a very natural way to capture the notion of infinity, but I don't know whether we could prove that the realization of $c$ in a model of $T'$ is Dedekind-infinite in the sense of ZFC. Therefore, in light of the question I put a link to, my question is: is $T'$ equivalent to ZFC?

Answer 1

Not in any sense. $T'$ is in fact a conservative extension of $\mathsf{ZF}$-$\mathsf{Inf}$; this is a consequence of the compactness theorem.

Now any well-founded model (or even $\omega$-model) of $T'$ restricts to a model of $\mathsf{ZF}$, but in the absence of such a semantic restriction $T'$ is no better than $\mathsf{ZF}$.

Answer 2

No; in fact, $T'$ is conservative over $T$ (that is, it does not prove any theorems in $L$ that $T$ does not prove). Indeed, every finite fragment of $T'$ is satisfied in every model of $T$, by letting $c$ denote some set with enough elements to satisfy all of the finitely many axioms you include. Every theorem of $T'$ is proved from only finitely many of its axioms, so this means it can't prove anything over $L$ that isn't true in every model of $T$.