乘法指数线性逻辑的关系模型是单射的(无弱化)
The relational model is injective for Multiplicative Exponential Linear Logic (without weakenings)
摘要:
我们证明了对于乘法指数线性逻辑(无弱化),割消法所引起的证明的句法等价关系与基于多集的关系模型所引起的证明的语义等价关系一致:一个是说模型(或语义)中的解释是单射的.我们实际上证明了一个更强的结果:两个无割证明的完整的乘法和指数片段的线性逻辑,其解释一致的多集为基础的关系模型是相同的“指数盒的门之间的连接”。
英文摘要:
We show that for Multiplicative Exponential Linear Logic (without weakenings) the syntactical equivalence relation on proofs induced by cut-elimination coincides with the semantic equivalence relation on proofs induced by the multiset based relational model: one says that the interpretation in the model (or the semantics) is injective. We actually prove a stronger result: two cut-free proofs of the full multiplicative and exponential fragment of linear logic whose interpretations coincide in the multiset based relational model are the same "up to the connections between the doors of exponential boxes".
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。