Suppose that a finiteness quantifier $\mathbf Fx$ is added to first order logic. Its semantics are: $\mathbf Fx\Phi(x)$ is true in a model just in case there a finitely many things in the domain of the model that satisfy $\Phi(x)$
So I have to prove an isomorphism with of $Th(\mathbb N)$ with the finiteness quantifier. But the kicker is that I cannot use any of the metatheory of regular FOL for this. No compactness etc. I really don't know how to proceed.
Does $Th(\mathbb N)$ even look that much different with a finiteness quantifier?
Any help is quite appreciated.