Proof Theory for Non-Contingency Logic
Abstract
{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.}
Related
- Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents
- An elementary proof of rational injectivity in equivariant KK-theory
- Studying proof data with proof theory: the case of AI-generated mathematics
- Proof of Universality of the Operator Dχ in ZEBTS Theory: From Spectral Ontology to the Law of Unity of the Triune Substance
- ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization
BibTeX
@misc{wang2026proof,
title = {{Proof Theory for Non-Contingency Logic}},
author = {Yunsong Wang and Lukas Zenger},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.38975},
eprint = {2609.38975},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.38975},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Proof Theory for Non-Contingency Logic
AU - Yunsong Wang
AU - Lukas Zenger
PY - 2026
DA - 2026/09/30
PB - arXiv
DO - 10.48550/arxiv.2609.38975
UR - https://arxiv.org/abs/2609.38975
AB - {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.}
ER -