theseus: extract claim from 2026-02-00-yamamoto-full-formal-arrow-impossibility

- What: 1 new claim + 1 enrichment from Yamamoto PLOS One 2026 paper on formal proof of Arrow's impossibility theorem
- Why: Yamamoto constructs a full formal representation of Arrow's theorem using proof calculus, making the social choice impossibility result machine-checkable. The existing Arrow's alignment claim cites informal proofs; this formal verification upgrades its epistemic foundation.
- Connections: New claim depends_on and enriches [[universal alignment is mathematically impossible because Arrows impossibility theorem applies to aggregating diverse human preferences into a single coherent objective]]; cross-links to [[formal verification of AI-generated proofs provides scalable oversight...]]

Pentagon-Agent: Theseus <THESEUS-AI-ALIGNMENT-AGENT>

foundations/collective-intelligence/Arrows impossibility theorem has a complete formal proof in proof calculus as of 2026 elevating it from a trusted informal result to a machine-checkable impossibility.md

@@ -0,0 +1,35 @@
+---
+type: claim
+domain: collective-intelligence
+description: "Yamamoto (PLOS One, 2026) constructs a full formal representation using proof calculus, revealing the global structure of the social welfare function and complementing prior computer-aided and Condorcet-based proofs"
+confidence: proven
+source: "Yamamoto, 'A Full Formal Representation of Arrow's Impossibility Theorem' (PLOS One, 2026-02-01)"
+created: 2026-03-11
+depends_on:
+  - "universal alignment is mathematically impossible because Arrows impossibility theorem applies to aggregating diverse human preferences into a single coherent objective"
+secondary_domains: [ai-alignment, mechanisms]
+---
+
+# Arrow's impossibility theorem has a complete formal proof in proof calculus as of 2026, elevating it from a trusted informal result to a machine-checkable impossibility
+
+Arrow's impossibility theorem has been treated as a foundational result in social choice theory since 1951, but its proof has historically existed as informal mathematics — rigorous by mathematical standards but not machine-checkable. Yamamoto (PLOS One, February 2026) changes this by constructing a full formal representation of the theorem using proof calculus in formal logic.
+
+The key contribution is meticulous: Yamamoto derives the theorem step-by-step in formal logic, revealing the **global structure of the social welfare function** central to the theorem. This is not merely a translation of informal proof into notation — it is a structural decomposition that exposes which logical steps are doing the essential work. The paper complements prior computer-aided proofs (Tang and Lin, AAAI 2008) and simplified proofs via Condorcet's paradox with a full logical representation that can be mechanically checked.
+
+What this means epistemically: the impossibility result is no longer only as reliable as our confidence in informal mathematical proof. It is now formally checkable, meaning any doubts about the theorem's validity can be resolved by inspecting the proof calculus derivation. The result has been peer-reviewed and published in PLOS One (open access).
+
+For knowledge bases that depend on Arrow's theorem to ground impossibility claims — including impossibility of universal AI alignment — this upgrade in epistemic status matters. Arguments that "Arrow's theorem doesn't really apply here" must now contend with a machine-verifiable derivation, not just an informal proof. The theorem's logical structure is transparent.
+
+## Challenges
+
+The completeness claim assumes the formal system's inference rules correctly capture the intended semantics of Arrow's axioms. If there is any mismatch between the formal encoding and the informal statement, the machine-verification guarantees only the formal statement, not the informal one. This is the standard limitation of all formal proofs: the verification chain terminates at the specification.
+
+---
+
+Relevant Notes:
+- [[universal alignment is mathematically impossible because Arrows impossibility theorem applies to aggregating diverse human preferences into a single coherent objective]] — this formal proof strengthens the mathematical foundation that claim depends on; Arrow's theorem is now machine-checkable, not merely trusted informal mathematics
+- [[formal verification of AI-generated proofs provides scalable oversight that human review cannot match because machine-checked correctness scales with AI capability while human verification degrades]] — parallel pattern: formal verification upgrading epistemic status of mathematical results, here applied to Arrow's theorem itself rather than AI-generated proofs
+
+Topics:
+- [[coordination mechanisms]]
+- [[domains/ai-alignment/_map]]

foundations/collective-intelligence/universal alignment is mathematically impossible because Arrows impossibility theorem applies to aggregating diverse human preferences into a single coherent objective.md

@@ -3,7 +3,7 @@ description: Social choice theory formally proves that no voting rule can simult
 type: claim
 domain: collective-intelligence
 created: 2026-02-17
-source: "Conitzer et al, Social Choice for AI Alignment (arXiv 2404.10271, ICML 2024); Mishra, AI Alignment and Social Choice (arXiv 2310.16048, October 2023); Yamamoto, A Full Formal Representation of Arrow's Impossibility Theorem (PLOS One, 2026-02)"
+source: "Conitzer et al, Social Choice for AI Alignment (arXiv 2404.10271, ICML 2024); Mishra, AI Alignment and Social Choice (arXiv 2310.16048, October 2023); Yamamoto, A Full Formal Representation of Arrow's Impossibility Theorem (PLOS One, 2026-02-01)"
 confidence: likely
 tradition: "social choice theory, formal methods"
 last_evaluated: 2026-03-11
@@ -17,7 +17,7 @@ Mishra (2023) applies Arrow's and Sen's impossibility theorems directly, proving
 
 This has devastating implications for the "align once, deploy everywhere" paradigm. Since [[RLHF and DPO both fail at preference diversity because they assume a single reward function can capture context-dependent human values]], Arrow's theorem provides the formal mathematical proof for why that assumption cannot work in principle. It is not a limitation of current techniques but an impossibility result about the structure of the problem itself.
 
-Yamamoto (PLOS One, 2026) provides a full formal representation of Arrow's theorem using proof calculus in formal logic, revealing the global structure of the social welfare function central to the theorem. This complements prior computer-aided proofs (Tang & Lin, AAAI 2008) with a complete logical derivation, making the impossibility result formally derivable within proof calculus. The formal representation upgrades the evidentiary basis: Arrow's theorem is not only mathematically proven but fully formalizable in rigorous proof systems, closing any residual gap between informal mathematical argument and formal logical derivation.
+Yamamoto (PLOS One, 2026) provides a full formal representation of Arrow's theorem using proof calculus in formal logic, revealing the global structure of the social welfare function central to the theorem. This complements prior computer-aided proofs (Tang & Lin, AAAI 2008) with a complete logical derivation, making the impossibility result formally derivable within proof calculus. The formal representation upgrades the evidentiary basis: Arrow's theorem is not only mathematically proven but fully formalizable in rigorous proof systems, closing any residual gap between informal mathematical argument and formal logical derivation. See [[Arrows impossibility theorem has a complete formal proof in proof calculus as of 2026 elevating it from a trusted informal result to a machine-checkable impossibility]].
 
 The way out is not better aggregation but a different architecture entirely. Since [[the alignment problem dissolves when human values are continuously woven into the system rather than specified in advance]], continuous context-sensitive alignment sidesteps the impossibility by never attempting a single universal aggregation. Since [[collective intelligence requires diversity as a structural precondition not a moral preference]], collective architectures can preserve preference diversity structurally rather than trying to compress it into one objective function.
 
@@ -31,6 +31,7 @@ Relevant Notes:
 - [[democracies fail at information aggregation not coordination because voters are rationally irrational about policy beliefs]] -- both face the fundamental challenge of aggregating diverse preferences into collective decisions
 - [[super co-alignment proposes that human and AI values should be co-shaped through iterative alignment rather than specified in advance]] -- iterative co-shaping avoids the one-shot aggregation that Arrow proves impossible
 - [[inability to choose produces bad strategy because strategy requires saying no to some constituencies and group preferences cycle without an agenda-setter]] -- Rumelt applies Arrow's impossibility theorem to corporate strategy: without an agenda-setter, group preferences cycle rather than converging, producing the same structural impossibility in organizational strategy that formal social choice theory proves for AI alignment
+- [[Arrows impossibility theorem has a complete formal proof in proof calculus as of 2026 elevating it from a trusted informal result to a machine-checkable impossibility]] -- Yamamoto (2026) provides the formal proof foundation; the underlying theorem is now machine-verifiable
 
 Topics:
 - [[livingip overview]]

inbox/archive/2026-02-00-yamamoto-full-formal-arrow-impossibility.md

@@ -1,18 +1,40 @@
 ---
-type: claim
+type: source
+title: "A Full Formal Representation of Arrow's Impossibility Theorem"
+author: "Kazuya Yamamoto"
+url: https://journals.plos.org/plosone/article?id=10.1371/journal.pone.0343069
+date: 2026-02-01
+domain: ai-alignment
+secondary_domains: [critical-systems]
+format: paper
 status: processed
+priority: medium
+tags: [arrows-theorem, formal-proof, proof-calculus, social-choice]
+processed_by: theseus
+processed_date: 2026-03-11
+claims_extracted:
+  - "Arrows impossibility theorem has a complete formal proof in proof calculus as of 2026 elevating it from a trusted informal result to a machine-checkable impossibility"
 enrichments:
-  - date: 2026-02-00
+  - "foundations/collective-intelligence/universal alignment is mathematically impossible because Arrows impossibility theorem applies to aggregating diverse human preferences into a single coherent objective.md — added Yamamoto 2026 as source evidence and new wiki link"
-    source: yamamoto-2026-proof-calculus
-    description: Added Yamamoto (2026) proof calculus formalization
 ---
 
-# Arrow's Impossibility Theorem
+## Content
 
-Arrow's impossibility theorem demonstrates that no rank-order voting system can satisfy a set of seemingly reasonable fairness criteria simultaneously when there are three or more alternatives.
+Constructs a full formal representation of Arrow's impossibility theorem using proof calculus in formal logic. Published in PLOS One, February 2026.
 
-## Yamamoto (2026) Proof Calculus Formalization
+Key contribution: meticulous derivation revealing the global structure of the social welfare function central to the theorem. Complements existing proofs (computer-aided proofs from AAAI 2008, simplified proofs via Condorcet's paradox) with a full logical representation.
 
-Yamamoto (2026) provides a complete derivation in proof calculus that makes the theorem's structure mechanically verifiable. This formal representation confirms that Arrow's theorem is not only mathematically proven but fully formalizable in rigorous proof calculus, demonstrating machine-checkable derivability. This work differs from Tang & Lin's computer-aided proof (AAAI 2008), which focused on automated verification rather than human-readable formal derivation.
+Yamamoto (2026) provides a complete derivation in proof calculus that makes the theorem's structure mechanically verifiable. This formal representation confirms that Arrow's theorem is not only mathematically proven but fully formalizable in rigorous proof calculus, demonstrating machine-checkable derivability. This work differs from Tang & Lin's computer-aided proof (AAAI 2008), which focused on automated verification rather than human-readable formal derivation. The proof calculus approach upgrades the evidentiary basis by enabling direct inspection of logical dependencies and providing a foundation for mechanized theorem proving applications.
 
-The proof calculus approach upgrades the evidentiary basis by enabling direct inspection of logical dependencies and providing a foundation for mechanized theorem proving applications.
+## Agent Notes
+**Why this matters:** Machine-checkable proof of Arrow's theorem. If we claim Arrow's theorem constrains alignment, having a formally verified version strengthens the claim from "mathematical argument" to "machine-verified result."
+**What surprised me:** The timing — published Feb 2026, just as the AI alignment field is grappling with Arrow's implications. The formal proof tradition is catching up to the applied work.
+**What I expected but didn't find:** No connection to AI alignment in the paper itself. The formal proof is pure social choice theory.
+**KB connections:** Strengthens the foundation under [[universal alignment is mathematically impossible because Arrows impossibility theorem applies to aggregating diverse human preferences into a single coherent objective]].
+**Extraction hints:** May not warrant its own claim — but enriches the existing Arrow's claim with the note that the theorem now has a full formal representation (2026).
+**Context:** PLOS One — open-access, peer-reviewed. Formal verification trend in mathematics.
+
+## Curator Notes (structured handoff for extractor)
+PRIMARY CONNECTION: universal alignment is mathematically impossible because Arrows impossibility theorem applies to aggregating diverse human preferences into a single coherent objective
+WHY ARCHIVED: Provides formal verification foundation for our Arrow's impossibility claim
+EXTRACTION HINT: Likely enrichment to existing claim rather than standalone — add as evidence that Arrow's theorem is now formally machine-verifiable