Mechanism Design Logic

Origin. Connects mechanism design (Hurwicz, 1960s) to logic. Pauly's coalition logic. Van der Hoek, Wooldridge: social choice in logic. Formal verification of mechanisms. Automated mechanism design foundations.

Models. Designing games for desired outcomes. Mechanism: game + rules. Designer: wants particular outcome (efficiency, fairness). Agents: strategic, self-interested. Logic: express and verify mechanism properties.

Formalism.

Social choice function: f: Preferences^n → Outcomes Aggregates preferences to outcome.

Mechanism: M = (S₁,...,Sₙ, g) where:

Sᵢ: strategy space for agent i
g: S₁ × ... × Sₙ → Outcomes (outcome function)

Implementation: f implemented by M if: equilibrium strategies yield f's output. Dominant strategy: works regardless of others. Nash: works given others' equilibrium play.

Properties (in logic):

Incentive compatibility: ∀i.∀θᵢ.∀θ'ᵢ. uᵢ(f(θ), θᵢ) ≥ uᵢ(f(θ'ᵢ, θ₋ᵢ), θᵢ) "Truth-telling is optimal"
Efficiency: ¬∃o'. ∀i. uᵢ(o') ≥ uᵢ(f(θ)) ∧ ∃i. uᵢ(o') > uᵢ(f(θ)) "No Pareto improvement"
Individual rationality: uᵢ(f(θ), θᵢ) ≥ uᵢ(default) "Participation is beneficial"

Verification: Check mechanism satisfies properties. Model check: finite types. Theorem prove: symbolic.

Auction logic: Vickrey auction: second-price sealed-bid. Verify: truthful bidding is dominant strategy.

Symbols.

Symbol	Unicode	Name	Meaning
f	—	Social choice	Preference aggregation
M	—	Mechanism	Game form
u	—	Utility	Payoff function
θ	U+03B8	Theta	An agent's type: its private information
∀	U+2200	Universal quantifier	Over agents and type reports
∃	U+2203	Existential quantifier	Over alternative outcomes, in the efficiency condition
¬	U+00AC	Negation	No Pareto improvement exists
∧	U+2227	Conjunction	Joins the two halves of Pareto dominance
≥	U+2265	Greater-than or equal to	Weak preference in utility
>	—	Greater than	Strict preference
×	U+00D7	Multiplication sign	Product of strategy spaces
→	U+2192	Function arrow	The type of the outcome function
S	—	Strategy	Action space
g	—	Outcome	Result function
IC	—	Incentive compatible	Truthful

Metatheory. Two impossibility theorems bound what any mechanism can do. Gibbard (1973) and Satterthwaite (1975) proved that on an unrestricted preference domain with at least three attainable alternatives, every strategyproof and surjective social choice function is dictatorial, so truthful voting cannot be made a dominant strategy. Myerson and Satterthwaite (1983) proved the analogous result with transfers: no bilateral trading mechanism is simultaneously efficient, incentive compatible, individually rational, and budget balanced. What remains positive is the revelation principle (Gibbard 1973, Myerson 1979): any outcome achievable in equilibrium of any mechanism is achievable by an incentive-compatible direct mechanism, which reduces the design space to truthful direct revelation. Maskin's theorem gives monotonicity as necessary for Nash implementation, and with at least three agents monotonicity plus no veto power as sufficient. Arrow's theorem and Gibbard–Satterthwaite have both been machine-checked, by Nipkow (2009) in Isabelle/HOL and by Tang and Lin (2009) via reduction to a finite base case decided by a SAT solver.

Applies to. Auction design. Voting systems. Resource allocation. Matching markets. Public goods. Regulatory design. Blockchain mechanisms.

Limitations. The central results are negative, so the field's positive content comes from restricting the domain — single-peaked preferences, quasilinear utility, a common prior — and each restriction is an assumption about agents rather than a theorem. The revelation principle is a statement about equilibrium outcomes only: it says a truthful mechanism exists, not that it can be computed or that agents can find the equilibrium, and it discards indirect mechanisms that may be far easier to run. Computation is where the constructions break down: the VCG outcome in a combinatorial auction requires solving winner determination, which is NP-hard and hard to approximate, and Conitzer and Sandholm (2003) showed that designing an optimal deterministic mechanism is NP-hard even with a single agent. Verification presupposes finitely many types, while the standard models are continuous.