Lindenbaum-Tarski algebra of a propositional langauge

Let $L$ be a classical propositional language. We define the equivalence relation $\sim$ over formulas of $L$ by $\varphi\sim\psi$ if and only if $\proves\varphi\Iff\psi$ . Let $B=L/\sim$ be the set of equivalence classes. We define the operations join $\vee$ , meet $\wedge$ , and complementation, denoted $[\varphi]'$ on $B$ by :

Intuitively, this algebra is an algebra of logical statements in which logically equivalent formulations of the same statement are not distinguished. One can develop intuition for this algrebra by considering a simple case. Suppose our language consists of a number of statement symbols $P_i$ and the connectives $\lor, \land, \neg$ and that $\proves$ denotes tautologies. Then our algebra consists of statements formed from these connectives with tautologously equivalent satements reckoned as the same element of the algebra. For instance, ``$\neg (P_1 \land P_2)$ '' is considered the same as ``$\neg P_1 \lor \neg P_2$ ''. Furthermore, since any statement of propositional calculus may be recast in disjunctive normal form, we may view this particular Lindenbaum-Tarski algebra as a Boolean analogue of polynomials in the $P_i$ 's and their negations.

It can be shown that the Lindenbaum-Tarski algebra of the propositional language $L$ is a free Boolean algebra freely generated by the set of all elements $[p]$ , where each $p$ is a propositional variable of $L$

Lindenbaum-Tarski algebra of a first order langauge

Now, let $L$ be a first order language. As before, we define the equivalence relation $\sim$ over formulas of $L$ by $\varphi\sim\psi$ if and only if $\proves\varphi\Iff\psi$ . Let $B=L/\sim$ be the set of equivalence classes. The operations $\vee$ and $\wedge$ and complementation on $B$ are defined exactly the same way as previously. The resulting algebra is the Lindenbaum-Tarski algebra of the first order language $L$ . It may be shown that

Remark. It may possible to define the Lindenbaum-Tarski algebra on logical languages other than the classical ones mentioned above, as long as there is a notion of formal proof that can allow the definition of the equivalence relation. For example, one may form the Lindenbaum-Tarski algebra of an intuitionistic propositional language. The resulting algebra is not a Boolean algebra, however. Instead, it is a Heyting algebra.