El forzamiento de la relación que Boolos, Burgess, y Jeffrey definir es lo que podría llamarse "fuerte forzado". Este es un caso muy concreto de relación, que es fácil de definir en el modelo de terreno, pero no en general respecto a la clásica lógica de la equivalencia. La lógica que se conserva es una intuitionistic uno (por "conservada", me refiero a la cuestión de que las reglas de inferencia son el sonido cuando provability es reemplazado por forzar).
Una cosa que es un poco confuso es que muchos de conjunto de la teoría de los libros que escribe ahora $\Vdash$ para la relación semántica: $p \Vdash \phi$ significa que por cada genéricos $G$ contiene $p$, $M[G]$ satisface $\phi$. Esta relación claramente conserva la lógica clásica, pero en su cara no hay manera de ver que es definible en el modelo de terreno.
Para demostrar que, a muchos de los contemporáneos de los libros de utilizar algunos decorados de notación (por ejemplo, $\Vdash^*$ o $\Vdash_s$) para definir un auxiliar de la relación (la que Boolos, Burgess, y Jeffrey llamar a $\Vdash$) que obviamente es definible en el modelo de terreno, pero que evidentemente no tiene las propiedades lógicas de la semántica de forzar la relación.
En cualquier caso, lo que se ha demostrado es que hay algunos forzando la relación definida en el modelo de terreno que tiene la propiedad:
Si $G$ es un filtro genérico, a continuación, $M[G]$ satisface una fórmula $\phi$ si y sólo si existe alguna condición en $G$ que las fuerzas de $\phi$
En mi versión de BB&J este es el Lema 23.7. Su exposición se centró en uno específico obligando noción, Cohen forzar, que permite mezclar el filtro genérico $G$ con el conjunto genérico, a la que llaman $A$, que se obtiene a partir del filtro. Así que toma un minuto para reconstruir los resultados generales de la especializada de las declaraciones de sus lemas.
Tienes razón en que puede definir a un "débil" forzar la relación $\Vdash_w$ desde el fuerte se $\Vdash_s$ con la regla de $p \Vdash_w \phi \Leftrightarrow p\Vdash_s \lnot\lnot \phi$, y, a continuación, la débil voluntad de preservar la lógica clásica.
El punto clave es que si $p \Vdash_s \lnot \lnot \phi$ entonces el conjunto de $r \leq p$ que la fuerza de $\phi$ es denso bajo $p$, y por lo tanto, cualquier filtro genérico que incluye a $p$ a un $r$. Por lo tanto, si todo un filtro genérico de las fuerzas de $\lnot \lnot \phi$ luego de que el filtro también obliga a $\phi$, incluso con la definición sintáctica de forzar. Del mismo modo, se sigue de la definición de $\Vdash_s$ que si $p \Vdash_s \lnot \lnot \lnot \lnot \phi$$p \Vdash_s \lnot \lnot \phi$, que no debe ser inesperado, si pensamos en $\Vdash_s$ como tener una especie de intuitionistic lógica.
En libros como Kunen, el $\Vdash^*$ relación es un poco diferente de las $\Vdash_s$ relación definida por BB&J. Kunen la definición de apelaciones a la densa establece en la cláusula de $(\exists x)$, mientras que el "fuerte" de la definición requiere que una condición que obliga a un cuantificador existencial tiene que la fuerza de un testimonio particular al mismo tiempo. Así que usted puede ver el $\Vdash^*$ tipo de definición directa de la incorporación de una doble negación, que es la forma en Kunen es capaz de demostrar lo $p \Vdash \phi \Leftrightarrow p \Vdash^* \phi$.
Parte 2
Deje $\Vdash_s$ ser el fuerte obligando relación de BB&J. Hemos de BB&J:
Lema 23.7. Si $G$ es un filtro genérico y $\phi$ es una frase, a continuación, $M[G]$ satisface $\phi$ si y sólo si hay un $p \in G$$p \Vdash_s \phi$.
Ahora la solución a su pregunta es, esencialmente, un poco de ejercicio con el punto clave que he mencionado anteriormente.
Proposición 1. $p \Vdash_s \lnot\lnot \phi$ si y sólo si para cada genéricos $G$ contiene $p$, $M[G]$ satisface $\phi$.
Para la dirección de avance, si $p \Vdash_s \lnot \lnot \phi$ entonces el conjunto de $r \leq p$ tal que $r \Vdash_s \phi$ es denso bajo $p$. Por lo tanto, cualquier filtro genérico que contiene $p$ contendrá un $r$, y por lo tanto $M[G]$ va a satisfacer $\phi$ por el lema.
Por el contrario, supongamos que para cada genéricos $G$ contiene $p$, $M[G]$ satisface $\phi$. Por contradicción, supongamos que hay una condición de $q \leq p$ que las fuerzas de $\lnot \phi$. A continuación, hay un filtro genérico $G$ contiene $q$$p$, y por el lema sabemos $M[G] $ satisface $\lnot \phi$. Esto es imposible por hipótesis, ya que $p \in G$.
Por lo tanto, por la definición de $\Vdash_s$, para cada $q \leq p$ hay algo de $r \leq q$$r \Vdash_s \phi$. Esto significa que el conjunto de tales $r$ es denso bajo $p$, lo que implica inmediatamente que $p \Vdash_s \lnot \lnot \phi$.
Proposición 2. Si $M[G]$ satisface $\phi \Leftrightarrow \psi$ por cada genéricos $G$ contiene $p$, $p \Vdash_s \lnot\lnot\phi$ si y sólo si $p \vDash_s \lnot\lnot\psi$.
Supongamos $p \Vdash_s \lnot\lnot\phi$. Luego, por la Proposición 1, $M[G] \vDash \phi$ por cada genéricos $G$ contiene $p$. Por lo tanto $M[G] \vDash \psi$ por cada genéricos $G$ contiene $p$, por hipótesis. La aplicación de la proposición de nuevo, $p \Vdash_s \lnot\lnot \psi$.
