Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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!

share|cite|improve this question
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. 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
up vote 1 down vote accepted

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

share|cite|improve this answer
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. – Asaf Karagila Sep 13 '11 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 Sep 14 '11 at 10:55

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.