# 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. Commented Sep 13, 2011 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
Commented Sep 13, 2011 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. Commented Sep 13, 2011 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
Commented Sep 14, 2011 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. Commented Sep 14, 2011 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).

• What about ZFC in which being finite is well defined? The question is whether or not this thing is possible, not if it is always possible. Commented Sep 13, 2011 at 23:05
• 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.
– aaa
Commented Sep 14, 2011 at 10:55