Álgebra de Lindenbaum-Tarski


En lógica matemática , el álgebra de Lindenbaum-Tarski (o álgebra de Lindenbaum ) de una teoría lógica T consiste en las clases de equivalencia de oraciones 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, por lo tanto, el álgebra del cocienteobtenido 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 [1] como un dispositivo para establecer la correspondencia entre el cálculo proposicional clásico y las álgebras booleanas . El álgebra de Lindenbaum-Tarski se considera el origen de la lógica algebraica moderna . [2]

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 .

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 ~ (definido anteriormente) 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 de relevancia , 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. [2]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 .