Lindenbaum algebra

In the mathematical logic is the Lindenbaum algebra (also Lindenbaum-Tarski algebra ) to a theory T the quotient algebra with respect to the equivalence relation of the provable equivalent sentences in T .

Algebra got its name after Adolf Lindenbaum . Alfred Tarski first published the construction of algebra in 1935 and showed that it is a Boolean algebra .

construction

Given a logical theory T and a system of proof, such as natural deduction (see e.g.), then one defines for formulas p and q :

${\displaystyle p\sim q\iff T\vdash p\to q{\text{ und }}T\vdash q\to p}$.

That the relation is reflexive and symmetrical follows directly from the definition. It is also transitive, because a proof for in can be constructed from proofs for and with the rules of removing the implication and introducing the implication . ${\displaystyle \sim }$ ${\displaystyle p\to q}$ ${\displaystyle q\to r}$ ${\displaystyle p\to r}$ ${\displaystyle T}$

We now denote with the equivalence class of with regard to this equivalence relation. The elements of Lindenbaum algebra are the equivalence classes and the operations of algebra as well as two distinctive elements, the zero and the one element, are defined as follows: ${\displaystyle [p]_{\sim }}$ ${\displaystyle p}$ ${\displaystyle {\mathcal {L}}}$

${\displaystyle [p]_{\sim }\cup [q]_{\sim }:=[p\lor q]_{\sim }}$

${\displaystyle [p]_{\sim }\cap [q]_{\sim }:=[p\land q]_{\sim }}$

${\displaystyle \quad \quad -[p]_{\sim }:=[\neg p]_{\sim }}$

${\displaystyle \quad \quad \quad \quad 0:=[\bot ]_{\sim }}$

${\displaystyle \quad \quad \quad \quad 1:=[\top ]_{\sim }}$

These definitions are independent of the choice of representatives of the equivalence classes.

Examples

Classic logic

The Lindenbaum algebra in classical logic is a Boolean algebra , as can be easily verified. Because the theorem of the excluded third holds in classical logic ( ), in Lindenbaum algebra the property is in particular for all elements ${\displaystyle p\lor \neg p=\top }$ ${\displaystyle a\in {\mathcal {L}}}$

${\displaystyle -a\cup a=1}$

Fulfills.

In predicate logic, the properties of quantifiers and equality are not reflected in the axioms of Boolean algebra. The cylinder algebra of Tarski is a generalization of Boolean algebra, the axioms for the existential and equality has.

Intuitionist logic

In the construction of Lindenbaum's algebra, formulas are equivalent that are demonstrably equivalent. This means that the rules of the system of evidence go into the definition. The principle of the excluded third applies in classical logic, but not in intuitionist logic (see e.g.). As a result, as Lindenbaum algebra in intuitionistic logic with the identical construction of the quotient algebra , we do not get a Boolean algebra as in classical logic, but a Heyting algebra .

Individual evidence

1. ^ A. Tarski: Fundamentals of the system calculus. First part . In: Fundam.Math . 25, 1935, pp. 503-526.
2. ^ WJ Blok, Don Pigozzi: Algebraizable logics . In: Memoirs of the AMS . 77, 1989 .; here: pages 1–2
3. ↑ M. Huth, M. Ryan: Logic in Computer Science: Modeling and Reasoning about Systems . 2nd Edition. Cambridge University Press, Cambridge 2004.
4. ^ D. van Dalen: Intuitionistic Logic . In: DM Gabbay, F. Guenthner (eds.): Handbook of Philosophical Logic . tape 5 . Springer, Dordrecht 2002, p. 1-114 .