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!
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).