数理論理学において、論理理論Tのリンデンバウム・タルスキ代数(またはリンデンバウム代数)は、同値関係~の下での理論の文の同値類(すなわち商)から構成されます。この同値類は、 pとqがTにおいて証明可能に同値であるときに、p ~ qとなるように定義されます。つまり、理論T が、ある文が他の文を含意していることを証明する場合、2つの文は同値です。したがって、リンデンバウム・タルスキ代数は、この合同関係によって式の代数を因数分解することによって得られる商代数です。
この代数は、論理学者アドルフ・リンデンバウムとアルフレッド・タルスキにちなんで名付けられました。1926年から1927年にかけて、リンデンバウムはヤン・ウカシェヴィチの数理論理学セミナーで独自の手法を開発し、[ 1 ] [ 2 ]、その後数十年にわたりタルスキの研究を通じて普及・一般化されました。[ 3 ]
リンデンバウム・タルスキー代数は現代代数論理の起源と考えられている。[ 4 ]
リンデンバウム・タルスキ代数Aにおける演算は、基礎理論Tにおける演算から継承される。これらには典型的には、同値類上で明確に定義されている連言と選言が含まれる。 Tに否定も存在する場合、論理が古典的である限り、 Aはブール代数となる。理論Tが命題トートロジーで構成される場合、リンデンバウム・タルスキ代数は命題変数によって生成される自由ブール代数となる。
Tが演繹に対して閉じている場合、 T/~のAへの埋め込みはフィルタである。さらに、 A のウルトラフィルタは完全な無矛盾理論に対応し、リンデンバウムの補題とウルトラフィルタの補題の同値性を確立する。
ハイティング代数と内部代数は、それぞれ直観論理と様相論理S4のリンデンバウム-タルスキー代数です。
タルスキ法が適用できる論理は代数化可能と呼ばれる。しかし、そうでない論理も数多く存在する。例えば様相論理S1、S2、S3は必然性の規則(⊢φ は ⊢□φ を意味する)を欠いており、したがって ~ (上で定義)は合同ではない(⊢φ→ψ は ⊢□φ→□ψ を意味しないため)。タルスキ法が適用できない別の種類の論理は関連性論理である。なぜなら、2つの定理がある場合、一方から他方への含意自体は関連性論理の定理ではない可能性があるからである。[ 4 ]代数化プロセス(および概念)の研究自体が、必ずしもタルスキ法によってではなく、興味深いトピックとして抽象代数論理の発展につながった。