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!

$\endgroup$
5
  • $\begingroup$ I presume that $\mathbb F(x)$ is all the finite subsets of $x$? This is a new notation for that, I have to say. $\endgroup$
    – Asaf Karagila ♦
    Commented Sep 13, 2011 at 18:54
  • $\begingroup$ This is a notation apparently introduced by the "Z" specification method. rose-hulman.edu/class/csse/cs415/zrm.pdf page 111 $\endgroup$
    – Matt
    Commented Sep 13, 2011 at 19:09
  • $\begingroup$ 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. $\endgroup$
    – Asaf Karagila ♦
    Commented Sep 13, 2011 at 21:55
  • $\begingroup$ @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)$. $\endgroup$
    – Matt
    Commented Sep 14, 2011 at 9:54
  • 1
    $\begingroup$ While I'm not sure if this question is actualyl a duplicate of this one, I am pretty certain you could find it helpful. $\endgroup$
    – Asaf Karagila ♦
    Commented Sep 14, 2011 at 16:50

1 Answer 1

Reset to default
2
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Asaf Karagila ♦
    Commented Sep 13, 2011 at 23:05
  • 2
    $\begingroup$ 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. $\endgroup$
    – aaa
    Commented Sep 14, 2011 at 10:55

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .