Tautologías teóricas de conjuntos

Question

Consideremos más concretamente las fórmulas no cuantificadas de una teoría de conjuntos (por ejemplo, NBG), las fórmulas, construidas a partir de variables y las constantes $\emptyset, V$ (el conjunto vacío y la clase de todos los conjuntos, respectivamente), utilizando únicamente los siguientes símbolos de la teoría de conjuntos: $\cup, \cap, C, \subseteq, =$ (unión, intersección, complemento, inclusión, eqaulidad, respectivamente).

Para cualquier fórmula F de este tipo, que no contenga conectivas proposicionales, se puede utilizar el siguiente procedimiento de decisión muy simple (VSDP):

Denotemos como Prop(F) el resultado de sustituir en F los símbolos $\cup, \cap, C, \subseteq,\emptyset, V, =$ sobre los símbolos $\vee, \wedge, \neg, \rightarrow, \equiv, false, true$ respectivamente.

Entonces la fórmula F es una tautología (set-teórica) si la formuala Prop(F) es una tautología proposicional.

Por ejemplo, la fórmula $X \subseteq X \cup Y$ es una tautología teórica de conjuntos, porque la fórmula Prop $(X \subseteq X \cup Y)$ Eso es, $X \rightarrow X \vee Y$ es una tautología proposicional.

Pero este procedimiento de decisión (VSDP) funciona también para algunas fórmulas no cuantificadas, que contienen también además de los símbolos $\cup, \cap, C, \subseteq, =$ también algunas conectivas proposicionales.

Por ejemplo, la fórmula $(X \subseteq X_1) \wedge (Y \subseteq Y_1) \rightarrow X \cup Y \subseteq X_1 \cup Y_1$ es una tautología set-teórica, y la fórmula $(X \rightarrow X_1) \wedge (Y \rightarrow Y_1) \rightarrow (X \vee Y) \rightarrow (X_1 \vee Y_1)$ es una tautología proposicional.

Así que mi pregunta es:

¿Cuál es la clase más amplia de fórmulas de este tipo a las que se puede aplicar este procedimiento de decisión muy simple (VSDP)?

Answer 1

$\DeclareMathOperator\pr{Prop}\let\sset\subseteq\let\nsset\nsubseteq$ En primer lugar, si $F$ es cualquier fórmula válida sin cuantificador, entonces $\pr(F)$ es una tautología: dada una asignación proposicional $e$ tal que $e(\pr(F))=0$ la valoración $$v(X)=\begin{cases}\varnothing&e(X)=0,\\V&e(X)=1\end{cases}$$ es un contraejemplo de $F$ . Por lo tanto, el problema es qué condiciones generales garantizan que cuando $\pr(F)$ es válido, $F$ es válido.

Sin más aclaraciones sobre lo que cuenta como "clase" de fórmulas, la única respuesta posible es que esto se cumple si y sólo si. (Por cierto, tanto las fórmulas válidas sin cuantificador como las tautologías proposicionales son coNP-completas).

La fórmula $X\sset Y\lor Y\sset X$ no es válida, sino su traducción proposicional, $(X\to Y)\lor(Y\to X)$ es. Nótese que esta fórmula es una cláusula formada por dos literales positivos.

Por otra parte, la traducción funciona fielmente para las fórmulas de Horn (conjunciones de cláusulas cada una de las cuales contiene a lo sumo un literal positivo). Basta con demostrarlo para las cláusulas de Horn $$\tag{$ * $}T_1(\vec X)\nsset T'_1(\vec X)\lor\cdots\lor T_n(\vec X)\nsset T'_n(\vec X)\lor T_0(\vec X)\sset T'_0(\vec X),$$ donde $T_i,T'_i$ son términos booleanos en variables de clase $X_j$ y puede que falte el último disyunto. Si $(*)$ no es válido, fije una valoración en $\vec X$ que lo refuta. Entonces $T_i(\vec X)\sset T'_i(\vec X)$ para todos $i>0$ pero $T_0(\vec X)\nsset T'_0(\vec X)$ . Fijar un elemento $a\in T_0(\vec X)$ tal que $a\notin T'_0(\vec X)$ . (Si el $T_0\sset T'_0$ falta en $(*)$ podemos tomar $a$ arbitrario). Definir una asignación proposicional $$e(X_j)=\begin{cases}0&a\notin X_j\\1&a\in X_j\end{cases}.$$ Entonces la misma expresión vale también para términos booleanos arbitrarios $T$ en lugar de $X_j$ Por lo tanto $e(T_i\to T'_i)=1$ para todos $i>0$ pero $e(T_0\to T'_0)=0$ . Así, la traducción proposicional de $(*)$ es falso en $e$ .

En $X\sset Y\lor Y\sset X$ ejemplo anterior (que obviamente se generaliza a cláusulas más largas con al menos dos literales positivos) muestra que siempre que restrinjamos la atención a clases de fórmulas definidas por la forma del esqueleto proposicional externo de la fórmula ignorando lo que hay dentro de las inclusiones atómicas, las fórmulas de Cuerno son las mejores posibles.

EDIT: Permítanme añadir una explicación de nivel superior. El conjunto de fórmulas válidas de la forma considerada en la pregunta es, salvo diferencias triviales de notación, la teoría universal del "conjunto de potencias" del álgebra booleana de todas las clases, que se ve fácilmente que coincide con la teoría universal de todas las álgebras booleanas no triviales (o: todas las álgebras booleanas no triviales finitamente generadas). Por otra parte, $\pr(F)$ es una tautología si $F$ se cumple en el álgebra booleana de 2 elementos $\mathbf2$ . Ahora, $\mathbf2$ genera álgebras booleanas como una cuasivariedad, y más concretamente, genera todas las álgebras booleanas no triviales utilizando subálgebras y productos directos no vacíos. Hasta equivalencia lógica, las sentencias universales de Horn son exactamente la clase de sentencias preservadas bajo subálgebras y productos directos no vacíos.