|
|
|
|
Lindenbaum-Tarski algebra
|
(Definition)
|
|
|
Let  be a classical propositional language. We define the equivalence relation  over formulas of  by
 if and only if
 . Let  be the set of equivalence classes. We define the operations join  , meet  , and complementation, denoted
![$ [\varphi]'$](http://images.planetmath.org:8080/cache/objects/2997/l2h/img9.png "$ [\varphi]'$") on  by :
We let
![$ 0=[\varphi\wedge \neg\varphi]$](http://images.planetmath.org:8080/cache/objects/2997/l2h/img17.png "$ 0=[\varphi\wedge \neg\varphi]$") and
![$ 1=[\varphi\vee \neg\varphi]$](http://images.planetmath.org:8080/cache/objects/2997/l2h/img18.png "$ 1=[\varphi\vee \neg\varphi]$") . Then the structure
 is a Boolean algebra, called the Lindenbaum-Tarski algebra of the propositional language  .
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  and the connectives
 and that  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, “
 ” is considered the same as “
 ”. 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  's and their negations.
It can be shown that the Lindenbaum-Tarski algebra of the propositional language  is a free Boolean algebra freely generated by the set of all elements ![$ [p]$](http://images.planetmath.org:8080/cache/objects/2997/l2h/img28.png "$ [p]$") , where each  is a propositional variable of 
Now, let  be a first order language. As before, we define the equivalence relation  over formulas of  by
 if and only if
 . Let  be the set of equivalence classes. The operations  and  and complementation on  are defined exactly the same way as previously. The resulting algebra is the Lindenbaum-Tarski algebra of the first order language  . It may be shown that
where  is the set of all terms in the language  . Basically, these results say that the statement
 is equivalent to taking the supremum of all statements
 where  ranges over the entire set  of variables. In other words, if one of these statements is true (with truth value  , as opposed to 0), then
 is true. The statement
 can be similarly analyzed.
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.
|
"Lindenbaum-Tarski algebra" is owned by CWoo. [ full author list (3) | owner history (2) ]
|
|
(view preamble)
| Other names: |
Lindenbaum algebra |
|
|
Cross-references: Heyting algebra, logical languages, entire, ranges, supremum, terms, first order language, variable, freely generated, free Boolean algebra, negations, polynomials, Boolean, disjunctive normal form, propositional calculus, equivalent, tautologies, connectives, number, simple, logically equivalent, algebra, Boolean algebra, structure, meet, join, operations, equivalence classes, formulas, equivalence relation, language
There are 4 references to this entry.
This is version 27 of Lindenbaum-Tarski algebra, born on 2002-06-02, modified 2008-04-24.
Object id is 2997, canonical name is LindenbaumAlgebra.
Accessed 3449 times total.
Classification:
| AMS MSC: | 03B10 (Mathematical logic and foundations :: General logic :: Classical first-order logic) | | | 03B05 (Mathematical logic and foundations :: General logic :: Classical propositional logic) | | | 03G05 (Mathematical logic and foundations :: Algebraic logic :: Boolean algebras) |
|
|
|
|
|
|
Pending Errata and Addenda
|
|
|
|
|
|
|
|
|
|
|
![$\displaystyle [\varphi]\vee [\psi]$](http://images.planetmath.org:8080/cache/objects/2997/l2h/img11.png "$\displaystyle [\varphi]\vee [\psi]$"){kind=small}
![$\displaystyle :=[\varphi\vee \psi]$](http://images.planetmath.org:8080/cache/objects/2997/l2h/img12.png "$\displaystyle :=[\varphi\vee \psi]$"){kind=small}
![$\displaystyle [\varphi]\wedge [\psi]$](http://images.planetmath.org:8080/cache/objects/2997/l2h/img13.png "$\displaystyle [\varphi]\wedge [\psi]$"){kind=small}
![$\displaystyle :=[\varphi\wedge \psi]$](http://images.planetmath.org:8080/cache/objects/2997/l2h/img14.png "$\displaystyle :=[\varphi\wedge \psi]$"){kind=small}
![$\displaystyle [\varphi]'$](http://images.planetmath.org:8080/cache/objects/2997/l2h/img15.png "$\displaystyle [\varphi]'$"){kind=small}
![$\displaystyle :=[\neg\varphi]$](http://images.planetmath.org:8080/cache/objects/2997/l2h/img16.png "$\displaystyle :=[\neg\varphi]$"){kind=small}
![$\displaystyle \bigvee_{t\in T}[\varphi(t)]$](http://images.planetmath.org:8080/cache/objects/2997/l2h/img41.png "$\displaystyle \bigvee_{t\in T}[\varphi(t)]$")
![$\displaystyle :=[\exists x \varphi(x)]$](http://images.planetmath.org:8080/cache/objects/2997/l2h/img42.png "$\displaystyle :=[\exists x \varphi(x)]$"){kind=small}
![$\displaystyle \bigwedge_{t\in T}[\varphi(t)]$](http://images.planetmath.org:8080/cache/objects/2997/l2h/img43.png "$\displaystyle \bigwedge_{t\in T}[\varphi(t)]$")
![$\displaystyle :=[\forall x \varphi(x)]$](http://images.planetmath.org:8080/cache/objects/2997/l2h/img44.png "$\displaystyle :=[\forall x \varphi(x)]$"){kind=small}