Loading article…
多項式代数（最近ではハルモス代数とも呼ばれる）は、ポール・ハルモスによって導入された代数構造であり、一階述語論理を研究するために設計されたものである。多項式代数は、代数論理において一階述語論理の構文とモデル理論を研究するために用いられる主要な代数的枠組みの一つである。
多項式代数と一階述語論理の関係は、ブール代数と命題論理の関係に類似している（リンデンバウム・タルスキー代数を参照）。一階述語論理と代数を関連付ける他の方法としては、タルスキーの円筒代数[ 1 ]（等号が論理の一部である場合）やローヴェアの関数意味論（圏論的アプローチ） [ 2 ]などがある。
多項式代数は、1950年代にポール・ハルモスによって代数論理のプログラムの一部として導入されました。このプログラムの目的は、論理体系の代数的対応物を提供することでした。一階述語論理と代数を関連付ける別のアプローチは、圏論的論理とローヴェアの関数的意味論によって提供されています。[ 2 ] [ 3 ]これらは、アルフレッド・タルスキとその共同研究者によって以前に導入された円筒代数 の代替として開発されました。多項式代数は、一階述語論理における量化子と置換の挙動を反映する代数形式を提供します。この理論は、ヘンキン、モンク、タルスキによる代数論理の研究でさらに発展しました。[ 4 ]
次元の多項式代数は、変数の置換と存在量化に対応する演算を備えたブール代数であり、基数を持つ変数の集合によってインデックス付けされます。置換演算は変数集合の変換に対応し、量化子演算は個々の変数に対する存在量化に対応する。より正確には、ブール演算に加えて、多項式代数には以下が含まれる。
これらの演算は、一階述語論理における置換と量化子の代数的挙動を反映する公理を満たす。
多項式代数の公理は、ブール演算、置換、および量化子間の相互作用を記述する。基本的な原理には、以下のものがある。
これらの公理は、変数の置換と存在量化の下で論理式が満たす代数的性質を捉えている。詳細な公理化はハルモスのモノグラフに記載されている。[ 3 ]
表現定理は、多項式代数が、関係と数列上の関数を用いて演算が定義される集合の代数として表現できることを示している。ハルモスは、局所的に有限な多項式代数と無限次元の多項式代数の両方について表現定理を証明した。[ 3 ] ダイニョーとモンクによる別の表現定理は、一般的な多項式代数の表現結果を確立している。[ 5 ] 多項式代数および関連する代数の表現理論のさらなる発展は、代数論理に関する後の文献で議論されている。[ 6 ] [ 7 ]これらの表現定理は、抽象的な代数構造と一階述語論理の意味論との間の橋渡しを確立する。
多項式代数の自然な例は、論理学から生じる。
無限一階言語の場合、論理的同値性を法とする式のリンデンバウム・タルスキー代数には、変数の置換と存在量化によって誘導される演算を装備することができる。これらの演算により、多項式代数が形成される。このような代数は、式の論理構造の代数的表現を提供する。 [ 8 ]
準多項代数は、置換演算のシステムが制限された多項代数の変種です。多項代数では、変数の集合の任意の変換に対応する置換が可能ですが、準多項代数では、有限個のサポートを持つ置換（通常は有限個の置換または変数の有限個の変換）のみが基本演算に含まれます。多くの解説では、準多項代数という用語は準多項等式代数を指します。これらの代数は、多項代数の特徴である置換メカニズムの一部を保持しつつ、円筒代数により密接に関連する構造として、代数論理の発展の中で導入されました。準多項代数は、円筒代数と完全な多項代数の中間クラスを形成し、等号に対応する特別な対角要素をさらに含んでいます。これらの構造は、等号を含む一階述語論理の代数的研究において重要な役割を果たします。多項式代数の場合と同様に、準多項式代数の演算は、一階述語論理の式に対する論理演算をモデル化することを目的としており、ブール演算は命題結合子に対応し、円筒化演算は存在量化に対応し、置換演算は変数の置換を表します。
準多項式代数および関連する円筒状代数の理論は、代数論理に関する文献で広く展開されてきた。 [ 9 ] [ 10 ] [ 6 ] [ 7 ] このような代数は、論理式の論理構造の代数的表現を提供する。表現結果によると、準多項式代数は相対化された設定において円筒状代数よりも強い表現特性を持つ。 [ 11 ] [ 12 ] 準多項式代数および関連する円筒状代数は、代数論理の現代研究において引き続き重要な役割を果たしている。
多項式代数は円筒代数と密接に関連しています。どちらの構造も一階述語論理のための代数的枠組みを提供します。多項式代数は円筒代数と密接に関連しており、円筒代数に対応する構造を特殊な場合として含みますが、置換と量化子の扱い方が異なります。円筒代数は量化子に対応する円筒化演算を重視しますが、多項式代数はより豊富な置換演算体系を取り入れています。これらの代数体系間の関係は、代数論理理論の重要な部分を形成します。
