Mi pregunta es:
Deje $\mathbb{P}$ ser un obligando a y $\tau \in V^\mathbb{P}$ es un nombre. Supongamos que $$1_{\mathbb{P} \times \mathbb{P}} \Vdash_{\mathbb{P} \times \mathbb{P}} \tau_\text{left} = \tau_\text{right}$$
donde $\tau_\text{left}$ $\tau_\text{right}$ son los habituales de $\mathbb{P} \times \mathbb{P}$ nombres que se le da a la evaluación de las $\tau$, según la izquierda y la derecha genérico. Entonces, ¿es cierto que existe un conjunto $x \in V$ tal que $$1_\mathbb{P} \Vdash_\mathbb{P} \check x = \tau$$
Algunas observaciones:
Tenga en cuenta que esto es cierto para los nombres forzado a ser el conjunto de los números ordinales: Si hay un ordinal $\lambda$ tal que $1_\mathbb{P} \Vdash \tau \subset \check \lambda$, entonces la pregunta anterior es una respuesta positiva.
Básicamente, esto sigue preguntando para cada una de las $\alpha < \lambda$, si $1_\mathbb{P} \Vdash \check \alpha \in \tau$.
Si $1_{\mathbb{P}} \Vdash \tau \subseteq \check y$ algunos $y \in V$, entonces la pregunta debería ser también una respuesta positiva.
También se sabe que uno puede de código arbitrario establece como conjuntos de los números ordinales. Se puede intentar hacer esto en el forzamiento de la extensión. Sin embargo, para reducir este regreso a el subconjunto de los ordinales caso, uno tendría que tener la codificación bijection ser forzado a ser el mismo en cualquier producto genérico, que no estoy seguro es posible. Sin embargo, si $\tau$ está obligado a ser un subconjunto de un modelo de terreno, entonces uno puede elegir una codificación bijection a ser en el modelo de terreno.
Otra cosa a probar que puede ser un rango argumento sobre los nombres que se utilizan para hacer $\tau$. Usando este método, he de empezar a ejecutar en forzar declaración como $``\sigma \notin \check V"$. A continuación, trabajar con productos, me gustaría solicitar que la declaración de más de una forzando la extensión de $V[G]$. Yo no soy lo incómodo de usar este nombre para el modelo de terreno. Soy consciente de que el modelo de terreno es definible en $V[G]$ el uso de parámetros de $V$. Sin embargo, si en $V$, $1_\mathbb{P}$ las fuerzas de algunos declaración utilizando $\check V$ $G \times H$ son producto genérico, no estoy seguro de si $V[H]$ satisfacer una misma cosa con $V[G]$ en lugar del modelo de terreno. No estoy seguro de si el comportamiento usual de forzar declaraciones en los productos de trabajo para forzar la declaración de que se utilice el nombre para el modelo de terreno.
De manera intuitiva, se considera que, si un nombre se interpreta de la misma manera en todos los genéricos de extensión, entonces debe ser un motivo de elementos del modelo. Gracias por cualquier información que puede ser proporcionada.
