アフィン論理

アフィン論理は、証明理論が収縮の構造規則を否定する部分構造論理であり、弱められた線形論理として特徴付けることもできる。

「アフィン論理」という名前は線型論理に関連付けられており、弱化規則を許容する点で線型論理と異なります。 ジャン＝イヴ・ジラールは、線型論理を線型代数の観点から特徴付ける線型論理の相互作用意味論の幾何学の一部としてこの名前を導入しました。ここで彼はベクトル空間上のアフィン変換に言及しています。^[1]

アフィン論理は線型論理に先行していた。VNグリシンは1974年にこの論理を使用した。^[2]ラッセルのパラドックスは、無制限の理解公理があっても、縮約なしに集合論では導出できないことに気づいた後である。^[3] 同様に、この論理は「直接論理」と呼ばれる述語論理の決定可能なサブ理論の基礎を形成した（Ketonen & Wehrauch、1984年、Ketonen & Bellin、1989年）。

アフィン論理は、アフィン矢印を線形矢印として書き換えることで線形論理に埋め込むことができます。 ${\displaystyle A\rightarrow B}$${\displaystyle A\multimap B\otimes \top }$

完全な線形論理 (つまり、乗法、加法、指数を含む命題線形論理) は決定不可能ですが、完全なアフィン論理は決定可能です。

アフィン論理は、 ludicsの基礎を形成します。

• VN Grishin、1974年。「非標準論理と集合論へのその応用」（ロシア語）。形式化言語と非古典論理の研究（ロシア語）、135-171。Izdat、「Nauka」、モスクワ。
• 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 年。「決定手順の再考: 直接論理に関する注記」『線形論理とその実装』。

• 関連するロジック
• アフィン型システム、サブ構造型システム