Note 1. Early I posted a related question [Set-theoretic tautologies](https://mathoverflow.net/questions/176732/set-theoretic-tautologies). But the answer did not contain any concrete references to the literature. So I posted this, more precisely formulated question, hoping to receive a concrete reference to the literature.
In any case, I am thankful to François G. Dorais and Emil Jeřábek for their answers.


Note 2. Because the 2-element Boolean algebra $\mathbf2$ is isomorphic to the powerset algebra on a singleton $V$, we can use the set-theoretic
notations $\emptyset, V, \cup, \cap, C, \subseteq$ instead of normally used in $\mathbf2$ the notations $0,1,+,.,',\leq$.


Let $B$ be a power set Boolean algebra.


Let $P$ be an unquantified formula constructed using variables and the symbols $\emptyset, V$ (the universe),
$\cup, \cap, C, \subseteq, =$ (union, intersection, complement, inclusion, equality, respectively) such as, for example, $A \subseteq A \cup X$.


[It is well known](https://mathoverflow.net/questions/176732/set-theoretic-tautologies), that such a formula is valid in $B$ iff it is valid in the 2-element Boolean algebra $\mathbf2$.


So instead of proving $P$ in $B$, we can check that $P$ is true in $\mathbf2$ - by checking $2^n$ possible cases ($n$ is the number of variables in $P$) substituting instead of each variable $\emptyset$ or $V$ and calculating the result, using the obvious rules:
$\emptyset \cup \emptyset = \emptyset$,
$\emptyset \cup V = V$,
$V \cup \emptyset = V$,
$V \cup V = V$ and so on for $\cap, C, \subseteq$.


If the result is $\top$ in all cases then $P$ is true in $\mathbf2$ and, therefore, in $B$.


Note that this method also works for some unquantified formulas containing also some propositional connectives - in addition, after calculating all set terms in $P$ we should check that the resulting formula(not containing variables) is true.
For example, $A \subseteq B \rightarrow A \cup X \subseteq B \cup X$ is true in $\mathbf2$ and $B$.


But there are some formulas(for example, $X \subseteq Y \lor Y \subseteq X$) that are valid in $\mathbf2$ but not in $B$.


So my question is:


What is the widest class of unquantified formulas in $B$ containing variables, the above set-theoretic symbols and
propositional connectives, which are valid simultaneously in $\mathbf2$ and in $B$?



Formulas that are valid simultaneously in a power set Boolean algebra $B$ and the 2-element Boolean algebra $\mathbf2$
The class of formulas you're looking for contains all quasi-identities:
$$a\_1 = b\_1 \land \cdots \land a\_k = b\_k \to a = b$$
where $k \geq 0$ and $a,a\_1,\ldots,a\_k,b,b\_1,\ldots,b\_k$ are terms formed using $\varnothing,V,{\complement},{\cap},{\cup}$. (We can omit ${\subseteq}$ because $a \subseteq b \iff a \cap b = a$, for example.) I believe these may be exactly the class you're looking for, up to logical equivalence modulo the theory of Boolean algebras.


Some general context: The "well-known fact" from the question is a consequence of [Birkhoff's HSP Theorem](https://en.wikipedia.org/wiki/Variety_(universal_algebra)#Birkhoff%27s_theorem) which says that a nonempty class of algebras is closed under homomorphisms (H), subalgebras (S) and (arbitrary) products (P) if and only if it is axiomatized by identities (i.e., $a = b$ where $a,b$ are terms). There is a generalization of this theorem to quasi-identities which says that a nonempty class of algebras is closed under isomomorphisms (I), subalgebras (S), products (P) and ultraproducts (U) if and only if it is axiomatized by quasi-identities.


A first-order formula $\phi$ (in the language $\varnothing,V,{\complement},{\cap},{\cup},{=}$) with property ISP will have the required property that $\phi$ is valid in $\mathbf{2}$ iff it is valid in every powerset algebra. The forward direction follows from IP since the powerset algebras are isomorphic to powers of $\mathbf{2}$. The reverse direction follows from IS because every nontrivial Boolean algebra contains an isomorphic copy of $\mathbf{2}$.


Note that every first-order formula has property IU by [Łoś's Theorem](https://en.wikipedia.org/wiki/Ultraproduct#%C5%81o%C5%9B%27s_theorem), and every quantifier-free formula has property S. So perhaps the quasi-identities are what you're looking for?




---


*Addendum*: What if the powerset algebras are not meant to include the trivial Boolean algebra? Then the above can be modified to include [Horn formulas](https://en.wikipedia.org/wiki/Horn_clause) of the form
$$a\_1 = b\_1 \land \cdots \land a\_k = b\_k \to \bot$$
as well, provided that property P is restricted to *nonempty* products everywhere.


However, this is not a very substantial extension since
$$a\_1 = b\_1 \land \cdots \land a\_k = b\_k \to V = \varnothing$$
is a quasi-identity which is equivalent to the above for all nontrivial Boolean algebras.


