AI 中文总结
研究关系量子模态逻辑中强制条件的结构及证明理论结果，通过证明模态后继集特性等，采用多结论序列局部有效性提供语义，构建典范模型，证明添加规则后的演算对三类框架可靠且完备来刻画其逻辑范围，建立组件模态证明理论。
AI 中文摘要
本文确定了关系量子模态逻辑中强制条件的结构和证明理论结果，即在一个世界可用的每个模态转换在与之兼容的每个世界也可用。我们证明模态后继集在兼容性组件上是恒定的，因此盒装真值集属于这些组件并集的布尔代数。同一组件中世界之间的关系为每个稳定命题分配其通过组件并集得到的最大下界和最小上界近似，在硬超选择模型中这些恰好是通过中心命题的近似。我们采用多结论序列的局部有效性为具有多个组件的框架上的模态排中律提供语义。通过添加一个点得到的连通化表明，组件框架、满足强制条件的等价框架以及具有通用模态可达性的连通兼容性框架对于单结论序列具有相同的逻辑。最后，极大一致对产生一个典范模型，并且通过添加T、4和B得到的演算对于这三类框架被证明是可靠且完备的。这些结果刻画了强制条件的逻辑范围并建立了组件模态的完备证明理论。
英文摘要
This paper determines the structural and proof-theoretic consequences of the forcing condition in relational quantum modal logic, under which every modal transition available at a world is also available at every world compatible with it. We prove that modal successor sets are constant on compatibility components, so boxed truth sets belong to the Boolean algebra of unions of these components. The relation holding exactly between worlds in the same component assigns to each stable proposition its greatest lower and least upper approximations by unions of components, and in hard superselection models these are exactly the approximations by central propositions. We adopt local validity for sequents with multiple conclusions to give a semantics for modal excluded middle on frames with several components. A connectedization obtained by adding one point then shows that component frames, equivalence frames satisfying the forcing condition, and connected compatibility frames with universal modal accessibility have the same logic for sequents with one conclusion. Finally, maximal consistent pairs yield a canonical model, and the calculus obtained by adding T, 4, and B is proved sound and complete for the three frame classes. These results characterize the logical scope of the forcing condition and establish a complete proof theory for component modalities.
