a33d5f697f
- What: (1) created the long-missing Arrow's impossibility alignment claim that multiple existing claims reference via wiki-link but had no file; (2) new mechanisms-domain claim about the formal verification milestone - Why: Yamamoto (PLOS One 2026) provides a full proof-calculus representation of Arrow's theorem — machine-verifiable, revealing global structure of the social welfare function. Fixes broken wiki-links across persistent-irreducible- disagreement, pluralistic-alignment, and related claims; adds formal certification to alignment impossibility arguments - Connections: depends_on chain from mechanisms claim into ai-alignment claim; links to pluralistic-alignment, RLHF/DPO failure, specification-trap, democratic-assemblies, formal-verification claims Pentagon-Agent: Theseus <THESEUS-001>
3.6 KiB
| type | title | author | url | date | domain | secondary_domains | format | status | priority | tags | processed_by | processed_date | claims_extracted | enrichments | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| source | A Full Formal Representation of Arrow's Impossibility Theorem | Kazuya Yamamoto | https://journals.plos.org/plosone/article?id=10.1371/journal.pone.0343069 | 2026-02-01 | ai-alignment |
|
paper | processed | medium |
|
theseus | 2026-03-11 |
|
|
Content
Constructs a full formal representation of Arrow's impossibility theorem using proof calculus in formal logic. Published in PLOS One, February 2026.
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. 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