Àlgebra de Lindenbaum-Tarski

En llògica matemàtica, el àlgebra de Lindenbaum-Tarski (també coneguda com a àlgebra de Lindenbaum) d'una teoria llògica T consistix en les classes d'equivalència de sentències de la teoria (és dir, el cocient, baixe la relació d'equivalència definida de tal manera que p q exactament quan p i q són provablement equivalents en T ). És dir, dos oracions són equivalents si la teoria T prova que cada una implica a l'atra. L'àlgebra de Lindenbaum-Tarski és, puix, l'àlgebra del cocient obtinguda al factorizar l'àlgebra de fòrmules per esta relació de congruència.

L'àlgebra du el nom dels llògics Adolf Lindenbaum i Alfred Tarski. Va ser introduït per primera volta per Tarski en 1935 com un dispositiu per a establir la correspondència entre la llògica proposicional clàssica i les àlgebra booleanas. L'àlgebra de Lindenbaum-Tarski es considera l'orige de la llògica algebraica moderna.

Operacions

Les operacions en un àlgebra A de Lindenbaum-Tarski s'hereten de les de la teoria subjacent T. Estos típicament inclouen conjunció i disjunció, que estan ben definides en les classes d'equivalència. Quan la negació també està present en T, llavors A és un àlgebra booleana, sempre que la llògica siga clàssica. Si la teoria T consistix en les tautologia proposicionals, l'àlgebra de Lindenbaum-Tarski és l'àlgebra booleana lliure generada per les variables proposicionals.

Àlgebra relacionades

Les àlgebra de Heyting i les àlgebra interiors són les àlgebra de Lindenbaum-Tarski per a la llògica intuicionista i la llògica modal S4, respectivament.

Una llògica per a la que és aplicable el método de Tarski es diu algebraisable. No obstant, hi ha una série de llògiques en les que este no és el cas, per eixemple, les llògiques modals S1, S2 o S3, que carixen de la regla de necessitat (⊢φ implica ⊢□φ), per lo que no és un congruència (perque ⊢φ→ψ no implica ⊢□φ→□ψ). Un atre tipo de llògica a on el método de Tarski no és aplicable és la llògica rellevant, perque donats dos teoremes, una implicació d'un a un atre pugues no ser en sí mateixa una teorema en una llògica de rellevància. L'estudi del procés de algebraización (i noció) com a tema d'interés per sí mateixa, no necessàriament pel método de Tarski, ha dut al desenroll de la llògica algebraica abstracta.