En los comentarios a la respuesta de Rob Arthan, el OP ha ampliado su pregunta:
¿Existe una técnica de forzamiento de tipos similar (que mantenga en su mayor parte la misma interpretación de los símbolos) que genere modelos de sistemas formales tales que una declaración particular sea verdadera en un modelo y la negación verdadera en otro modelo, manteniendo la consistencia interna de ambos modelos?
Es esta aclaración la que quiero abordar.
Es un poco confuso -en particular, la frase "que en su mayoría mantiene la misma interpretación de los símbolos" no tiene mucho sentido para mí-, pero interpreto todo el comentario como una pregunta:
Supongamos que $T$ es una teoría y $\varphi$ es una frase independiente de $T$ . ¿Existe un método para construcción de modelos de $T\cup\{\varphi\}$ y $T\cup\{\neg\varphi\}$ ? En particular, ¿hay alguna que sea similar al forzamiento, en el sentido de que se parte de un modelo de $T$ y "ampliarlo" de ciertas maneras? Y por último, ¿hay más similitudes entre ese método y el forzamiento?
Tenga en cuenta que, al tratarse de una pregunta sobre construcción de modelos frente a la consistencia de las teorías, aquí hay un poco más de sutileza. (Y ese aspecto está completamente ausente en el título y en la pregunta del cuerpo, así que si este es lo que estás preguntando deberías editarlos, y si no es lo que estás preguntando entonces necesitas aclarar más tu pregunta).
La respuesta a su pregunta, interpretada de esta manera, es sí . Antes de entrar en detalles, permítanme hacer un resumen: deberían investigar el teorema de completitud de Goedel (¡no es una errata!) y su demostración mediante la henkinización.
Bien, ahora (algunos) detalles:
En primer lugar, olvidemos la "estructura de base" y fijémonos en el proceso de construcción de un modelo de teoría consistente. Resulta que esto siempre se puede hacer y, de hecho, hay un método específico para hacerlo llamada "Henkinización". Aunque no es equivalente al forzamiento, éste (y ideas más avanzadas en la misma línea ) comparten un parecido familiar con el forzamiento: a grandes rasgos, construyen el objeto deseado en "etapas", cumpliendo varios "requisitos" por el camino, y confiando en un comportamiento suficientemente "genérico" para asegurar que funcionan como se desea. (Aclarar lo que significa todo esto requiere un lote de trabajo, y forzar en particular es realmente muy duro; pero puede que le interese estas tomas de fuerza desde una perspectiva intuitiva .)
Así que la Henkinización nos permite construir explícitamente un modelo $M$ de cualquier teoría consistente $T$ . En particular, si $\varphi$ es independiente de $T$ entonces ambos $T\cup\{\varphi\}$ y $T\cup\{\neg\varphi\}$ son consistentes, por lo que tenemos un método (Henkinización) que puede construir modelos de cada uno. Ahora, ¿qué pasa si intentamos ampliar una estructura determinada ¿en lugar de construir uno ex nihilo? Es decir, supongamos $T$ es alguna teoría y $\varphi$ es independiente de $T$ y $M$ es un modelo de $T$ . ¿Puedo producir modelos $M_0$ , $M_1$ que son "más grandes" que $M$ en el que $\varphi$ es verdadero y falso respectivamente? (En particular, este proceso debe ser garantizado que funciona para todos $M$ - no debería depender de $M$ teniendo alguna forma específica).
La respuesta depende de lo que se entienda exactamente por "mayor" (hay muchas formas de comparar estructuras matemáticas), pero bajo una interpretación la respuesta es afirmativa para una amplia clase de teorías. A saber, bajo hipótesis bastante razonables sobre $T$ (es suficiente para $T$ sea completa para las oraciones sin cuantificador, lo que equivale a $T$ decidir exactamente qué tipos de comportamiento "local" se dan en sus modelos - por ejemplo, la teoría de grupos no es completa para oraciones sin cuantificador, porque algunos grupos son no abelianos (= tienen la configuración " $a*b\not=b*a$ ") mientras que otros son abelianos (= no tienen esa configuración)) cada una de las teorías $$T_0=T\cup AtDiag(M)\cup\{\varphi\}$$ y $$T_1=T\cup AtDiag(M)\cup\{\neg\varphi\}$$ es coherente; aquí " $AtDiag(M)$ " es el diagrama atómico de $M$ que describe a un nivel muy básico cómo los elementos de $M$ se relacionan entre sí. Aplicando la Henkinización se obtienen modelos $M_0$ y $M_1$ de $T_0$ y $T_1$ respectivamente; y como cada uno de $T_0$ y $T_1$ satisfacen el diagrama atómico de $M$ , $M$ "incrustaciones" en un sentido preciso en $M_0$ y $M_1$ .
EDIT: Se puede preguntar razonablemente:
¿Qué tan complicada es la Henkinización?
Esta es una pregunta un poco vaga, pero una forma de precisarla es a través de teoría de la computabilidad podemos preguntar, dada una teoría computable $T$ ¿es fácil calcular (= construir de forma completamente explícita) un modelo de $T$ por la Henkinización? Y, ¿cómo de fácil es calcular un modelo de $T$ a través de cualquier método (es decir, ¿la Henkinización es óptima)?
Resulta que la Henkinización es óptima y produce modelos de forma "casi computable". En concreto, siempre podemos encontrar un modelo de $T$ que es bajo - es decir, cuyo problema de detención no es más complicado que el problema de detención clásico . Más concretamente, cualquier Grado de AP calcula un modelo de $T$ (y hay grados bajos de PA ). Tal modelo puede ser construido vía Henkinización, y este resultado es óptimo - hay teorías computables, cada modelo de las cuales computa un grado PA.
Y de hecho, si $T$ es decidible, entonces el proceso de Henkinización puede hacerse computable ¡! Así que la complejidad que existe proviene del paso técnico de completar la teoría, no de la parte de construcción de modelos de la Henkinización en sí. Por lo tanto, la conclusión para mí es que el teorema de completitud de Goedel está muy cerca de ser constructivamente cierto.
