四值图模型用于冲突解决：核心框架及Lean 4中的机器检查形式化
A Four-Valued Graph Model for Conflict Resolution: Core Framework and a Machine-Checked Formalization in Lean 4
- Institute of Science Tokyo（东京科学大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文提出四值图模型QCW-GMCR，结合Belnap逻辑处理冲突解决中的认知模糊性，并给出Lean 4形式化验证，涵盖分级可达性、规范归约及避免灾难的均衡概念。
AI中文摘要：
本笔记整合了准封闭世界冲突解决图模型（QCW-GMCR）的核心内容，该模型将标准冲突解决图模型与Belnap的四值逻辑相结合，以表示选项层面的认知模糊性，并将该框架与机器检查的Lean 4形式化配对。QCW-GMCR结合了：（1）四值选项赋值与到状态层面可行性的组合传播；（2）基于FDE启发的转移-保证语义的分级可达性（确定的、可信的、可能的），其中确定可达性与布尔片段中的FDE推论相关；（3）从四值评估到二元决策的公理化确定性归约，包括反映不同风险态度的四个规范算子；以及（4）具有准封闭世界安全不变量的避免灾难的均衡概念。四值超博弈扩展捕捉了决策者之间的异质主观评估。我们陈述了核心定义和结果，并报告了在Lean 4及mathlib中验证的部分，包括经典GMCR稳定性层次、四值合取的代数与组合性质、规范归约的性质以及分级可达性层次。该形式化还帮助识别并纠正了早期主张，包括用真值单调性替换知识单调性公理。本预印本为框架及其当前形式验证状态提供了稳定、可引用的记录。
英文摘要：
This note consolidates the core of the Quasi-Closed World Graph Model for Conflict Resolution (QCW-GMCR), which extends the standard Graph Model for Conflict Resolution with Belnap's four-valued logic to represent option-level epistemic ambiguity, and pairs the framework with a machine-checked Lean 4 formalization. QCW-GMCR combines: (1) FOUR-valued option assignments with compositional propagation to state-level feasibility; (2) graded reachability (definite, credible, possible) based on an FDE-inspired transition-warrant semantics, with definite reachability related to FDE consequence in the Boolean fragment; (3) axiomatized deterministic reductions from four-valued assessments to binary decisions, including four canonical operators reflecting distinct risk attitudes; and (4) catastrophe-avoiding equilibrium concepts with a quasi-closed-world safety invariant. A four-valued hypergame extension captures heterogeneous subjective assessments across decision makers. We state the core definitions and results and report the parts verified in Lean 4 with mathlib, including the classical GMCR stability hierarchy, algebraic and compositional properties of FOUR-valued conjunction, properties of the canonical reductions, and the graded reachability hierarchy. The formalization also helped identify and correct earlier claims, including a knowledge-monotonicity axiom replaced by truth monotonicity. This preprint provides a stable, citable record of the framework and its current formal verification status.
