非偶然性逻辑的证明论

中文摘要 AI 辅助

非偶然性逻辑（$\KWL$）用表示一个命题必然为真或必然为假的算子替换了模态逻辑中通常的必然性算子。除了其内在的逻辑趣味外，它在认识论逻辑中可自然地解释为“知道是否”，在可证明性逻辑的算术解释下可解释为可判定性。尽管非偶然性逻辑的语义已被广泛研究，但其证明论仍相对欠发达。在本文中，我们为$\KWL$在广泛的框架条件类上发展了一个统一的证明论框架。我们的方法基于广义路径条件（GPCs），这是一种语法理论形式体系，能统一刻画许多标准模态框架性质。对于每个有限的GPC集合$\gpc$，我们构造一个相应的带标签的矢列演算。所有演算共享一组共同的逻辑规则，仅通过由$\gpc$生成的单一结构规则而不同，该规则捕捉了底层框架条件。我们证明这些演算相对于其相应的框架类是可靠且完备的，从而为一大类非偶然性逻辑提供了统一的证明论。

英文摘要

{Non-contingency logic $(\KWL)$ replaces the usual necessity operator of modal logic with an operator expressing that a proposition is necessarily true or necessarily false. Besides its intrinsic logical interest, it admits natural interpretations as knowing whether in epistemic logic and as decidability under the arithmetical interpretation of provability logic. Although the semantics of non-contingency logic have been extensively studied, its proof theory remains comparatively underdeveloped. In this paper, we develop a uniform proof-theoretic framework for $\KWL$ over a broad class of frame conditions. Our approach is based on generalized path conditions (GPCs), a grammar-theoretic formalism that uniformly captures many standard modal frame properties. For every finite set $\gpc$ of GPCs, we construct a corresponding labelled sequent calculus. All calculi share a common set of logical rules and differ only by a single structural rule generated from $\gpc$, which captures the underlying frame conditions. We prove that these calculi are sound and complete with respect to their corresponding frame classes, thereby providing a uniform proof theory for a large family of non-contingency logics.}

发表机构

• Institut für Informatik, Universität Bern（伯尔尼大学）
• Philosophy Department, Peking University（北京大学）

机构由 AI 辅助整理，请以论文原文为准。