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.