Álgebra de Lindenbaum-Tarski

En lógica matemática, el álgebra de Lindenbaum-Tarski (también conocida como álgebra de Lindenbaum) de una teoría lógica T consiste en las clases de equivalencia de sentencias de la teoría (es decir, el cociente, bajo la relación de equivalencia ~ definida de tal manera que p ~ q exactamente cuando p y q son probablemente equivalentes en T ). Es decir, dos oraciones son equivalentes si la teoría T prueba que cada una implica a la otra. El álgebra de Lindenbaum-Tarski es, pues, el álgebra del cociente obtenida al factorizar el álgebra de fórmulas por esta relación de congruencia.

El álgebra lleva el nombre de los lógicos Adolf Lindenbaum y Alfred Tarski. Fue introducido por primera vez por Tarski en 1935​ como un dispositivo para establecer la correspondencia entre la lógica proposicional clásica y las álgebras booleanas. El álgebra de Lindenbaum-Tarski se considera el origen de la lógica algebraica moderna.​

Operaciones

Las operaciones en un álgebra A de Lindenbaum-Tarski se heredan de las de la teoría subyacente T. Estos típicamente incluyen conjunción y disyunción, que están bien definidas en las clases de equivalencia. Cuando la negación también está presente en T, entonces A es un álgebra booleana, siempre que la lógica sea clásica. Si la teoría T consiste en las tautologías proposicionales, el álgebra de Lindenbaum-Tarski es el álgebra booleana libre generada por las variables proposicionales.

Álgebras relacionadas

Las álgebras de Heyting y las álgebras interiores son las álgebras de Lindenbaum-Tarski para la lógica intuicionista y la lógica modal S4, respectivamente.

Una lógica para la que es aplicable el método de Tarski se llama algebraizable. Sin embargo, hay una serie de lógicas en las que este no es el caso, por ejemplo, las lógicas modales S1, S2 o S3, que carecen de la regla de necesidad (⊢φ implica ⊢□φ), por lo que ~ no es un congruencia (porque ⊢φ→ψ no implica ⊢□φ→□ψ). Otro tipo de lógica donde el método de Tarski no es aplicable es la lógica relevante, porque dados dos teoremas, una implicación de uno a otro puede no ser en sí misma un teorema en una lógica de relevancia.​ El estudio del proceso de algebraización (y noción) como tema de interés por sí mismo, no necesariamente por el método de Tarski, ha llevado al desarrollo de la lógica algebraica abstracta.