Construcción de un ejemplo que apoya el teorema de interpolación proposicional

Question

Estoy tratando de construir una prueba simple de la Proposicional Teorema de Interpolación. Para la siguiente, vamos a $At(\phi)$ el conjunto de la frase símbolos que se producen en una frase $\phi$. Supongamos que $\psi$ es un tautológica consecuencia de $\phi$, pero ni $\neg\phi$ ni $\psi$ es una tautología, y por lo $\psi$ no es tautológica consecuencia de $\phi$ por razones triviales. Quiero mostrar que hay alguna frase $\gamma$ tal que

i) $\gamma$ es un tautológica consecuencia de $\phi$.

ii) $\psi$ es un tautológica consecuencia de $\gamma$

iii) $At(\gamma)\subseteq At(\phi)\cap At(\psi)$

A partir iii) $\gamma$ debe ser construido a partir de la sentencia de símbolos que se encuentran tanto en $\phi$$\psi$, así que me mostró por primera vez que el $At(\phi)\cap At(\psi)\neq\emptyset$. Ya que ni $\neg\phi$ ni $\psi$ es una tautología, no debe existir la verdad asignaciones $V,W$ tal que $V(\neg\phi)=F$ $W(\psi)=F$ y a partir de esto $V(\phi)=T$$W(\phi)=F$. Si $At(\phi)\cap At(\psi)=\emptyset$ podemos definir una verdad asignación para la frase símbolos $p_i$,

$U(p_i)=V(p_i)$ si $p_i\in At(\phi)$, $U(p_i)=W(p_i)$ si $p_i\in At(\psi)$.

Pero, a continuación,$U(\phi)=V(\phi)=T$, pero $U(\psi)=W(\psi)=F$, lo que contradice el hecho de que $\psi$ es un tautológica consecuencia de $\phi$.

Mi pregunta ahora es, ¿hay algún tipo de método para la construcción de $\gamma$ tal que las condiciones i) y ii) están satisfechos?

Answer 1

En este papel por Krajíček, encontrará algunas otras pruebas del teorema de interpolación de Craig.

Answer 2

Inducción sobre el número de sentencia de los símbolos es el tipo de prueba de Craig dio originalmente, y es lo que los lógicos llaman sintáctico de la prueba. También es posible dar una semántica o modelo de la teoría de la prueba. Bell y Slomson dan una para la lógica de primer orden en el Capítulo 7, sección 4 de su texto los Modelos y Ultraproducts. No he visto un modelo de la teoría de la prueba para la lógica proposicional. (Presentado como una respuesta porque no tengo suficiente rep todavía comentario.)