直觉主义动态逻辑
Intuitionistic Dynamic Logic
浏览论文内容
中文总结 AI 辅助
研究直觉主义动态逻辑的数学理论，涵盖五种该逻辑。通过开发证明论工具、进行语义研究，建立相关性质与界限。主要贡献为开发演算、获有限模型性质及可判定性、给出直觉主义线性时态逻辑完备公理系统。
中文摘要 AI 辅助
本文发展了直觉主义动态逻辑的数学理论，它是直觉主义命题逻辑通过模态和定点算子的扩展。此类系统为关于变化的推理提供形式工具，比如数学系统随时间演变或主体信息更新后的知识状态。我们研究了五种直觉主义动态逻辑：直觉主义主模态、直觉主义公共知识逻辑、直觉主义线性时态逻辑、双直觉主义模态逻辑和双直觉主义线性时态逻辑。在证明论方面，我们开发了合理且完备的希尔伯特式公理系统以及非良基和循环相继式演算。在语义方面，我们在各类动态模型上研究这些逻辑，这些模型是满足合流性和框架条件的双关系克里普克模型。我们建立了表达能力结果、有限模型性质、可判定性以及复杂度界限。主要贡献有三方面。首先，我们为直觉主义主模态和公共知识逻辑开发了分析性循环相继式演算，通过稳健的证明搜索论证获得完备性。其次，通过对动态模型的复杂组合分析，我们为双直觉主义模态逻辑获得了有限模型性质和可判定性。第三，我们为具有时态算子“下一个”“最终”和“从此以后”的直觉主义线性时态逻辑开发了合理且完备的公理系统，从而为关于有限公理系统存在性的长期开放问题提供了肯定答案。
英文摘要
This thesis develops the mathematical theory of intuitionistic dynamic logics - extensions of intuitionistic propositional logic with modalities and fixed point operators. Such systems provide formal tools for reasoning about change, such as encountered in mathematical systems evolving over time or in the knowledge state of an agent after an information update. We investigate five intuitionistic dynamic logics: intuitionistic master modality, intuitionistic common knowledge logic, intuitionistic linear temporal logic, bi-intuitionistic modal logic and bi-intuitionistic linear temporal logic. On the proof theoretic side we develop sound and complete Hilbert-style axiomatizations as well as non-wellfounded and cyclic sequent calculi. On the semantic side we study these logics over various classes of dynamic models, which are birelational Kripke models satisfying confluence and frame conditions. We establish expressivity results, the finite model property, decidability, as well as complexity bounds. The main contributions are threefold. First, we develop analytic cyclic sequent calculi for intuitionistic master modality and common knowledge logic, where completeness is obtained by a robust proof search argument. Second, we obtain the finite model property and decidability for bi-intuitionistic modal logic via an intricate combinatorial analysis of dynamic models. Third, we develop a sound and complete axiomatization for intuitionistic linear temporal logic featuring the temporal operators next, eventually and henceforth, thereby providing a positive answer to the long-standing open question concerning the existence of a finite axiomatization.
