Source-linked AI summary
A Four-Valued Graph Model for Conflict Resolution: Core Framework and a Machine-Checked Formalization in Lean 4
Yukiko Kato
TL;DR
Binary GMCR cannot distinguish a decision maker’s negative verdict from a lack of knowledge, a distinction relevant to grave decisions without reliable probabilities. QCW-GMCR combines four-valued option assessments with graded reachability, deterministic reductions, and catastrophe-avoiding equilibria, alongside a Lean 4 formalization. The note reports the formalization’s status and corrections to earlier claims, while identifying open questions and remaining work.
Problem
Binary GMCR cannot represent incomplete or contradictory information about options, collapsing “will not act” and “do not know whether [a decision maker] will act.”
Source: §1 · p. 1Method
QCW-GMCR extends GMCR with Belnap four-valued option status, an FDE-inspired transition-warrant operation, deterministic reductions to binary decisions, and catastrophe-avoiding equilibria.
Source: §1 · p. 2, §4 · pp. 4–5, §5.1 · p. 7Results
The note reports the formalization’s current status and corrections to reduction-operator monotonicity and reachability definitions, as well as corrected FDE and GMCR-recovery characterizations.
Source: §11 · pp. 14–15Takeaways & Limitations
At stability level U, a state remains stable even when decision makers reason optimistically about capabilities.
Source: §6 · p. 9The weakest epistemic-divergence conditions for hypergame equilibrium existence remain open, and graded reachability omits definite option deselections absent a definite-warrant hypothesis.
Source: §5.2 · p. 9, §8 · p. 11
Abstract
from arXiv · showhide
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.
1 Introduction
QCW-GMCR addresses the limits of binary GMCR when information is incomplete or contradictory, especially for grave decisions without reliable probabilities. It extends option-level four-valued reasoning into reachability, reductions, and safe equilibria, and documents a machine-checked Lean 4 formalization.
1 Introduction
- Binary GMCR collapses “B will not act” and “we do not know whether B will act,” although that distinction matters for rational choice.Standard GMCR assigns each option, state, and transition a binary status.Source: §1 · pp. 1–2
- For grave, irreversible decisions without defensible probabilities, QCW-GMCR represents epistemic status as Y, N, YN, or U rather than a numerical uncertainty degree.These values encode positive grounds, negative grounds, both, or neither.Source: §1 · p. 2
- Relative to Kato (2022), which introduced a state-level definition, this framework adds option-level composition, entailment-based graded reachability, constrained reductions, safe equilibria, and a safety invariant.The machine-checked formalization is also new to this note.Source: §1 · p. 2
- QCW-GMCR distinguishes option-status ambiguity from uncertainty about preferences, subjective games, or awareness of which options exist.U concerns an option represented in a decision maker’s subjective model; structural unawareness concerns options absent from that model.Source: §1 · p. 2
- The note presents the framework’s core definitions and safety guarantees and reports which results are machine-checked in Lean 4 with mathlib and which remain informal.The authors connect formal verification to the framework’s aim of safety under epistemic ambiguity.Source: §1 · p. 2
2 Preliminaries
The preliminaries define the graph structure and stability concepts used by GMCR, then introduce Belnap’s four-valued logic and its truth and knowledge orders. They also state the classical stability hierarchy verified in Lean and the algebraic properties of conjunction used later.
2.1 Standard GMCR
- GMCR represents finite decision makers, states, unilateral moves, and strict preferences; preferences may be complete without being transitive.Indifference is the absence of strict preference in either direction, and identity moves may be allowed.Source: §2.1 · p. 3
- Nash stability excludes unilateral improvements; GMR, SMR, and SEQ add opponent sanctions, with SMR blocking escape and SEQ requiring improving sanctions.A state stable for all decision makers under a concept is an equilibrium of that concept.Source: §2.1 · p. 3
- Lean verifies Nash ⊆ SMR ⊆ GMR and Nash ⊆ SEQ ⊆ GMR without assuming completeness or transitivity of preferences.The standard complete, possibly intransitive GMCR preferences are included.Source: §2.1 · p. 3
2.2 Belnap’s four-valued logic
- Belnap’s truth space FOUR comprises Y, N, YN, and U, ordered separately by truth and by knowledge.In the truth order, N is below U and YN, which are incomparable; both are below Y. In the knowledge order, U is below N and YN.Source: §2.2 · p. 3
- Conjunction is the meet in the truth order, and its verified algebra includes commutativity, associativity, idempotence, and YN ∧ U = N.N is absorbing and Y is the identity for conjunction.Source: §2.2 · pp. 3–4, Table 1 · p. 4
3 Option-Level Epistemic Foundations
QCW-GMCR assigns each represented option a four-valued epistemic status and composes those assignments into state-level feasibility. Under the default conjunction, the resulting state status follows from its constituent option statuses, preserving traceability of ambiguity.
3 Option-Level Epistemic Foundations
- Each represented option receives Y, N, YN, or U, and a state is a complete assignment over options, giving 4^|O| open-world states rather than 2^|O|.The values indicate definitely selected, definitely not, contradictory evidence, or unknown.Source: §3 · p. 4
- Default conjunctive composition maps option assignments to state feasibility: any N forces N, all Y gives Y, and the stated homogeneous YN and U cases yield YN and U respectively.A mixture of YN and U yields N under conjunction.Source: §3 · p. 4
- State-level ambiguity inherits from option-level uncertainty, allowing analysts to trace its sources; option-dependence constraints can be evaluated four-valuedly and conjoined with feasibility.Examples of such constraints include mutual exclusivity and implication.Source: §3 · p. 4
4 Entailment-Based Reachability
The section grades transitions with an FDE-inspired four-valued warrant operation rather than treating reachability as all-or-nothing. It relates definite moves to FDE consequence in the Boolean fragment and shows that path warrant cannot increase through concatenation.
4 Entailment-Based Reachability
- A move’s warrant is the conjunction of the transition-warrant values for its changed options; the operation is FDE-inspired, not a primitive FDE conditional.The connective’s rows represent pre-values and its columns post-values.Source: §4 · pp. 4–5, Table 2 · p. 5
- Definite, credible, and possible reachability admit warrants from DY = {Y}, DYN = {Y, YN}, and DU = {Y, YN, U}, respectively.The nested warrant sets establish the hierarchy; comparing warrants by truth order would not do so.Source: §4 · p. 5
- FDE consequence between complete state descriptions does not characterize moves: it holds only when the states are identical.The natural conjecture equating Boolean-state moves with consequence between full state formulas is false.Source: §4 · p. 6
- For Boolean unilateral moves, definite reachability aligns with FDE consequence over positive commitments: a move may add them but cannot retract them.A transition from Y to N on a changed option blocks definite warrant.Source: §4 · p. 6
- Concatenating a path cannot increase its entailment warrant because each added transition contributes another conjunct.A path is no more secure than its weakest constituent warrant.Source: §4 · p. 6
5 Quasi-Closed World Architecture
QCW-GMCR transforms ambiguity-rich assessments into a safety-preserving quasi-closed world through four layers. It combines deterministic reductions with structural exclusion of catastrophic states.
5 Quasi-Closed World Architecture
- The architecture moves from an open world toward a safety-preserving quasi-closed world through four layers.The supplied passages identify the layers as an architecture but do not specify all four layer contents.Source: §5 · p. 7
5.1 Reduction operators
- Reduction operators preserve definite Y and N assessments while resolving ambiguous FOUR values into binary feasibility decisions.Four canonical operators exhaust the classical-extension deterministic reductions and encode distinct risk attitudes.Source: §5.1 · pp. 7–8
- Truth monotonicity is the admissibility condition: all four canonical operators satisfy it, whereas knowledge monotonicity would exclude contradiction-cautious decisions.The Lean formalization refuted the earlier knowledge-monotonicity requirement; only δprec among the canonical operators is knowledge-monotone.Source: §5.1 · pp. 7–8
5.2 Catastrophe exclusion and the safety invariant
- The forbidden set F and its one-move boundary B are removed from the reduced state space to define the quasi-closed space.The boundary contains non-forbidden reduced states with a unilateral move into F.Source: §5.2 · p. 8
- Restricting admissible paths to the quasi-closed space makes forbidden states unreachable, a path-level guarantee beyond stability of resting points.The structural barrier complements preference-based deterrence; defense in depth also includes an entailment barrier when every transition into F has E = N.Source: §5.2 · p. 8
- QCW-GMCR recovers standard GMCR equilibria when feasibility is binary, there are no forbidden states, and every unilateral move is definitely warranted.Boolean feasibility alone does not suffice for recovery.Source: §5.2 · pp. 8–9
- Graded reachability can exclude a physical option de-selection because epistemic warrant and the physical act are distinct; reconciling them requires a two-layer move model.The proposed physical-state-plus-epistemic-warrant model is left to future work.Source: §5.2 · p. 9
6 Entailment-Graded and Catastrophe-Avoiding Equilibria
The section defines stability using entailment-graded improvements and safe reachability. It identifies the most demanding stability level and a robustness guarantee spanning reduction operators and entailment levels.
6 Entailment-Graded and Catastrophe-Avoiding Equilibria
- GMR, SMR, and SEQ restrict improvement and sanction moves to level-ℓ reachability, with an asymmetric variant allowing different levels for initial moves and sanctions.Catastrophe-avoiding variants restrict moves to safe reachability within Squasi.Source: §6 · p. 9
- Level U stability is the most demanding and remains stable even when decision makers reason optimistically about capabilities.The stability hierarchy is grounded in the nested improvement sets, with emptiness propagating downward through their inclusions.Source: §6 · p. 9
- Cross-level robustness means stability at all three entailment levels, equivalently level U; full robustness also requires stability under all four canonical operators.Cross-operator robustness alone means stability under all four operators.Source: §6 · p. 9
- If a state is fully robust and every transition into F has E = N, it remains stable and F remains unreachable under every admissible reduction operator and entailment level.The result applies equivalently to the four canonical operators.Source: §6 · p. 9
7 Coalitional Stability under Epistemic Ambiguity
The coalitional extension grades joint improvements by the warrant of their constituent moves, extending GMCR coalition analysis to epistemically ambiguous settings. The section establishes a stability hierarchy and a coalition-robust catastrophe invariant.
7 Coalitional Stability under Epistemic Ambiguity
- A level-ℓ coalitional improvement is reached through a nonempty sequence of unilateral moves by coalition members, each carrying move entailment in Dℓ, and improves every member's preference.The definition adopts one convention among literature variants about legality and whether all coalition members must improve.Source: §7 · p. 10
- Coalitional Nash stability nests as SCNash,U ⊆ SCNash,YN ⊆ SCNash,Y because the warrant condition relaxes across the nested levels.The improvement-warrant sets satisfy DY ⊂ DYN ⊂ DU.Source: §7 · p. 10
- A joint maneuver's warrant is bounded by its weakest link, so nominal coalition power may exceed its epistemically executable power.Tightening the entailment level thins coalitional reachability at least as fast as individual reachability.Source: §7 · p. 10
- The quasi-closed-world invariant extends to coalitional sequences: if decision makers stay within Squasi and avoid unilateral moves into B, no coalition sequence reaches F.The path-structural proof applies regardless of who moves.Source: §7 · p. 10
- The classical binary coalitional stability hierarchy is machine-checked, while the level-ℓ grading remains beyond the formalization frontier.The checked hierarchy includes CNash ⊆ CSMR ⊆ CGMR and CNash ⊆ CSEQ ⊆ CGMR.Source: §7 · p. 10
8 Four-Valued Hypergames
The four-valued hypergame gives each decision maker subjective assessments of option feasibility and safety, and defines a shared safe core across their subjective worlds. A nonempty core alone does not ensure a common equilibrium; existence follows under agreement on the core when the restricted graph has an equilibrium.
8 Four-Valued Hypergames
- A nonempty shared safe core does not guarantee a hypergame catastrophe-avoiding equilibrium: two states and two decision makers yield disjoint stable sets even under Nash, GMR, SMR, or SEQ.Each subjective game has an equilibrium, but the states stable for the two decision makers differ.Source: §8 · pp. 10–11
- When decision makers agree on reachability and preferences within the shared safe core, an equilibrium of the safe-move-restricted graph yields a hypergame catastrophe-avoiding equilibrium there.Moves outside the core are excluded by construction; full-game stability is not claimed or required.Source: §8 · p. 11
- The weakest epistemic-divergence conditions that preserve existence remain open, between sufficient full agreement on the core and insufficient mere nonemptiness.The existence result requires agreement on subjective reachability and preferences within the core, plus an equilibrium in the restricted graph.Source: §8 · p. 11
- The four-valued hypergame places ignorance and contradictory evidence inside option assessments, whereas earlier hypergame-GMCR models kept options binary within each perceived game.Binary coincident assessments recover an ordinary graph model, while binary divergent assessments recover a classical first-level hypergame.Source: §8 · p. 11
- An empty shared safe core diagnoses structural epistemic conflict: decision makers must align beliefs before equilibrium analysis can proceed.The proposed alignment can involve joint fact-finding, operator harmonization, or catastrophe-threshold alignment.Source: §8 · p. 12
9 Illustrative Example
The example shows how contradictory evidence about escalation changes its reachability status and how a forbidden catastrophe can constrain outcomes. Under the example’s stated preference and move assumptions, mutual de-escalation is robust across the reduction operators and reachability levels.
9 Illustrative Example
- Under Γ∧, states involving B’s escalation inherit feasibility YN, while states built only on definite options remain Y.The example assigns contradictory evidence to B’s escalation capability.Source: §9 · p. 12
- Mutual de-escalation is stable across all four reduction operators and all entailment levels when the example adds a forbidden nuclear-exchange state with a single-step boundary.The verdict depends on the example’s specified preferences and moves, not option status alone.Source: §9 · p. 12
- B’s escalation from mutual de-escalation has warrant Y ⇒w YN, making it credible but not definite.At the definite level B has no escalation moves; at the credible level the threat re-enters analysis and GMR, SMR, and SEQ sanctions must be examined.Source: §9 · p. 12
10 Machine-Checked Formalization in Lean 4
The Lean 4 development machine-checks a reusable classical GMCR core and selected QCW-GMCR results, including stability hierarchies, four-valued algebra, reductions, and graded reachability. It targets the framework’s load-bearing skeleton; several central theorems remain unformalized.
10.1 Classical GMCR core
- The classical core represents decision makers’ moves and strict preferences as relations over types of decision makers and states.Coalitional reachability is built from single moves by coalition members.Source: §10.1 · p. 12
- The classical individual stability hierarchy is machine-checked, including Nash ⊆ SMR ⊆ GMR and Nash ⊆ SEQ ⊆ GMR, alongside improvement-reachability and legality inclusions.The formalization also verifies coalitional hierarchies for Nash, GMR, SMR, and SEQ stability.Source: §10.1 · p. 13
- The individual and coalitional hierarchy proofs require no preference axioms, and definitions range over arbitrary, possibly infinite, type-level models.Finiteness is imposed only where computation requires it.Source: §10.1 · p. 13
10.2 Four-valued layer
- The four-valued layer machine-checks conjunction’s commutativity, associativity, and idempotence, plus absorption by N, identity of Y, and compositional propagation over finite option sets.The truth space and connectives are decidable, with algebraic facts proved by exhaustive case analysis.Source: §10.2 · p. 13
- Each of the four canonical reduction operators is computable and satisfies classical extension and truth monotonicity; knowledge monotonicity is refuted for three operators and proved for δprec.The refuted knowledge-monotonicity claims prompted a correction to the framework.Source: §10.2 · p. 13
- The four-valued formalization verifies definite ⇒ credible ⇒ possible reachability and represents the quasi-closed space as Sreduced \ (F ∪ B).It also formalizes the subjective assessment and preference core of the hypergame and a shared-safe-core membership predicate.Source: §10.2 · p. 13
10.3 Scope and outlook
- The Lean development targets core algebra, reductions, reachability, and classical stability, while the quasi-closed-world invariant and corrected hypergame existence theorem remain unformalized.Other pending items include the corrected FDE characterization, path-entailment decay, and level-ℓ stability results.Source: §10.3 · p. 14
- Because the four-valued definitions are computable over finite types, the development can serve as a verified reference implementation for concrete conflicts.The sensitivity-analysis protocol can run through code whose correctness properties are theorems rather than test cases.Source: §10.3 · p. 14
11 Concluding Remarks
The conclusion records QCW-GMCR’s core framework and the current scope of its Lean formalization. Formal checking exposed and helped correct claims, while further formalization and extensions remain future work.
11 Concluding Remarks
- QCW-GMCR’s recorded core combines option-level four-valued foundations, entailment-graded reachability, constrained reduction operators, and catastrophe-avoiding equilibria with a quasi-closed-world invariant.The note also records the current status of the Lean 4 formalization.Source: §11 · p. 14
- Formalization exposed the reduction-operator monotonicity issue and helped align reachability definitions with the machine-checked warrant hierarchy.Further analytical checks led to a corrected FDE characterization, GMCR-recovery condition, and hypergame-existence statement.Source: §11 · pp. 14–15
- Future work includes formalizing remaining theorems, dynamic extensions with belief revision, empirical validation of reduction operators, and scaling methods for large option spaces.Source: §11 · p. 15