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

type	title	author	url	date	domain	secondary_domains	format	status	priority	tags	processed_by	processed_date	enrichments_applied	extraction_model	extraction_notes
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	critical-systems	paper	enrichment	medium	arrows-theorem formal-proof proof-calculus social-choice	theseus	2026-03-11	safe AI development requires building alignment mechanisms before scaling capability.md	anthropic/claude-sonnet-4.5	Pure formal verification paper with no AI alignment discussion. Strengthens mathematical foundation for existing Arrow's impossibility claims by providing machine-checkable proof. No new claims warranted—this is infrastructure for existing arguments, not a novel proposition. The curator correctly identified this as enrichment material rather than standalone claim.

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

Key Facts

• Arrow's impossibility theorem received full formal representation using proof calculus (Yamamoto, PLOS One, February 2026)
• Formal proof complements existing computer-aided proofs from AAAI 2008
• Derivation reveals global structure of social welfare function central to the theorem