This Demonstration enables the user to decide whether a formula of equivalential calculus is a tautology. Is there any simple rule? The Demonstration also introduces the notion of the set of a formula, a measure of the symmetry of the formula of equivalential calculus.
In 1929 Le\:015bniewski 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 :
if is a propositional variable, otherwise .
This definition has a simple consequence for equivalential calculus: a subformula of a formula is in iff there is an odd number of occurrences of in formula . So 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 sets.
The notion also provides a measure for the symmetry of formulas. Only formulas like have singleton sets.
 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, 20(40), 1985 pp. 269–270.