Lindenbaum–Tarski algebra

In mathematical logic, the Lindenbaum–Tarski algebra (or Lindenbaum algebra) of a logical theory T consists of the equivalence classes of sentences of the theory (i.e., the quotient) under the equivalence relation ~ defined such that p ~ q exactly when p and q are provably equivalent in T. That is, two sentences are equivalent if the theory T proves that each implies the other. The Lindenbaum–Tarski algebra is thus the quotient algebra obtained by factoring the algebra of formulas by this congruence relation.

Source: Wikipedia — Lindenbaum–Tarski algebra (CC BY-SA 4.0)