リンデンバウム・タルスキー代数

数理論理学において、論理理論Tのリンデンバウム・タルスキ代数(またはリンデンバウム代数)は、同値関係~の下での理論の同値類(すなわち)から構成されます。この同値類は、 pqがTにおいて証明可能に同値であるときに、p ~ qとなるように定義されます。つまり、理論T が、ある文が他の文を含意していることを証明する場合、2つの文は同値です。したがって、リンデンバウム・タルスキ代数は、この合同関係によって式の代数を因数分解することによって得られる商代数です。

この代数は、論理学者アドルフ・リンデンバウムアルフレッド・タルスキにちなんで名付けられました。1926年から1927年にかけて、リンデンバウムはヤン・ウカシェヴィチの数理論理学セミナーで独自の手法を開発し、[ 1 ] [ 2 ]、その後数十年にわたりタルスキの研究を通じて普及・一般化されました。[ 3 ]

リンデンバウム・タルスキー代数は現代代数論理の起源と考えられている。[ 4 ]

オペレーション

リンデンバウム・タルスキ代数Aにおける演算は、基礎理論Tにおける演算から継承される。これらには典型的には、同値類上で明確に定義されている連言選言が含まれる。 Tに否定も存在する場合、論理が古典的である限り、 Aはブール代数となる。理論Tが命題トートロジーで構成される場合、リンデンバウム・タルスキ代数は命題変数によって生成される自由ブール代数となる。

Tが演繹に対して閉じている場合、 T/~のAへの埋め込みはフィルタである。さらに、 A のウルトラフィルタは完全な無矛盾理論に対応し、リンデンバウムの補題ウルトラフィルタの補題の同値性を確立する。

ハイティング代数内部代数は、それぞれ直観論理様相論理S4のリンデンバウム-タルスキー代数です。

タルスキ法が適用できる論理は代数化可能と呼ばれる。しかし、そうでない論理も数多く存在する。例えば様相論理S1S2S3は必然性の規則(⊢φ は ⊢□φ を意味する)を欠いており、したがって ~ (上で定義)は合同ではない(⊢φ→ψ は ⊢□φ→□ψ を意味しないため)。タルスキ法が適用できない別の種類の論理は関連性論理である。なぜなら、2つの定理がある場合、一方から他方への含意自体は関連性論理の定理ではない可能性があるからである。[ 4 ]代数化プロセス(および概念)の研究自体が、必ずしもタルスキ法によってではなく、興味深いトピックとして抽象代数論理の発展につながった。

参照

参考文献

  1. ^ SJ Surma (1982). 「リンデンバウム代数概念の起源とその後の応用について」.論理学、方法論、科学哲学VI, 第6回国際論理学、方法論、科学哲学会議議事録. 論理学と数学の基礎研究. 第104巻. pp.  719– 734. doi : 10.1016/S0049-237X(09)70230-7 . ISBN 978-0-444-85423-0
  2. ^ Jan Woleński. 「アドルフ・リンデンバウム」 .インターネット哲学百科事典.
  3. ^ A. Tarski (1983). J. Corcoran (編). Logic, Semantics, and Metamathematics — Papers from 1923 to 1938 — Trans. JH Woodger (第2版). Hackett Pub. Co.
  4. ^ a b W.J. Blok , Don Pigozzi (1989). 「代数化可能な論理」 AMS紀要77 ( 396).; こちら: 1-2ページ
  • ヒンマン、P. (2005). 『数理論理学の基礎』 AKピーターズ. ISBN 1-56881-262-0