In 1929 Leśniewski recognized that the equivalential calculus could be axiomatized. He also observed that a formula of propositional calculus in which equivalence is the only propositional function is a tautology if and only if each propositional letter occurs an even number of times .
The notion of the
set of a formula of propositional calculus with negation, implication, disjunction and conjunction is introduced in .
The definition for the equivalence is given in :
is a propositional variable, otherwise
This definition has a simple consequence for equivalential calculus: a subformula
of a formula
iff there is an odd number of
is a tautology iff no propositional variable is in
This notion also gives a linear lower bound on the proof length in equivalential calculus with an axiom schema (where substitution is applicable only to an axiom). We must only construct a set of tautologies with large
The notion also provides a measure for the symmetry of formulas. Only formulas like
 J. Łukasiewicz, "The Equivalential Calculus," in Polish Logic (1920–1939)
(S. McCall, ed.), Oxford: Clarendon Press, 1967, pp. 90–91.
 G. S. Ceitin and A. A. Chubaryan, "Some Estimates of Proof Length in Classical Propositional Calculus (in Russian)," Mathematical Questions of Cybernetics and Computation
, Erevan, DAN Arm. SSR, 1975 pp. 57–64.
 I. Hafner, "On Lower Bound of the Proof Length in the Equivalential Calculus," Glasnik Matematički
(40), 1985 pp. 269–270.