アフィン論理は、証明理論によって縮約の構造規則が否定される部分構造論理である。また、弱化を伴う線型論理としても特徴付けられる。
「アフィン論理」という名称は線型論理と関連付けられており、弱化規則を許容する点で線型論理とは異なる。 ジャン＝イヴ・ジラールは、線型論理を線型代数の観点から特徴付ける相互作用意味論の幾何学の一部としてこの名称を導入した。ここで彼はベクトル空間上のアフィン変換に言及している。[1]
アフィン論理は線形論理に先行していた。VNグリシンは1974年にこの論理を用いた。[2]ラッセルのパラドックスは、無制限の理解公理を用いても、縮約なしに集合論では導出できないことを観察した後である。[3] 同様に、この論理は「直接論理」と呼ばれる述語論理の決定可能なサブ理論の基礎を形成した（Ketonen & Wehrauch, 1984; Ketonen & Bellin, 1989）。
アフィン論理は、アフィン矢印を線形矢印として書き換えることで線形論理に埋め込むことができます。
完全な線形論理 (つまり、乗法、加法、指数を含む命題線形論理) は決定不可能ですが、完全なアフィン論理は決定可能です。
アフィン論理は、ゲーム理論の基礎を形成します。
注記
- ^ Jean-Yves Girard , 1997. 「アフィン」。TYPESメーリングリストへのメッセージ。
- ^ Grishin、1974年、その後、Grishin、1981年。
- ^ フレデリック・フィッチの実証的に整合した集合論を参照
参考文献
- VNグリシン, 1974.「非標準論理とその集合論への応用」（ロシア語）. 『形式化言語と非古典論理の研究』（ロシア語）, 135–171. イズダート「ナウカ」, モスクワ.
- VN Grishin、1981 年。「短縮ルールを使用しない論理に基づく述語および集合論的計算」（ロシア語）。イズベスティア アカデミイ ナウク SSSR セリヤ マテマチェスカヤ 45(1):47-68。 239. 数学。 USSR Izv.、18、no.1、モスクワ。
- J. KetonenとR. Weyhrauch, 1984, 「述語計算の決定可能な断片」理論計算機科学32:297-307.
- J. KetonenとG. Bellin、1989年。「決定手続きの再考：直接論理に関するノート」『線形論理とその実装』所収。
参照
