# Can the power set be axiomatised?

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.

-
I presume that $\mathbb F(x)$ is all the finite subsets of $x$? This is a new notation for that, I have to say. –  Asaf Karagila Sep 13 '11 at 18:54
This is a notation apparently introduced by the "Z" specification method. rose-hulman.edu/class/csse/cs415/zrm.pdf page 111 –  Matt Sep 13 '11 at 19:09
Matt, do you have any further assumptions about the theory? Do you want the characterization to be internal or external? (That is $M$ would think that $D^P$ is all the finite sets of $D^U$, or is it enough for us to know that externally? I find the question unclear on that matter, and I have somewhat of a trouble trying to answer it due to that. –  Asaf Karagila Sep 13 '11 at 21:55
@Asaf Karagila. Perhaps I could rephrase it: Let the signature contain a predicate $in(U,P)$. Is there a set of axioms such that every model is isomorphic to the one with $D^P=\mathbb{F}(D^U)$ and $in^I(x,y) = (x\in y)$. –  Matt Sep 14 '11 at 9:54
While I'm not sure if this question is actualyl a duplicate of this one, I am pretty certain you could find it helpful. –  Asaf Karagila Sep 14 '11 at 16:50

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