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!

  • 0
    I presume that $\mathbb F(x)$ is all the finite subsets of $x$? This is a new notation for that, I have to say.2011-09-13
  • 0
    This is a notation apparently introduced by the "Z" specification method. http://www.rose-hulman.edu/class/csse/cs415/zrm.pdf page 1112011-09-13
  • 0
    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.2011-09-13
  • 0
    @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)$.2011-09-14
  • 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-definable-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).

  • 0
    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.2011-09-13
  • 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