Recently I have looked at logics on introductory level and was seduced to develop a perspective on base of Boolean algebras.
I experienced that as "enlightening" but I still feel a bit unsecure. This also because I did not really engaged Boolean algebras in the material used for learning.
So I decided to expose my "findings" here for some testing.
Thank you very much in advance.
Let $\mathcal L$ denote a language and let $S(\mathcal L)$ denote the set of $\mathcal L$-sentences.
Usually based on a deduction system an expression like $\Sigma\vdash\phi$ states that $\phi\in S(\mathcal L)$, that $\Sigma\subseteq S(\mathcal L)$ and that a deduction of $\phi$ from $\Sigma$ exists.
Abbreviating $\{\psi\}\vdash\phi$ by $\psi\vdash\phi$ let us look at $\vdash$ as a relation on $S(\mathcal L)$.
It is evident that in that context $(S(\mathcal L),\vdash)$ is a preorder with specific properties. As any preorder it induces a poset $\mathcal B_{\vdash}$ which can be shown to be a Boolean algebra. The elements of $\mathcal B_{\vdash}$ are equivalence classes of the relation $\sim$ prescribed by $\phi\sim\psi\iff \phi\vdash\psi\text{ and }\psi\vdash\phi$ and in the sequel I denote such classes as $[\phi]_{\vdash}$.
Similarly we can construct a Boolean algebra $\mathcal B_{\vDash}$ on base of the semantic relation $\vDash$.
It seems to me that proving the completeness theorem is actually the same as proving that $\mathcal B_{\vdash}$ and $\mathcal B_{\vDash}$ coincide, or equivalently that the two relation $\vdash$ and $\vDash$ defined on $S(\mathcal L)$ coincide. If I understood well then the essence of proving the completeness theorem is proving that every ultrafilter of $\mathcal B_{\vdash}$ can be written as $\{[\chi]_{\vdash}\mid \chi\in\mathsf{Th}(\mathfrak A)\}$ where $\mathfrak A$ denotes some $\mathcal L$-structure.
The statement $\Sigma\nvdash\phi$ can be translated to: "$[\phi]_{\vdash}$ is not an element of the filter generated by $\{[\psi]_{\vdash}\mid \psi\in\Sigma\}$".
Now if the statement $\phi\vdash\psi$ is false then some ultrafilter $U$ exists with $[\phi]_{\vdash}\in U$ and $[\psi]_{\vdash}\notin U$. Then $U=\{[\chi]_{\vdash}\mid \chi\in\mathsf{Th}(\mathfrak A)\}$ for some $\mathcal L$-structure $\mathfrak A$ so that $[\phi]_{\vdash}\in\mathsf{Th}(\mathfrak A)$ and $[\psi]_{\vdash}\notin\mathsf{Th}(\mathfrak A)$, proving that the statement $\phi\vDash\psi$ is false as well.
That means that $\phi\vDash\psi\implies\phi\vdash\psi$ and the opposite direction is a consequence of soundness.
Everything okay above? Finally I wondered: "why are Boolean algebras not mentioned?" Is it so maybe that logicians – busy with meta-mathematics – automatically avoid mathematics as much as possible to keep things unmixed?
Best Answer
They are indeed mentioned, and in fact play a fundamental role - however, they're generally introduced after the completeness theorem is proved, which means they aren't considered separately. The corresponding algebra and its various relatives (see below) are called Lindenbaum(-Tarski) algebras.
Pedagogically, this is a slightly awkward situation: for students who haven't seen Boolean algebras before, introducing the $\mathcal{B}_?$s before we can do something with them is probably not helpful, but for students who have seen Boolean algebras before it could be quite illuminating. Most classes err towards the former population.
In the rest of this answer I'll make some comments to flesh out the picture.
First, note that in general we go beyond the picture above. Specifically, we generalize from sentences to formulas with free variables from some prescribed set $\{x_1,...,x_n\}$, and work modulo a theory $T$ (so the equivalence relation is "$T$-provable equivalence"). Call this "$\mathcal{B}_n(T)$." When $T$ is complete, the ultrafilters on $\mathcal{B}_n(T)$ are just $n$-types, and give us the type space. This is where these algebras really take off in classical model theory, e.g. in the omitting types theorem. Accordingly, this is usually the point at which this notion appears in introductory logic curricula.
Second, we can look at logics beyond first-order logic (their study being abstract model theory). While not visible in the first-order situation, there's an interesting subtlety between the completeness properties for individual sentences and sets of sentences which is mediated by the compactness of the semantics involved.
Specifically, consider the following four facts:
$\mathcal{B}_\vdash=\mathcal{B}_\models$ (that is, $\varphi\vdash\psi\iff\varphi\models\psi$ for all sentences $\varphi,\psi$).
Ultrafilters on $\mathcal{B}_\models$ correspond exactly to theories of structures.
$\vdash$ and $\models$ coincide on sets of sentences: $\Phi\vdash\Psi\iff\Phi\models\Psi$ for $\Phi,\Psi\subseteq Sent$.
Ultrafilters on $\mathcal{B}_\vdash$ correspond exactly to theories of structures.
Point (2) is just the compactness theorem; note that we can prove compactness without proving completeness first (e.g. via ultraproducts), so there is a meaningful distinction between the two. Meanwhile point (3) is the completeness theorem and point (4) follows from points (2) and (3). Moreover, these relationships are very general: they apply to abstract logics in general. (Here by "abstract logic" I mean a triple $\mathcal{L}$ consisting of a set $Sent_\mathcal{L}$ of sentences, a proves relation $\vdash_\mathcal{L}$, and a satisfies relation $\models_\mathcal{L}$ satisfying some very mild properties - not including completeness.)
Point (1), interestingly, is surprisingly weak in general! Take a non-compact entailment relation $\models_*$ on some set of sentences (say, the usual semantics for second-order logic) and let $\vdash_*$ be its "finitization" $$\Gamma\vdash_*\varphi\quad\iff\quad\exists\Gamma_0\subseteq_{fin}\Gamma(\Gamma_0\models_*\varphi).$$ Point (1) holds but point (3) fails for the resulting system. Meanwhile, point (2) of course fails since $\models_*$ is noncompact. So really what we have is that (1) by itself isn't very strong, but (1)+(2) is.
Finally, changing stances entirely note that we can choose to take the deductive structure as primitive, and ignore semantics entirely. This takes us into the realm of algebraic logic. Roughly speaking, there we consider deductive systems which are simply free algebras $A$ (thought of as the set of wffs given by some basic syntactic rules) equipped with a deduction relation $\vdash$ satisfying some very mild properties.
We can recast a deduction system $\mathfrak{D}=(A,\vdash)$ as a Lindenbaum-like algebra given by elements of $A$ preordered by $\vdash$, and taking the obvious quotient yields a partial order. However, this partial order does not in general faithfully reflect the structure of $\mathfrak{D}$! Specifically, there may be syntactic operations which are not well-defined on $\vdash$-equivalence classes. Really what we want to look at are congruences on the algebra $A$ which are related to the deduction relation $\vdash$. The book Algebraizable Logics by Blok/Pigozzi is a wonderful treatment of this topic with lots of examples, and the introduction already gives a good taste of the topic and is freely available online from the AMS.