5
$\begingroup$

I want to consider many-sorted first order logic with distinguished sorts $U$ and $P$.

Can I state a (finite?) set of first order formulae such that any model $M = (D^U, D^P, I)$ interprets the sort $P$ as the set of finite subsets of the interpretation of $U$. That is: $D^P \stackrel{\sim}{=} \{X \subseteq {D^U} \mid X \mbox{ is finite}\} = \mathbb{F}(D^U) \subseteq 2^{D^U}$

It seems that $\mathbb{F}(D^U) \subseteq D^P$ can be required by a axioms.

Thanks for your answers!

  • 1
    While I'm not sure if this question is actualyl a duplicate of [this one](http://math.stackexchange.com/questions/894/why-is-the-finitely-many-quantifier-not-defina$b$le-in-first-order-logic), I am pretty certain you could find it helpful. – 2011-09-14

1 Answers 1

2

No. Take a non-trival ultrapower of a model with $D^U=\mathbb{N}$. The $D^U$ of this ultrapower is a nonstandard model a of the natural numbers, and if x is a nonstandard element of it $\{y \in D^U|y\lt x\}$ is an infinite element of $D^P$ (if it were not an element of $D^P$ we would have that $\forall x \in D^U \exists y \in D^P \forall z \in D^U z \in y \iff z \lt x$ was a first-order statement true in the original model but not the ultrapower, contradicting ĊoĊ›'s theorem).

  • 2
    You can make a first-order definition of finiteness in ZFC, but for any such definition there is a model of ZFC in which an infinite set satisfies that definition. – 2011-09-14