Definition (Lindenbaum-Tarski algebra). Let $Q$ be a logical doctrine (CPC, IPC, etc), $L$ be a propositional language, and $T$ be an $L$-theory. The Lindenbaum-Tarski algebra $F^Q(T)$ is built in the following way:

• The underlying set of $F^Q(T)$ is the set of equivalence classes $[\phi ]$ of propositions $\phi$, where $\phi \sim \psi$ when $T,\phi {⊢}_Q\psi$ and $T,\psi {⊢}_Q\phi$;

• If $\bowtie$ is a logical connective in the fragment $Q$, we set $[\phi ]\bowtie [\psi ]:=[\phi \bowtie \psi ]$ (should check well-defined: exercise).