Puede que el juego de poder ser axiomatised?

Question

Quiero considerar muchos ordenados de primer orden de la lógica con la distinguida tipo $U$$P$.

Puedo un estado finito (?) conjunto de fórmulas de primer orden tal, que cualquier modelo de $M = (D^U, D^P, I)$ interpreta el tipo $P$ como el conjunto de los subconjuntos finitos de la interpretación de $U$. Que es: $$D^P \stackrel{\sim}{=} \{X \subseteq {D^U} \mid X \mbox{ is finite}\} = \mathbb{F}(D^U) \subseteq 2^{D^U}$$

Parece que $\mathbb{F}(D^U) \subseteq D^P$ puede ser requerido por los axiomas.

Gracias por sus respuestas!

Answer 1

No. No tome un trivial ultrapower de un modelo con $D^U=\mathbb{N}$. El $D^U$ de este ultrapower es un modelo no estándar de los números naturales, y si x es un elemento no estándar de es $\{y \in D^U|y\lt x\}$ es un infinito elemento de $D^P$ (si no fuera un elemento de $D^P$ tendríamos que $\forall x \in D^U \exists y \in D^P \forall z \in D^U z \in y \iff z \lt x$ fue de primer orden enunciado verdadero en el modelo original, pero no la ultrapower, contradiciendo Łoś del teorema).