Three-variable statements of set-pairing (Q1885036)

Tarski discovered that in elementary systems for set theory (à la Zermelo) there are formulas \(D\) and \(E\) containing at most three variables -- two of them free -- such that in every model of the system the binary relations defined by these formulas are functions that have the property: for every \(x, y\) in the universe there is a \(z\) which is mapped to \(x\) by \(D\) and to \(y\) by \(E\). Tarski and Givant called these functions a pair of \textit{conjugated quasiprojections}. Using such functions Tarski and Givant were able to translate many set theories into a restricted predicate calculus with only three variables and then into the calculus of binary relations as equational theories without variables. From the authors' summary: ``The approach to algebraic specifications of set theories proposed by Tarski and Givant inspires current research aimed at taking advantage of the purely equational nature of the resulting formulations for enhanced automation of reasoning on aggregates of various kinds \(\ldots\) The viability of the said approach rests upon the possibility to form ordered pairs and to decompose them by means of conjugated projections.'' The authors consider different definitions of pairing functions within several axiom systems of weak set theory. They then make translations into the calculus of binary relation, obtaining variable-free equational versions of these weak theories. They also experimentally probe the borderline where expressibility in three variables fails.