"Algebra and Substructural Logics - take 4" (AsubL4) 初日

縮約規則とリソース保存性が対応することはよく知られていますが、線型論理に深く対応するように、リソース保存性の概念を導入したλ計算(およびリソースλ代数)の話。リソース-λ項の外延性が定理として証明できるとか、驚き。
S4が直観主義論理の modal companion*1 であるのはよく知られているので、その部分構造論理バージョンの話。S4FLがFLの modal companion であることを示した。
関連論理のイヤなところは、公理および推論規則の数がとにかく多いことで、推論規則十いくつのリストを見せられると困ります。
小野先生の講演は、distributive law を満たす residuated lattice を MacNeile完備化すると、distributive law が保存されないことがあるので、問題が起こらないやり方を探る話でした。完備化は、ファジイ論理にとって本質的な操作だけど、奥が深い。

*1:直観主義論理がAを証明することと、ハイティング代数上でAがvalidであることと、位相的ブール第数条でG(A)がvalidであることと、S4でG(A)が証明可能であることが同値になる