En la semántica Kriple, cada nodo tiene dos relaciones, $\models$ y $\Vdash$ . En el caso más sencillo, la lógica proposicional intuicionista, cada nodo es un modelo en el clásico sentido para algún alfabeto limitado en la lógica proposicional.
La magia de los marcos de Kripke consiste en utilizar colecciones parcialmente ordenadas de modelos clásicos para estudiar la lógica intuicionista (y también para estudiar la lógica modal). El punto clave es que, clásicamente, para satisfacer $A \to B$ sólo significa satisfacer $B$ o no satisfacer $A$ . Pero para fuerza $A \to B$ es más fuerte: significa que en cada descendiente del nodo, si $A$ es verdadera en ese descendiente, entonces $B$ también es cierto en la descendencia. Por lo tanto, la cuestión es que $\Vdash$ no es lo mismo que $\models$ .
El teorema de completitud para la lógica intuicionista y los marcos de Kripke muestra que la lógica de la relación de forzamiento $\Vdash$ se alinea exactamente con la lógica intuicionista.
Además, en la lógica modal, no existe ninguna cláusula para el $\Box$ o $\Diamond$ conectivos en la definición del clásico $\models$ relación. Pero hay definiciones para lo que significa forzar una fórmula que comienza con una de estas conectivas.
Esto está estrechamente relacionado con el forzamiento en la teoría de conjuntos, también. Algunos textos antiguos de teoría de conjuntos trabajaban con una relación de forzamiento "fuerte", que sólo daba lugar a una lógica intuicionista. Estos textos utilizaban entonces una incrustación de doble negación de la lógica clásica en la lógica intuicionista para estudiar el forzamiento en la lógica clásica. Los textos de teoría de conjuntos más recientes suelen incorporar la traducción de la doble negación directamente en la definición de la relación de forzamiento, o utilizan una definición más semántica que da automáticamente la lógica clásica. Esto puede ocultar la naturaleza intuicionista subyacente del forzamiento en teoría de conjuntos.
