线性可实现性与蕴含代数
Linear Realisability and Implicative Algebras
AI总结：
本文首次建立了线性可实现性模型与克里内和克里维内的可实现性构造之间的正式联系，通过米克尔框架提出对蕴含代数的线性分解。
摘要：
可实现性，由克里内引入，可以被理解为布劳威尔-海廷-科莫戈罗夫（BHK）证明解释的一种具体化，提供了一个将数学陈述和证明以构造性或计算内容来解释的框架。随着时间的推移，这一概念通过各种扩展不断发展，例如克里塞尔的修改可实现性或克里维内的经典可实现性。与此同时，吉拉德在线性逻辑中的工作引入了另一种视角，通常被视为BHK解释的另一种具体实现。所得到的构造，包括几何交互、 Ludics 和交互图等模型，最近被统一称为线性可实现性模型，以强调与直觉主义和经典可实现性的直观联系。本文首次建立了线性可实现性模型与克里内和克里维内的可实现性构造之间的正式联系。我们的方法利用米克尔的框架：正如线性逻辑可以被视为直觉主义和经典逻辑的分解，我们提出对蕴含代数的线性分解，并展示线性可实现性模型提供了此类分解的具体例子。
英文摘要：
Realizability, introduced by Kleene, can be understood as a concretization of the Brouwer-Heyting-Kolmogorov (BHK) interpretation of proofs, providing a framework to interpret mathematical statements and proofs in terms of their constructive or computational content. Over time, this concept has evolved through various extensions, such as Kreisel's modified realizability or Krivine's classical realizability. Parallel to these developments, Girard's work on linear logic introduced another perspective, often seen as another concrete realization of the BHK interpretation. The resulting constructions, encompassing models like geometry of interaction, ludics, and interaction graphs, were recently unified under the term linear realizability models to stress the intuitive connection with intuitionnistic and classical realizability. The present work establishes for the first time a formal link between linear realizability models and the realizability constructions of Kleene and Krivine. Our approach leverages Miquel's framework: just as linear logic can be viewed as a decomposition of intuitionistic and classical logic, we propose a linear decomposition of implicative algebras and show that linear realisability models provide concrete examples of such decompositions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
