b917ff7e4f
- What: Added Yamamoto (PLOS One, 2026-02) as evidence to the existing Arrow's impossibility claim in foundations/collective-intelligence/. Enriched body with paragraph on formal proof calculus representation and its implications. Updated source field and last_evaluated date. Marked archive source as processed. - Why: Yamamoto provides the first full formal representation of Arrow's theorem in proof calculus (complementing AAAI 2008 computer-aided proof), revealing the global structure of the social welfare function. This upgrades the claim's evidentiary basis from mathematical argument to formally derivable result, strengthening the alignment impossibility implication. - Connections: Enrichment only — no standalone claim warranted per curator notes. Relates to formal verification theme in domains/ai-alignment/ (machine-checked correctness). Pentagon-Agent: Theseus <3F9A1B2C-D4E5-6F7A-8B9C-0D1E2F3A4B5C>
2.7 KiB
| type | title | author | url | date | domain | secondary_domains | format | status | processed_by | processed_date | claims_extracted | enrichments | priority | tags | |||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 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 | theseus | 2026-03-11 | 0 | 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 evidence for formal proof calculus representation of Arrow's theorem; added to source field and body | medium |
|
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.
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