LindenbaumAlgebra 2002-06-02 10:29:36 2008-04-24 21:21:34 Definition % this is the default PlanetMath preamble. as your knowledge % of TeX increases, you will probably want to edit this, but % it should be fine as is for beginners. % almost certainly you want these \usepackage{amssymb} \usepackage{amsmath} \usepackage{color} \usepackage{amsfonts} % used for TeXing text within eps files %\usepackage{psfrag} % need this for including graphics (\includegraphics) %\usepackage{graphicx} % for neatly defining theorems and propositions %\usepackage{amsthm} % making logically defined graphics \usepackage[arrow,curve,poly,arc,2cell,frame,web]{xypic} % there are many more packages, add them here as you need them % define commands here \newcommand{\br}{[\![} \newcommand{\rb}{]\!]} \newcommand{\oq}{\text{``}} \newcommand{\cq}{\text{''}} \newcommand{\im}{\mathbf{Im}} \newcommand{\dom}{\mathbf{Dom}} \newcommand{\Or}{\vee} \newcommand{\Implies}{\Rightarrow} \newcommand{\Iff}{\Leftrightarrow} \newcommand{\proves}{\vdash} \renewcommand{\And}{\wedge} \newcommand{\Sup}{\bigwedge} \newcommand{\Inf}{\bigvee} \newcommand{\Z}{\mathbb{Z}} \newcommand{\F}{\mathbb{F}} \newcommand{\Q}{\mathbb{Q}} \newcommand{\R}{\mathbb{R}} \newcommand{\C}{\mathbb{C}} \newcommand{\Nat}{\mathbb{N}} \newcommand{\M}{\mathfrak{M}} \newcommand{\N}{\mathfrak{N}} \newcommand{\A}{\mathfrak{A}} \newcommand{\B}{\mathfrak{B}} \newcommand{\K}{\mathfrak{K}} \newcommand{\G}{\mathbb{G}} \newcommand{\Def}{\overset{\operatorname{def}}{:=}} \newcommand{\spec}{\text{{\bf Spec}}} \newcommand{\stab}{\text{{\bf Stab}}} \newcommand{\ann}{\text{{\bf Ann}}} \newcommand{\irr}{\text{{\bf Irr}}} \newcommand{\qt}{\text{{\bf Qt}}} \newcommand{\st}{\mathcal{Qt}} \newcommand{\ro}{\mathbf{r.o.}} \newcommand{\Endo}{\text{{\bf End}}} \newcommand{\mat}{\text{{\bf Mat}}} \newcommand{\der}{\text{{\bf Der}}} \newcommand{\rad}{\text{{\bf Rad}}} \newcommand{\trd}{\text{{\bf tr.d.}}} \newcommand{\cl}{\text{{\bf acl}}} \newcommand{\Int}{\text{{\bf int}}} \newcommand{\V}{\mathbb{V}} \newcommand{\D}{\mathbf{D}} \newcommand{\del}{\partial} \renewcommand{\O}{\mathcal{O}} \newcommand{\aut}{\mathbf{Aut}} \newcommand{\height}{\text{\bf Height}} \newcommand{\coheight}{\text{\bf Co-height}} \newcommand{\lcm}{\operatorname{lcm}} \newcommand{\Gal}{\operatorname{Gal}} \newcommand{\x}{\mathbf{x}} \newcommand{\y}{\mathbf{y}} \newcommand{\inner}[2]{\langle #1|#2\rangle} \renewcommand{\r}{{r}} \renewcommand{\t}{{t}} \newcommand{\restr}{\upharpoonright} \newcommand{\Matrix}[4]{\left(\begin{array}{cc} #1 & #2 \\ #3 & #4 \end{array}\right)} \subsubsection*{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 : \begin{align*} [\varphi]\vee [\psi]&:=[\varphi\Or\psi]\\ [\varphi]\wedge [\psi]&:=[\varphi\And\psi]\\ [\varphi]'&:=[\neg\varphi] \end{align*} We let $0=[\varphi\And\neg\varphi]$ and $1=[\varphi\Or\neg\varphi]$. Then the structure $(B,\vee,\wedge,',0,1)$ is a Boolean algebra, called the \emph{Lindenbaum-Tarski algebra} of the propositional language $L$. 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$ \subsubsection*{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 \begin{align*} \bigvee_{t\in T}[\varphi(t)]&:=[\exists x \varphi(x)]\\ \bigwedge_{t\in T}[\varphi(t)]&:=[\forall x \varphi(x)] \end{align*} where $T$ is the set of all terms in the language $L$. Basically, these results say that the statement $\exists x \varphi(x)$ is equivalent to taking the supremum of all statements $\varphi(x)$ where $x$ ranges over the entire set $V$ of variables. In other words, if one of these statements is true (with truth value $1$, as opposed to $0$), then $\exists x\varphi(x)$ is true. The statement $\forall x\varphi(x)$ can be similarly analyzed. \textbf{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.