 Nonetheless, we can perform some of the steps of the Lindenbaum-Tarski method in the logic \(\blK\). We can define the Leibniz congruence of every \(\blK\)-theory in a uniform way by using formulas in two variables. But in this particular case the set of formulas has to be infinite. Let \(\Delta(p, q) = \{\Box^n (p \leftrightarrow q): n\) a natural number\(\}\), where for every formula \(\phi , \Box^0\phi\) is \(\phi\) and \(\Box^n\phi\) for \(n \gt 0\) is the formula \(\phi\) with a sequence of \(n\) boxes in front \((\Box \ldots \Box \phi)\). Then, for every \(\blK\)-theory \(T\) the relation \(\theta(T)\) defined by