Riesz空间与模态Riesz空间的证明论
Proof Theory of Riesz Spaces and Modal Riesz Spaces
AI总结：
本文为Riesz空间和模态Riesz空间设计超序列演算证明系统，证明可靠性、完备性和切割消去，并首次证明模态Riesz空间理论的可判定性，应用于概率程序逻辑。
摘要：
我们为Riesz空间和模态Riesz空间的理论设计了超序列演算证明系统，并证明了关键定理：可靠性、完备性和切割消去。这些定理随后被用于获得关于这两个理论的一些有趣结果的完全语法证明。最值得注意的是，我们证明了一个新颖的结果：模态Riesz空间的理论是可判定的。这项工作在概率程序逻辑领域有应用，因为模态Riesz空间为概率μ-演算所基于的Riesz模态逻辑提供了代数语义。
英文摘要：
We design hypersequent calculus proof systems for the theories of Riesz spaces and modal Riesz spaces and prove the key theorems: soundness, completeness and cut elimination. These are then used to obtain completely syntactic proofs of some interesting results concerning the two theories. Most notably, we prove a novel result: the theory of modal Riesz spaces is decidable. This work has applications in the field of logics of probabilistic programs since modal Riesz spaces provide the algebraic semantics of the Riesz modal logic underlying the probabilistic mu-calculus.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
