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?
Best Answer
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}$.