In der mathematischen Logik ist die Lindenbaum-Algebra (auch Lindenbaum-Tarski-Algebra) zu einer Theorie T die Quotientenalgebra bezüglich der Äquivalenzrelation der beweisbar äquivalenten Sätze in T.

Die Algebra hat ihren Namen nach Adolf Lindenbaum. Alfred Tarski hat die Konstruktion der Algebra 1935 in[1] erstmals publiziert und gezeigt, dass sie eine Boolesche Algebra ist[2].

Konstruktion

Bearbeiten

Gegeben eine logische Theorie T und ein Beweissystem, wie etwa die natürliche Deduktion (siehe z. B.[3]), dann definiert man für Formeln p und q:

 .

Dass die Relation   reflexiv und symmetrisch ist, ergibt sich unmittelbar aus der Definition. Sie ist auch transitiv, denn aus Beweisen für   und   lässt sich mit den Regeln der Beseitigung der Implikation und der Einführung der Implikation ein Beweis für   in   konstruieren.

Wir bezeichnen nun mit   die Äquivalenzklasse von   bezüglich dieser Äquivalenzrelation. Die Elemente der Lindenbaum-Algebra   sind die Äquivalenzklassen und man definiert die Operationen der Algebra sowie zwei ausgezeichnete Elemente, das Null- und das Einselement, folgendermaßen:

 
 
 
 
 

Diese Definitionen sind unabhängig von der Wahl der Repräsentanten der Äquivalenzklassen.

Beispiele

Bearbeiten

Klassische Logik

Bearbeiten

Die Lindenbaum-Algebra in der klassischen Logik ist eine Boolesche Algebra, wie man leicht verifiziert. Weil der Satz vom ausgeschlossenen Dritten in der klassischen Logik ( ) gilt, ist in der Lindenbaum-Algebra für alle Elemente   insbesondere die Eigenschaft

 

erfüllt.

In der Prädikatenlogik spiegeln sich die Eigenschaften der Quantoren und der Gleichheit nicht in den Axiomen der Booleschen Algebra. Die Zylinderalgebra von Tarski ist eine Verallgemeinerung der Booleschen Algebra, die Axiome für den Existenzquantor und die Gleichheit hat.

Intuitionistische Logik

Bearbeiten

Bei der Konstruktion der Lindenbaum-Algebra sind Formeln äquivalent, die beweisbar äquivalent sind. Das bedeutet, dass die Regeln des Beweissystems in die Definition eingehen. In der klassischen Logik gilt der Satz des ausgeschlossenen Dritten, in der intuitionistischen Logik jedoch nicht (siehe z. B.[4]). Infolgedessen erhalten wir als Lindenbaum-Algebra in der intuitionistischen Logik mit der identischen Konstruktion der Quotientenalgebra keine Boolesche Algebra wie in der klassischen Logik, sondern eine Heyting-Algebra.

Einzelnachweise

Bearbeiten
  1. A. Tarski: Grundzüge des Systemenkalküls. Erster Teil. In: Fundam.Math. 25. Jahrgang, 1935, S. 503–526.
  2. W.J. Blok, Don Pigozzi: Algebraizable logics. In: Memoirs of the AMS. 77. Jahrgang, 1989 (iastate.edu).; hier: Seiten 1–2
  3. M. Huth, M. Ryan: Logic in Computer Science: Modelling and Reasoning about Systems. 2. Auflage. Cambridge University Press, Cambridge 2004.
  4. D. van Dalen: Intuitionistic Logic. In: D.M. Gabbay, F. Guenthner (Hrsg.): Handbook of Philosophical Logic. Band 5. Springer, Dordrecht 2002, S. 1–114.