Lindenbaum algebra is a free algebra The following is a continuation of this question. 
I would like to prove that the Lindenbaum algebra is a free algebra. Hopefully I would like to hear hints on how to proceed in the 'right' direction.
Let $X$ be a set of propositional variables, $M$ the set of all boolean expressions over $X$ and $L = M/_{\sim}$ the partition of $M$ into logically equivalent sentences. 
The claim is that $L$ is free over $X$ with respect to the map $e:X \mapsto L$ defined as $e(x) = [x]$ where $[x]$ denotes the equivalence class of $x \in X.$
Let $B$ be any boolean algebra and $f:X\mapsto B$ any function. We want to argue that there is precisely one homomorphism $\overline{f}:L\mapsto B$ so that $\overline{f}\circ e = f.$ The only choice I see is to extend the map defined as
$$\overline{f}([a]) = f(x) \; \hbox{if} \; x \in X \; \hbox{and} \; [x] = [a]$$
to a homomorphism in the natural way (if $[a]$ is not the equivalence class of propositional element then apply $\overline{f}$ to recursively to the subterms of a compound element in $[a]$)
The following seems like the wrong way to do it since then one has many technicalities to show.


*

*$\overline{f}$ is well defined.

*That $\overline{f}$ is indeed the only possible homomorphism. Is it valid to use an inductive argument to show that if $\overline{g}$ is another such homomorphism then it has to be that $\overline{f} = \overline{g}$ since $f,g$ agree for all elements that are equivalence classes of propositional variables and any other element in $L$ is a finite expression of these? 
As said I believe I haven't defined $\overline{f}$ in a convenient way to allow me to prove the necessary conditions.
Is there a better way to approach this?
 A: What you’re doing is fine: you want to define $\bar f$ by structural recursion on formulas of $L$. The base of it is what you already have: $\bar f\big([x]\big)=f(x)$ for $x\in X$. Now if $\varphi,\psi\in L$ and $\bar f\big([\varphi]\big)$ and $\bar f\big([\psi]\big)$ have been defined, let 
$$\begin{align*}
&\bar f\big([\varphi\lor\psi]\big)=\bar f\big([\varphi]\big)\lor\bar f\big([\psi]\big),\\
&\bar f\big([\varphi\land\psi]\big)=\bar f\big([\varphi]\big)\land\bar f\big([\psi]\big),\text{ and }\\
&\bar f\big([\lnot\varphi]\big)=\lnot\bar f\big([\varphi]\big)\;.
\end{align*}$$
You know that if $\varphi\equiv\varphi'$ and $\psi\equiv\psi'$, then $\varphi\lor\psi\equiv\varphi'\lor\psi'$, $\varphi\land\psi\equiv\varphi'\land\psi'$, and $\lnot\varphi\equiv\lnot\varphi'$, so $\bar f$ is well-defined. To show that $\bar f$ is unique, just do what you sketched in (2): show by structural induction (parallel to the structural recursion defining $\bar f$) that if $g:L\to B$ is a homomorphism such that $g\!\upharpoonright\! X=f$, then $g=\bar f$.
