1: \documentclass{article}

2: \usepackage{latexsym,amsmath,amssymb}

3: 

4: \def\log#1{\mathtt{#1}} % logic

5: \def\ss#1{\widehat{#1}} % gives the set of maxcon sets which contain #1

6: \def\o#1{\mathsf{#1}}

7: 

8: % the following is from Yde Venema

9: \newcommand{\bis}{\mathrel{\mathchoice%

10: {\raisebox{.3ex}{$\,

11:   \underline{\makebox[.7em]{$\leftrightarrow$}}\,$}}%

12: {\raisebox{.3ex}{$\,

13:   \underline{\makebox[.7em]{$\leftrightarrow$}}\,$}}%

14: {\raisebox{.2ex}{$\,

15:   \underline{\makebox[.5em]{\scriptsize$\leftrightarrow$}}\,$}}%

16: {\raisebox{.2ex}{$\,

17:   \underline{\makebox[.5em]{\scriptsize$\leftrightarrow$}}\,$}}}}

18: \def\bisim{\bis}

19: 

20: % Abbreviations

21: \renewcommand{\l}{\langle}

22: \renewcommand{\r}{\rangle}

23: \renewcommand{\phi}{\varphi}

24: \newcommand{\Dia}{\Diamond}

25: \newcommand{\lr}{\leftrightarrow}

26: \newcommand{\ali}{\divideontimes} % for alternative iteration

27: \def\mv#1{\xrightarrow{#1}}

28: \def\dht#1#2#3#4#5{\{#1\} \{#2\} #3 \{#4\} \{#5\}}

29: 

30: 

31: \newcommand{\cfg}{C \! f \! g}

32: 

33: % Logical Systems

34: \newcommand{\GL}{\textsl{GL}}

35: \newcommand{\PDL}{\textsl{PDL}}

36: \newcommand{\FOL}{\textsl{FOL}}

37: 

38: % Special Environments

39: \newcounter{tbsnr}

40: \newenvironment{tbs}

41: {\addtocounter{tbsnr}{1}\par\bigskip \noindent\fbox{\thetbsnr}

42: \hspace*{\fill}\begin{minipage}{10cm}\tt}

43: %\typein{OPPASSEN GEBLAZEN}}

44: {\end{minipage}\hspace*{\fill}\bigskip}

45: \newcommand{\tb}[1]{\begin{tbs}{#1}\end{tbs}}

46: 

47: \newenvironment{proof}{{\em Proof.}}{\hfill $\Box$ \\}

48: 

49: \newtheorem{theorem}{Theorem}

50: \newtheorem{lemma}[theorem]{Lemma}

51: \newtheorem{corollary}[theorem]{Corollary}

52: \newtheorem{proposition}[theorem]{Proposition}

53: \newtheorem{definition}{Definition}

54: 

55: \begin{document}

56: 

57: \title{Programming and Verifying \\  Subgame-Perfect Mechanisms}

58: 

59: \author{Marc Pauly \vspace{0.3 cm} \\

60: \small CNRS, IRIT \\

61: \small \texttt{pauly@irit.fr}}

62: 

63: \date{\today}

64: 

65: 

66: \maketitle

67: 

68: \begin{abstract}

69: An extension of the WHILE-language is developed for programming

70: game-theoretic mechanisms involving multiple agents. Examples of

71: such mechanisms include auctions, voting procedures, and

72: negotiation protocols. A structured operational semantics is

73: provided in terms of extensive games of almost perfect

74: information. Hoare-style partial correctness assertions are

75: proposed to reason about the correctness of these mechanisms,

76: where correctness is interpreted as the existence of a subgame-perfect 

77: equilibrium. Using an extensional approach to pre- and

78: postconditions, we show that an extension of Hoare's original

79: calculus is sound and complete for reasoning about subgame-perfect

80: equilibria in game-theoretic mechanisms.  We use the calculus to

81: verify some simple mechanisms like the Dutch auction.

82: \end{abstract}

83: 

84: %

85: %-------------------------------------

86: %

87: \section{Introduction}

88: %

89: %-------------------------------------

90: %

91: 

92: In recent years, games have become more prominent in different

93: areas of computer science research. The reason for this seems to

94: be the realisation that games form a natural generalisation of

95: programs. This insight can be realised on a number of different

96: levels (we shall only mention two): On a foundational level, games

97: have been used to provide an alternative model of computation, the

98: alternating Turing machine \cite{alternating-TM}. At a more

99: abstract level, program logics like propositional dynamic logic

100: have been extended to games \cite{Parikh}.

101: 

102: From a game-theoretic perspective, much of this work is extremely

103: narrow, since it mainly focuses on determined 2-player win/loss

104: games of perfect information. On the other hand, game theory has

105: developed a wealth of techniques to study more complicated

106: situations where agents interact, involving more than two players,

107: imperfect information, and preferences over outcomes which cannot

108: be captured by simply distinguishing between winning and losing.

109: Still, it has been suggested \cite{Parikh:SoSo} that combining

110: research in game theory and computer science, we may be able to

111: obtain a better understanding of {\em social software}, i.e., of

112: the formal properties of the social processes we are involved in.

113: The present paper tries to contribute to this aim.

114: 

115: More concretely, we attempt to generalise techniques from formal

116: program verification to games or game-theoretic mechanisms such as

117: auctions, voting procedures, etc. From a logical perspective, two

118: approaches suggest themselves. On the one hand, one might extend

119: model checking approaches \cite{Clarke}, where one uses, for

120: instance, temporal logic to specify properties of a system

121: (program/game) and proceeds to verify these properties using model

122: checking. This approach has been generalised to reason about

123: coalitional power in games \cite{coal1}. On the other hand, one

124: can try to extend approaches based on theorem proving using a

125: formal calculus in which one can derive certain properties of a

126: system. This approach will be taken here.

127: 

128: The axiomatic or compositional approach to program verification

129: was introduced by Hoare \cite{Hoare-logic} and Dijkstra \cite{D},

130: and provided the foundation stone for formal program verification

131: \cite{Nielson,Apt-Olderog,Francez}. In Hoare's calculus,

132: correctness assertions of the form $\{P\} \pi \{Q\}$ are used to

133: express that program $\pi$, when executed in a state satisfying

134: $P$, will terminate in a state satisfying $Q$ (provided it does

135: terminate). In generalising the

136: program verification approach to games, this paper makes two

137: contributions: First, it defines a programming language which is a

138: simple extension of the WHILE-language sufficient to program

139: game-theoretic mechanisms. The syntax of this language is defined

140: in section \ref{syntax}, and section \ref{semantics} provides a

141: structured operational semantics in terms of extensive games of

142: almost perfect information. Second, we are going to extend Hoare's

143: calculus to reason about the correctness of these mechanisms,

144: where correctness is interpreted as the existence of a subgame-perfect 

145: equilibrium with a certain payoff. In section

146: \ref{mech-des}, we define our new notion of correctness by

147: providing a game-theoretic interpretation of $\{P\}\pi\{Q\}$, also

148: linking it to the game-theoretic notion of implementation and

149: mechanism design.  Section \ref{calculus} presents an extensional

150: calculus for reasoning about mechanism correctness, and provides

151: proofs of soundness and completeness.  Finally, section \ref{apps}

152: illustrates the calculus in the verification of a few simple mechanisms.

153: 

154: %

155: %-------------------------------------

156: %

157: \section{Syntax of MPL}

158: \label{syntax}

159: %

160: %-------------------------------------

161: %

162: 

163: Our mechanism programming language (MPL) is a simple extension of

164: standard imperative programming languages; more concretely,

165: our point of departure is the well-known WHILE-language (see e.g.

166: \cite{Nielson}).

167: We assume throughout that we are given a nonempty set of agents or players

168: $Ags$,

169: a set of mechanism variables $MV$, a set of function symbols $Funs$ and a set

170: of relation symbols $Rels$. Using these, we inductively define

171: terms $t$, boolean expressions $B$ and

172: mechanisms (or game forms) $\gamma$ as follows:

173: 

174: \[ \begin{array}{|rl|}

175: \hline

176: t := & x \; | \; f^k(t_1, \ldots, t_k) \\[1ex]

177: 

178: B := & true \; | \; R^k(t_1, \ldots, t_k) \; | \;

179:  \neg B \; | \; B_{1} \wedge B_{2} \\[1ex]

180: 

181: \gamma := & x:=t \; | \; \gamma_{1} ; \gamma_{2} \; | \;

182: \mathtt{if} \: B \: \mathtt{then} \: \gamma_{1} \: \mathtt{else} \: \gamma_{2}

183: \; | \; \mathtt{while} \: B \: \mathtt{do} \: \gamma \; | \; \\

184: & \mathtt{ch}_A(\{x_a | a \in A\}) \\ \hline

185: \end{array} \]

186: where $a {\in} Ags$, $f^k {\in} Funs$ is a $k$-ary function symbol

187: (in case $k=0$ we are dealing

188: with constants), $R^k {\in} Rels$ a $k$-ary

189: relation symbol, $x,x_a {\in} MV$, and $A \subseteq Ags$ is finite and

190: nonempty.

191: 

192: The last construct presents the only addition to the standard

193: WHILE-language: $\mathtt{ch}_A$ lets agent $a \in A$ choose any value for

194: the variable $x_a$.  The agents in $A$ are making their choice

195: simultaneously, so in order to prevent conflicting assignments to

196: variables, we require all the $x_a$ to be distinct.  One can think of

197: the $\mathtt{ch}_A$ construct as a strategic game among $n$ agents,

198: where the strategic choice of an agent is represented by the value of

199: his/her variable.  While the set of agents may be infinite, we require

200: each $\mathtt{ch}_A$ construct to involve only finitely many agents. 

201: In the special case where $|A|=1$, we have a simple nondeterministic

202: choice.  More concretely, in case agent $1$ can choose between 2

203: different strategies, executing $\gamma_{1}$ vs.\ executing

204: $\gamma_{2}$, we can describe this situation as \[

205: \mathtt{ch}_{\{1\}}(\{x_1\}) ; \mathtt{if} \: x_1=0 \: \mathtt{then}

206: \: \gamma_{1} \: \mathtt{else} \: \gamma_{2} ,\] where we assume that

207: the domain of computation is the set of natural numbers, for instance,

208: and $= \: \in Rels$ and $0 \in Funs$.

209: 

210: MPL is an extremely general programming language for a large

211: variety of different kinds of mechanisms. In section

212: \ref{mech-des} we shall use it for defining mechanisms for

213: different kinds of auctions. Voting procedures are further

214: examples of mechanisms which can be programmed using MPL. As an

215: example, the well-known Borda-count procedure (see, e.g.,

216: \cite{Brams:voting}) can be programmed as follows:

217: \begin{tabbing}

218: $\mathtt{ch}_{Ags}(\{x_1,x_2, \ldots, x_N\})$; \\

219: $i:=1;$ \\

220: $\mathtt{while} \: i \leq K \: \mathtt{do} \: c_i:=0; i:=i+1$; \\

221: $a:=1;$ \\

222: $\mathtt{while}$ \= $\: a \leq N \: \mathtt{do}$ \\

223:     \> $i:=1;$ \\

224:     \> $\mathtt{while}$ \= $\: i \leq K \: \mathtt{do}$ \\

225:     \> \> $c_i:= c_i + x_a[i];$ \\

226:     \> \> $i:=i+1;$ \\

227:     \> $a:=a+1$

228: \end{tabbing}

229: In this example, we assume that $Ags=\{1, 2, \ldots, N\}$, and

230: that the agents have to choose among $K$ candidates. First, each

231: agent $a$ can cast a ballot of the form $x_a = (p_1, p_2, \ldots,

232: p_K)$, where $p_i$ is the number of points the agent gives to

233: candidate $i$. Ballots have to be rankings of candidates, i.e.,

234: the most preferred candidate must obtain $K$ points, the next

235: preferred candidate $K-1$ points, etc., so that the least-preferred 

236: candidate obtains 1 point. Hence, we assume implicitly

237: that the domain of computation contains these possible ballots,

238: and that the initial choice assigns a ballot to each $x_a$. (Note

239: that since the domain of computation will also contain the natural

240: numbers, we need to make sure that each $x_a$ is assigned to an

241: element of the appropriate ballot type, but we shall ignore this

242: problem in order to keep the algorithm simple.) Once the ballots

243: are cast, $a$ is initialised to the first agent, and $i$ to the

244: first candidate. The variable $c_i$ counts the number of points

245: accumulated by candidate $i$, and is initialised to $0$. The main

246: part of the algorithm then simply sums up the points for each

247: candidate, where $x_a[i]$ refers to $p_i$, in case $x_a = (p_1,

248: p_2, \ldots, p_K)$. The winner of the vote will be the candidate

249: accumulating the most points.

250: 

251: A further example of a well-known mechanism which can be

252: programmed in MPL is a version of Rubinstein's negotiation

253: protocol of alternating offers (see \cite{Osborne,Kraus}).

254: \begin{tabbing}

255: $agree:=false;$ \\

256: $optout:=false;$ \\

257: $i:=1$; \\

258: $\mathtt{while}$ \= $\: \neg optout \wedge \neg agree \: \mathtt{do}$ \\

259: \> $\mathtt{if} \: i=1 \: \mathtt{then} \:

260: \mathtt{ch}_{\{1\}}(\{x\}) \mathtt{else} \:

261: \mathtt{ch}_{\{2\}}(\{x\});$ \\

262: \> $\mathtt{if} \: i=1 \: \mathtt{then} \:

263: \mathtt{ch}_{\{2\}}(\{y\}) \mathtt{else} \:

264: \mathtt{ch}_{\{1\}}(\{y\});$ \\

265: \> $\mathtt{if} \: y=0 \:$ \= $\mathtt{then} \: agree:= true$ \\

266: \>\> $\mathtt{else} \: \mathtt{if} \: y=1 \: \mathtt{then} \:

267: optout:= true \: \mathtt{else} \: i:=3-i$

268: \end{tabbing}

269: For simplicity, we have assumed that there are only two agents who

270: try to reach an agreement over, e.g., the price of a car which

271: agent 1 wants to sell to agent 2, and so we can assume the domain

272: of computation to be simply the natural numbers. The negotiation

273: procedure can end in an agreement concerning the price, one of the

274: agents can opt out of the negotiation (in which case some

275: predetermined event will occur), or the negotiation can go on

276: forever. The protocol starts by agent 1 making a price offer $x$.

277: Agent 2 responds by choosing $y$, where we interpret $y=0$ as

278: signalling agreement to the price offered, $y=1$ as a decision to

279: opt out of the negotiation, and any other value for $y$ as

280: signalling the desire to make a counteroffer, upon which we get

281: another iteration of the loop with the roles reversed.

282: 

283: The above negotiation protocol is very general, and numerous

284: instances of it have been analysed game-theoretically

285: \cite{Kraus}. We shall not go into this or the voting mechanism in

286: more detail, since our main aim at this point is only to suggest the 

287: generality of the mechanism programming language defined.  Section

288: \ref{apps} will provide a more detailed and more formal treatment of

289: examples such as the ones given here. In the following section, we shall

290: provide a formal semantics for this language in terms of games. 

291: Furthermore, we will subsequently provide a calculus for reasoning

292: about the existence of game-theoretic equilibria in these mechanisms,

293: and about the payoffs the agents obtain in equilibrium.

294: 

295: Note that MPL only allows one to construct mechanisms with

296: almost-perfect information, i.e., agents are perfectly informed

297: about all the choices made except possibly for simultaneous moves.

298: Different subclasses of MPL-mechanisms correspond to various

299: natural assumptions regarding the power of the mechanism designer

300: and the agents in general.  The class MPL(PRG) of {\em programs}

301: is the class of MPL-mechanisms which do not contain any

302: $\mathtt{ch}_A$ construct. Without this construct, MPL is simply

303: the WHILE-language. The class MPL(PI) of {\em perfect-information

304: mechanisms} will restrict the use of $\mathtt{ch}_A$ to cases

305: where $|A|=1$, i.e., where all choices involve only a single

306: agent. Perfect-information mechanisms allow different agents to

307: make choices at different times, but all choices are public, there are 

308: no simultaneous moves.

309: 

310: %

311: %--------------------------------------------------------

312: %

313: \section{Structured Operational Semantics via Games}

314: \label{semantics}

315: %

316: %--------------------------------------------------------

317: %

318: 

319: The most detailed semantics we can provide for MPL expressions is a

320: structured operational semantics which specifies the configurations a

321: mechanism can be in and the possible transitions between

322: configurations.  For programs, such a semantics gives rise to an

323: execution sequence or trace, and in case of nondeterministic programs to

324: an execution tree.  Since in the case of mechanisms we are dealing with

325: multiple agents, we arrive at a game tree whose

326: positions are the possible configurations of the mechanism.

327: 

328: As is standard in first-order logic, we will work with an

329: interpretation ${\mathcal I}$ which provides us with a domain

330: $D_{\mathcal I}$ and functions and relations over $D_{\mathcal I}$

331: as interpretations for the symbols in $Funs$ and $Rels$.

332: Furthermore, we assume that besides the relations associated to

333: symbols in $Rels$, our interpretation contains an additional

334: binary $\geq_a^{\mathcal I}$-relation for every agent $a \in Ags$.

335: The $\geq_a^{\mathcal I}$ relation will be used to represent agent

336: $a$'s preference over the elements of the domain. Note that

337: mechanisms programmed in MPL cannot refer to these preferences,

338: since $\geq_a \not\in Rels$.

339: 

340: The only requirements on ${\mathcal I}$ are that the preference

341: relations $\geq_a^{\mathcal I} \subseteq D_{\mathcal I} \times

342: D_{\mathcal I}$ satisfy the following properties: (1)

343: $\geq_a^{\mathcal I}$ must be a partial pre-order, i.e., a

344: reflexive and transitive relation on $D_{\mathcal I}$, and (2)

345: there is a uniformly worst outcome (which we denote as $-\infty$),

346: i.e., there is some $d \in D_{\mathcal I}$ such that for all $a

347: \in Ags$ and $x \in D_{\mathcal I}$ we have $x \geq_a^{\mathcal I} d$. 

348: Usually, preference relations will be total orders, but our framework

349: does not require this. The uniformly worst outcome is needed to deal

350: with some infinite runs resulting from while-loops, it plays no

351: substantive role in any of the examples considered.

352: 

353: A state $s: MV \rightarrow D_{\mathcal I}$ is a function assigning

354: a domain element to each mechanism variable. Let $S_{\mathcal I}$

355: be the set of all states over ${\mathcal I}$. In general, whenever

356: the intended interpretation ${\mathcal I}$ is clear we shall tend

357: to omit it. The following standard logical notation will be used:

358: ${\mathcal I},s \models \phi$ denotes that a first-order formula

359: $\phi$ whose variables are all in $MV$ is true in ${\mathcal I}$

360: at state $s$. Similarly, we let $\phi^{\mathcal I} = \{s \in

361: S_{\mathcal I} | {\mathcal I}, s \models \phi\}$.  Again, when the

362: intended interpretation is clear, we shall often simply write $s

363: \models \phi$.

364: 

365: Given interpretation ${\mathcal I}$ and an initial

366: state $s_{0}$, we shall interpret every mechanism $\gamma$ as a game form

367: of almost-perfect information $G(\gamma, s_{0}, {\mathcal I})$.

368: Let $\cfg$ denote the set of {\em configurations}, i.e., the set of

369: all pairs $\l \gamma, s \r$ where $\gamma$ is a mechanism or the empty

370: mechanism $\Lambda$, and $s$ is a state. We define a transition

371: relation $\mv{A} \subseteq \cfg \times \cfg$ for $A \subseteq Ags$ such that

372: $c \mv{A} c'$ states that the game can proceed from $c$ to $c'$ provided the agents

373: $A$ make some choice/move. In case the move does not require any agent to make

374: a choice, we will have $A = \emptyset$. In the standard

375: way (see e.g. \cite{Nielson}), we define the $\mv{A}$ relations inductively as

376: the smallest sets satisfying the following axioms and inference rules, the only

377: novelty here being the definition for $\mathtt{ch}_A$:

378: \[ \begin{array}{|cc|}

379: \hline

380:     \multicolumn{2}{|c|}{

381:     \l x:=t, s \r  \mv{\emptyset}  \l \Lambda, s^x_t \r} \\[5ex]

382: 

383:     \multicolumn{2}{|c|}{\l \mathtt{ch}_A(X), s \r

384:      \mv{A}

385:     \l \Lambda, s' \r \mbox{ where $s'(y)=s(y)$ for all $y \not\in X$}} \\[5ex]

386: 

387:     \dfrac{\l \gamma_{1}, s \r  \mv{A}  \l \Lambda, s' \r}{\l \gamma_{1}

388:     ; \gamma_{2} , s \r  \mv{A}  \l \gamma_{2}, s' \r} &

389:     \dfrac{\l \gamma_{1}, s \r  \mv{A}  \l \gamma_{1}' , s' \r}{\l

390:     \gamma_{1} ; \gamma_{2}, s \r  \mv{A}  \l \gamma_{1}' ; \gamma_{2}, s' \r}

391:     \\[5ex]

392: 

393: 

394:     \multicolumn{2}{|c|}{\dfrac{{\mathcal I},s \models B}{\l \mathtt{if} \: B \:

395:     \mathtt{then} \: \gamma_{1} \: \mathtt{else} \: \gamma_{2}, s \r

396:     \mv{\emptyset}  \l \gamma_{1}, s \r}} \\[5ex]

397:     \multicolumn{2}{|c|}{\dfrac{{\mathcal I},s \not\models B}{\l \mathtt{if} \: B \:

398:     \mathtt{then} \: \gamma_{1} \: \mathtt{else} \: \gamma_{2}, s \r

399:     \mv{\emptyset}  \l \gamma_{2}, s \r}} \\[5ex]

400: 

401:     \dfrac{{\mathcal I},s \not\models B}{\l \mathtt{while} \: B \:

402:     \mathtt{do} \: \gamma, s \r  \mv{\emptyset}  \l \Lambda, s \r} &

403:     \dfrac{{\mathcal I},s \models B}{\l \mathtt{while} \: B \: \mathtt{do}

404:     \: \gamma, s \r  \mv{\emptyset}  \l \gamma ; \mathtt{while} \: B \: \mathtt{do}

405:     \: \gamma, s \r}

406: \\[3ex]  \hline

407: \end{array} \]

408: where $s^x_t(y)=s(y)$ for $y \neq x$ and $s^x_t(x)=t^{{\mathcal I}, s}$, the

409: interpretation of $t$ in ${\mathcal I}$ at $s$.

410: 

411: Let $\cfg^*$ be the set of all finite nonempty sequences of

412: configurations $c_0, c_1,$ $\ldots, c_n$ such that $c_i = \l

413: \gamma_i, s_i \r$ and

414: \[ \l \gamma_0, s_0 \r \mv{A_1} \l \gamma_1, s_1 \r \mv{A_2} \ldots

415: \mv{A_{n}} \l \gamma_n, s_n \r ,\] and let $\cfg^*_a$ be those

416: sequences which end in a configuration $c_n$ for which there is

417: some configuration $c_{n+1}$ and set $A \subseteq Ags$ such that

418: $c_n \mv{A} c_{n+1}$ and $a \in A$. Infinite configuration

419: sequences as well as finite configuration sequences $c_0, \ldots,

420: c_n$ for which there is no $c_{n+1}$ and $A$ such that $c_n \mv{A}

421: c_{n+1}$ are called {\em terminal}, and we denote the set of

422: terminal sequences as $\cfg^t$.

423: 

424: The move relations give rise to the game tree or {\em semi-game}

425: $G(\gamma, s_{0}, {\mathcal I})$ which starts at the initial

426: position/configuration $\l \gamma, s_{0} \r$. We interpret

427: $\cfg^*$ as the set of (partial) histories of the game, where each

428: agent $a$ gets to move at the positions which are in $\cfg^*_a$.

429: Note that we talk of a tree, since we can think of possible loops

430: as infinite branches. While we shall usually refer to $G(\gamma,

431: s_0, {\mathcal I})$ as a game (omitting the ``semi''), note that a

432: semi-game lacks a link between runs/histories and preferences, for

433: although ${\mathcal I}$ does contain information about the

434: players' preferences over outcomes, the triple $G$ does not have

435: any mapping between histories of the game and outcomes. Such a

436: mapping $\widehat{o}$ will be added shortly.

437: 

438: A {\em strategy} for agent $a$ in semi-game $G(\gamma_0, s_{0}, {\mathcal I})$ is a

439: function $\sigma^{a} : \cfg^*_a \rightarrow D_{\mathcal I}$.

440: Given a strategy profile  $\sigma = (\sigma^1, \ldots, \sigma^n)$, i.e., a strategy

441: $\sigma^{a}$ for every agent $a \in Ags$, we obtain

442: a unique (possibly infinite) {\em run} which we denote

443: as $run(\sigma)$, i.e., a maximal sequence of

444: configurations

445: \[ \l \gamma_0, s_0 \r \mv{A_1} \l \gamma_1, s_1 \r \mv{A_2} \ldots \]

446: where $\l \gamma_0, s_0 \r$ is the initial configuration, and for

447: all $A_{k+1} \neq \emptyset$ we have $s_{k+1}(x_i) = \sigma^i(\l

448: \gamma_0, s_0 \r, \ldots, \l \gamma_k, s_k \r)$ for all $i \in A$,

449: and $s_{k+1}(y)=s_k(y)$ otherwise. If $run(\sigma)$ is finite, we

450: let $s_{\sigma}$ denote the state associated to the last

451: configuration of $run(\sigma)$.

452: 

453: %

454: \subsection*{Preferences, Predicates, and Strategic Equilibria}

455: %

456: 

457: Each agent has certain preferences over the various possible

458: outcomes of the mechanism.  Given interpretation ${\mathcal I}$

459: and two outcomes $o,o' {\in} D_{\mathcal I}$, agent $i$ prefers

460: $o$ at least as much as $o'$ whenever $o \geq_i^{\mathcal I} o'$

461: holds. Often, the elements in $D_{\mathcal I}$ will be elements of

462: some product space, so that, e.g., $(o_1, o_2) \in \mathbb{R}

463: \times \mathbb{R}$ will yield outcome $o_1$ for player 1 and

464: outcome $o_2$ for player 2, where $(o_1,o_2) \geq_i (o'_1, o'_2)$

465: iff $o_i \geq o'_i$.

466: 

467: An {\em outcome function} $\widehat{o}: \cfg^t \rightarrow

468: D_{\mathcal I}$ assigns an outcome to every terminal history, and

469: we let $\widehat{O}$ denote the the set of all outcome functions.

470: Given a semi-game $G(\gamma, s, {\mathcal I})$ we then obtain a

471: {\em game} $G(\gamma, s, {\mathcal I}, \widehat{o})$, where for

472: each terminal sequence of configurations $\bar{c}$ the associated

473: outcome is $\widehat{o}(\bar{c})$, and agent $i$ prefers

474: $\bar{c}_1$ to $\bar{c}_2$ iff $\widehat{o}(\bar{c}_1) \geq_i

475: \widehat{o}(\bar{c}_2)$. Given profile $\sigma$, we usually write

476: $\widehat{o}(\sigma)$ instead of $\widehat{o}(run(\sigma))$, as we

477: shall not be very careful about distinguishing $\sigma$ from

478: $run(\sigma)$.

479: 

480: Subgames of games will play a special role in the equilibrium

481: notion to be defined subsequently. A game $G'(\gamma', s',

482: {\mathcal I}, \widehat{o}|G')$ is a {\em subgame} of a game

483: $G(\gamma, s, {\mathcal I}, \widehat{o})$ iff there is a finite

484: sequence of configurations $ \l \gamma_0, s_0 \r \mv{A_1} \l

485: \gamma_1, s_1 \r \mv{A_2} \ldots \mv{A_n} \l \gamma_n, s_n \r$ for

486: some $n \geq 0$ such that $\l \gamma_0, s_0 \r = \l \gamma, s \r$

487: and $\l \gamma_n, s_n \r = \l \gamma', s' \r$. The outcome function 

488: $\widehat{o}|G'$ is the restriction of $\widehat{o}$ to $G'$, i.e.,

489: $\widehat{o}|G'(\l \gamma_n, s_n \r,\ldots,$ 

490: $\l \gamma_{n+k}, s_{n+k} \r) = \widehat{o}(\l \gamma_0, s_0,

491: \r, \ldots, \l \gamma_n, s_n \r, \ldots, \l \gamma_{n+k}, s_{n+k}

492: \r)$. Similarly for a strategy

493: profile $\sigma$ for $G$, we let $\sigma|G'$ denote its

494: restriction to $G'$, where $\sigma^a|G'(\l \gamma_n, s_n \r,$

495: $\ldots, \l \gamma_{n+k}, s_{n+k} \r) = \sigma^a(\l \gamma_0, s_0,

496: \r, \ldots, \l \gamma_n, s_n \r, \ldots, \l \gamma_{n+k}, s_{n+k}

497: \r)$.

498: 

499: Now that we have defined how executions of mechanisms give rise to

500: game trees, we can apply two well-known equilibrium notions from

501: game theory (see, e.g., \cite{Osborne} for a discussion of these

502: notions). Given a strategy profile $\sigma = (\sigma^1, \ldots,

503: \sigma^n)$ and a strategy $\tau^i$ for player $i$, let $(\tau^i,

504: \sigma^{-i})$ denote the modified strategy profile $(\sigma^1,

505: \ldots, \sigma^{i-1}, \tau^i, \sigma^{i+1}, \ldots, \sigma^n)$.

506: Furthermore, let $\sigma {\sim_{i}} \tau$ denote that the strategy

507: profiles $\sigma$ and $\tau$ differ at most regarding the strategy

508: prescribed for player $i$. Considering any game $G(\gamma,s,

509: {\mathcal I}, \widehat{o})$, we call a strategy profile $\sigma$ a

510: {\em Nash equilibrium} (NE) in $G$ iff for all agents $i$ and

511: strategies $\tau^i$ we have $\widehat{o}(\sigma)

512: \geq_{i}^{\mathcal I} \widehat{o}((\tau^{i}, \sigma^{-i}))$.

513: Furthermore, $\sigma$ is a {\em subgame-perfect equilibrium} (SPE)

514: iff for every subgame $G'$ of $G$, $\sigma|G'$ is a Nash

515: equilibrium in $G'$.

516: 

517: \bigskip

518: 

519: We shall usually obtain an outcome function $\widehat{o}$ from an

520: extended predicate, to be explained now. Given a state 

521: $s: MV \rightarrow D_{\mathcal

522: I}$ and an outcome $o \in D_{\mathcal I}$, we call $(s,o)$ an {\em

523: extended state}, or {\em e-state} for short. A {\em predicate} on

524: ${\mathcal I}$ is simply a set of states $P \subseteq S_{\mathcal

525: I}$, and hence every FOL formula $\phi$ containing only variables

526: of $MV$ gives rise to a predicate $\phi^{\mathcal I}$. Similarly,

527: an {\em extended predicate}, or {\em e-predicate} for short, is a

528: set of $e$-states $P \subseteq S_{\mathcal I} \times D_{\mathcal

529: I}$, and every FOL formula which contains variables of $MV$ plus a

530: new outcome variable $x_o \not\in MV$ gives rise to an

531: e-predicate. We say that e-predicate $P$ is {\em functional} iff for every $s

532: {\in} S_{\mathcal I}$ there exists a unique $o {\in} D_{\mathcal

533: I}$ such that $(s,o) {\in} P$. Given two predicates (or

534: alternatively, two e-predicates), intersection, complementation,

535: etc.\ can be defined simply set-theoretically. Given a predicate

536: $P_{1}$ and an e-predicate $P_{2}$, however, we define $P_{1} \cap

537: P_{2} = \{(s,o) \in P_{2} | s \in P_{1}\}$.

538: 

539: Games can be obtained from extended predicates as follows: Given

540: semi-game $G(\gamma, s, {\mathcal I})$ and e-predicate $Q$, let

541: $\widehat{O}_Q$ contain all the outcome functions $\widehat{o}$ 

542: which assign an outcome satisfying $Q$ to every finite history, i.e.,

543: \[ \widehat{O}_Q = \{\widehat{o} \in \widehat{O} \; | \;

544: \forall run(\sigma) \in \cfg^t: \; \mbox{ if $run(\sigma)$ is

545: finite then } (s_{\sigma}, \widehat{o}(\sigma)) \in Q\}.\]

546: Note that in general,

547: $\widehat{O}_Q$ may be empty or contain multiple outcome

548: assignments. But given e-predicate $Q$ and some $\widehat{o}_Q \in

549: \widehat{O}_Q$, we are able to turn the semi-game $G(\gamma,s,{\mathcal I})$

550: into a game $G(\gamma, s, {\mathcal I}, \widehat{o}_Q)$.

551: 

552: %

553: %--------------------------------------------------------

554: %

555: \section{Mechanism Correctness}

556: \label{mech-des}

557: %

558: %--------------------------------------------------------

559: %

560: 

561: \subsection{Hoare Logic: From Programs to Games}

562: \label{ext-int}

563: 

564: Hoare in \cite{Hoare-logic} introduced correctness assertions of

565: the form $\{P\}\gamma \{Q\}$, where $\gamma$ is a program and $P$

566: and $Q$ are predicates. The intended interpretation of this

567: assertion is that in every state which satisfies $P$, any

568: terminating execution of program $\gamma$ ends in a state which

569: satisfies $Q$. In this paper, we shall extend this approach to

570: reason about the correctness of game-theoretic mechanisms under

571: subgame-perfect equilibria.

572: 

573: In lifting standard Hoare triples to games we generalise them in

574: two ways. We can view the postcondition $Q$ as

575: specifying the winning condition for the game, i.e., all plays of

576: the game ending in a state which satisfies $Q$ are a win, all

577: others a loss. Note that under the partial correctness reading,

578: infinite runs are in fact also treated as wins. Our first

579: generalisation consists of moving from simple win/loss situations,

580: represented by predicates, to general preference structures. This

581: is achieved by moving from predicates to e-predicates which also

582: specify the outcome or payoff at a state. Second and more

583: importantly, we move from simple claims about the existence of a

584: strategy profile satisfying the postcondition to more refined

585: claims about the existence of a strategy profile which has an

586: equilibrium property. This equilibrium property is generally quite

587: complex, and it is the complexity of this equilibrium property

588: which can present a challenge to compositionality, in particular

589: to the Hoare inference rule for composing two programs/games (see

590: lemma \ref{sound-comp} below).

591: 

592: Before defining our mechanism correctness assertions

593: $\{P\}\gamma\{Q\}$, it is important to point out that we are

594: following an {\em extensional} rather than an {\em intensional}

595: approach (see also \cite{Nielson}). We assume that pre- and

596: postconditions are predicates, i.e., semantic objects rather than

597: formulas of some logical language. Naturally, this means that the

598: calculus we present later is not fully syntactic. In the

599: intensional approach, however, one runs into the problem of {\em

600: expressiveness}, since it may happen that under a given

601: interpretation the logical language is not rich enough to express

602: all the preconditions needed. This complicates completeness proofs

603: considerably, due to the need for an arithmetisation of syntax

604: (G\"{o}delisation), etc. Furthermore, we feel that this extra

605: work yields more insights about the logic used for the assertion

606: language (usually first-order logic) than about the game theoretic

607: mechanisms and their equilibria, which is what we are interested

608: in here.

609: 

610: Due to its fully syntactic nature, it does seem likely that the

611: automated verification of mechanisms would benefit from using the

612: intensional approach, and we do intend to investigate this

613: approach in the future (see also comments in the last section).

614: However, note that in contrast to most computer programs whose

615: domain of computation contains at least the natural numbers,

616: mechanisms like voting procedures often use a finite domain

617: of computation, e.g., because there is only a small number of

618: possible candidates running for president. In such cases, it may

619: in fact be easier to do automatic verification using the

620: extensions of the predicates directly. Second, even if this is not

621: the case, the best logic to choose for automated verification may

622: very much depend on the class of mechanisms under consideration,

623: the theorem prover to be used, etc. Hence, for our present

624: purposes, we decide to postpone these issues since they are more 

625: relevant for implementation, and the extensional approach conveniently

626: allows us to do so.

627: 

628: 

629: \subsection{Mechanism Correctness and Implementation}

630: 

631: Assume that we are given some interpretation ${\mathcal I}$, a

632: mechanism $\gamma$, and e-predicates $P$ and $Q$. Then we say that

633: $\{P\} \gamma \{Q\}$ is {\em valid} in ${\mathcal I}$, denoted as

634: $ {\mathcal I} \models \{P\} \gamma \{Q\}$, iff

635: \begin{quote}

636:     for every $(s,o) \in P$, there is an outcome function

637:     $\widehat{o} \in \widehat{O}_Q$ and a strategy profile $\sigma$ such

638:     that $\sigma$ is an SPE in $G(\gamma, s, {\mathcal I},

639:     \widehat{o})$ and $\widehat{o}(\sigma)=o$.

640: \end{quote}

641: 

642: The notion defined indeed generalises the standard partial

643: correctness assertions of Hoare in the following way: Given an

644: arbitrary element $d \in D_{\mathcal I}$ and a predicate $P

645: \subseteq S_{\mathcal I}$, let $P^* = \{(s,d) | s \in P\}$. Then

646: given any program $\gamma \in \mbox{MPL(PRG)}$ and predicates $P$

647: and $Q$, the partial correctness assertion $\{P\} \gamma \{Q\}$

648: holds in interpretation ${\mathcal I}$ iff ${\mathcal I} \models

649: \{P^*\} \gamma \{Q^*\}$.

650: 

651: In order to link our mechanism correctness assertion to the

652: game-theoretic literature on mechanism design and implementation

653: theory \cite{Osborne,Moore:implementation,RoE}, we shall define

654: our version of the mechanism design problem more formally. Given a

655: set of possible outcomes $D_{\mathcal I}$ of the mechanism and the

656: set of preference profiles over $D_{\mathcal I}$, a {\em social

657: choice correspondence} $f$ maps a preference profile $(\geq_i)_{i

658: \in Ags}$ to a set of outcomes $X \subseteq D_{\mathcal I}$. The

659: idea is that at preference profile $(\geq_i)_{i \in Ags}$, society

660: or the mechanism designer wants one of the outcomes in

661: $f((\geq_i)_{i \in Ags})$ to be implemented or achieved. In case

662: $f((\geq_i)_{i \in Ags})$ is empty, society is indifferent to the

663: outcome actually realised. The mechanism design problem is to find

664: a mechanism which implements the social choice correspondence in a

665: non-centralised manner, i.e., no matter what the preferences of

666: the agents are, self-interested agents will have an incentive to

667: play so that the outcome intended by the designer will obtain. We

668: shall now see how this problem can be translated into our

669: mechanism correctness assertions.

670: 

671: For a preference profile $(\geq_i)_{i \in Ags}$ where each $\geq_i

672: \subseteq D_{\mathcal I} \times D_{\mathcal I}$, let ${\mathcal

673: I}[(\geq_i)_{i \in Ags}]$ denote the model which is obtained from

674: ${\mathcal I}$ by

675: replacing the interpretation of the preference relations by the

676: $\geq_i$. Furthermore, for a given social choice correspondence

677: $f$, let $f^*(x)= \{(s,o) \in S_{\mathcal I} \times D_{\mathcal

678: I}| o \in f(x)\}$, and let $Q$ be any functional e-predicate. Then

679: we say that the pair $(\gamma,Q)$ {\em SPE-implements} a social

680: choice correspondence $f$ iff for all preference profiles

681: $(\geq_i)_{i \in Ags}$ we have

682: \[{\mathcal I}[(\geq_i)_{i \in Ags}] \models \{f^*((\geq_i)_{i \in

683: Ags})\} \gamma \{Q\}.\] To see what this statement actually

684: expresses, let us unpack the definition: $(\gamma, Q)$

685: SPE-implements social choice correspondence $f$ iff

686: \begin{quote}

687: for all preference profiles $(\geq_i)_{i \in Ags}$, for all states

688: $s \in S_{\mathcal I}$, and for all $o \in f((\geq_i)_{i \in

689: Ags})$, there is some $\widehat{o} \in \widehat{O}_Q$ and some

690: strategy profile $\sigma$ such that $\sigma$ is an SPE for

691: $G(\gamma, s, {\mathcal I}[(\geq_i)_{i \in Ags}], \widehat{o})$

692: and $\widehat{o}(\sigma)=o$.

693: \end{quote}

694: Note that this notion of implementation is a weak notion which

695: does not ask every but only some equilibrium profile to yield the

696: desired outcome, hence strictly speaking we are dealing with

697: mechanism design rather than implementation theory. In the

698: remainder of this section, we shall look at a few concrete

699: examples of mechanism design.

700: 

701: %

702: \subsection{Auctions}

703: \label{auctions}

704: %

705: 

706: Over the domain of natural numbers, the mechanism

707: \[\mathtt{ch}_{\{1,2\}}(\{x_1,x_2\})\] can represent a sealed-bid

708: auction where the two players simultaneously choose their bids, e.g.,

709: in euros, in order to obtain some desirable object, say a piano.

710: Since this game is atomic, the notions of SPE and NE coincide, and

711: hence we can phrase the existence of Nash equilibria using the

712: correctness notion defined earlier.

713: 

714: Consider the case of a second-price auction where the player

715: who makes the highest bid has to pay the price of the loser's bid.

716: We assume that our model ${\mathcal I}$ has the natural

717: numbers as its domain, and contains two constants $v_1$ and $v_2$

718: whose values denote the private valuations of the players. Instead

719: of representing outcomes as pairs $o=(o_1,o_2)$ we shall assume

720: that there are two outcome variables $o_1$ and $o_2$ which

721: determine the payoffs of player 1 and 2, respectively. A player's payoff 

722: is 0 if he fails to obtain the piano, and his valuation minus the other player's

723: bid if he does obtain the piano. The

724: preference ordering over elements of the domain is the obvious

725: one: $d_1 \geq_i d_2$ iff $d_1 \geq d_2$. Note that a player's preference relation

726: is completely determined by his valuation. 

727: 

728: The postcondition of

729: the second-price auction is the e-predicate expressed by the following formula

730: $\psi$:

731: \[ (x_1 \geq x_2 \rightarrow (o_1=v_1-x_2 \wedge o_2=0)) \wedge

732:     (x_1 < x_2 \rightarrow (o_1=0 \wedge o_2=v_2-x_1)) \]

733: It is easy to see that this postcondition expresses the payoffs of

734: the players in the second-price auction. Note also that the postcondition

735: fomalises the tie-breaking rule which assigns the object to player 1 in

736: case the bids are equal. Now consider the

737: e-predicate expressed by the following formula $\phi$:

738: \[ (v_1 \geq v_2 \rightarrow (o_1=v_1-v_2 \wedge o_2=0)) \wedge

739:     (v_1 < v_2 \rightarrow (o_1=0 \wedge o_2=v_2-v_1)) \]

740: We claim that ${\mathcal I} \models \{\phi^{\mathcal I}\}

741: \mathtt{ch}_{\{1,2\}}(\{x_1,x_2\}) \{\psi^{\mathcal I}\}$: If player

742: 1's valuation is at least as high as player 2's valuation, then the

743: auction has a Nash-equilibrium in which player 2's payoff is 0 and

744: player 1's payoff is the difference between the valuations.  Similarly

745: in case player 2's valuation is higher.

746: 

747: To see why this is so, note that it is a well-known result in game

748: theory (see, e.g., \cite{Osborne}) that in a second-price

749: sealed-bid auction, bidding your valuation results in a Nash

750: equilibrium (in fact, it is even a dominant strategy). Hence, if each

751: player bids $x_i=v_i$, the outcomes are the ones specified by

752: $\phi$, and the strategies are in equilibrium. 

753: 

754: In fact, from the validity of $\{\phi^{\mathcal I}\}

755: \mathtt{ch}_{\{1,2\}}(\{x_1,x_2\}) \{\psi^{\mathcal I}\}$

756: we can derive

757: some information about the nature of the winning strategies. For suppose

758: w.l.o.g.\ that $v_1 \geq v_2$. Using precondition $\phi$, we know that 

759: $o_1 = v_1 - v_2$ and $o_2 = 0$. Now we can distinguish two cases: In the

760: first case, we have a Nash equilibrium (and hence also a SPE) where player 1 bids 

761: less than player 2, i.e., $x_1 < x_2$. Now using the postcondition $\psi$

762: and the fact that the outcome variables $o_1$ and $o_2$ are never changed by 

763: any mechanism, we know that $o_1= 0$ and $o_2 = v_2 - x_1$. Hence $x_1 = v_2 = v_1$

764: and $x_2 > v_2 = v_1$, i.e., the players' valuations must be the same and

765: player 2 must bid higher than his valuation. It is easy to check that these bids

766: indeed constitute a Nash equilibrium. 

767: In the second case, we have a Nash equilibrium with $x_1 \geq x_2$. Again using

768: the postcondition, $o_2= 0$ and $o_1 = v_1 - x_2$. Hence, $x_2 = v_2$ and

769: $x_1 \geq v_2$. Thus, player 2 bids his valuation and player 1 bids at least player

770: 2's valuation. Again, these bid combinations all constitute Nash equilibria, and

771: our intended equilibrium, where each player bids his own valuation, 

772: is included in this second case.

773: 

774: In a private-value environment, a sealed-bid second-price auction is essentially

775: outcome equivalent with an English auction, where bidders keep increasing the price

776: over a number of bidding rounds until there is no more bidder who wants to 

777: obtain the object for a higher price.  In an English auction, bidding

778: slightly more than the second-highest valuation will suffice to obtain

779: the object.  Analogously, we can consider a sealed-bid first-price

780: auction where the winner has to pay his own bid rather than the

781: second-highest bid.  The first-price auction is essentially outcome

782: equivalent to the Dutch (or descending) auction, where the auctioneer

783: continues to lower the price of the object until a player decides to

784: take the object for the current price.  If the players' valuations are

785: not public, the safe strategy is to stop the auction just below one's

786: valuation, the result being that the player with the highest valuation

787: will obtain the object for the price of almost his valuation.

788: 

789: Contrary to these results, we shall show in section \ref{apps} that 

790: from the perspective of SPEs, the Dutch auction is also similar to

791: a sealed-bid second-price auction. In order to apply SPEs as a solution concept, 

792: we need to assume that players' preferences are public. In an auction, this

793: means that players know each other's valuations. In this case, however, if

794: $v_1 > v_2$, player 1 can wait longer before calling out to stop the

795: Dutch auction, he can wait until the prices reach $v_2$ or just above. 

796: Hence, when preferences are public, it would seem that Dutch auction

797: and second-price auction share a SPE. We will verify this claim in

798: section \ref{apps}, thereby also obtaining the precise conditions for

799: this equivalence.

800: 

801: Finally, a further remark relating auction preconditions to the notion of 

802: SPE-implementation.

803: In a second-price auction, we want to SPE-implement the social choice correspondence

804: $f$ which assigns to a preference profile $(v_1,v_2)$ the outcome

805: $(o_1,o_2)$ with $o_1=v_1 - v_2$ and $o_2=0$ in case $v_1 \geq v_2$ and

806: $o_2=v_2 - v_1$ and $o_1=0$ in case $v_1 < v_2$. While the precondition $\phi$

807: given above does capture this social choice correspondence in an intuitive sense,

808: note that it is not the precondition used in our definition of SPE-implementation.

809: This is because SPE-implementation, as we defined it, requires a correctness

810: claim for each preference profile separately. In contrast, our precondition $\phi$

811: covers all preference profiles in one precondition, since it conditions the assigned

812: outcomes on the relationship between the valuation constants. This formulation

813: leads to a much more general result and hence is usually preferable. In the next

814: section, we shall present an example using the notion of SPE-implementation

815: literally.

816: 

817: 

818: %

819: \subsection{Solomon's Dilemma}

820: \label{sol}

821: %

822: 

823: The biblical dilemma of Solomon (1 Kings 3:16-28) has often been

824: used to illustrate the basic idea of implementation theory

825: \cite{Osborne,Moore:implementation}. In the same spirit, we shall

826: use it here to illustrate our notion of SPE-implementation. The

827: game-theorist will get the additional benefit of seeing a

828: well-known example of implementation theory translated into our

829: framework. Solomon's dilemma is that two women have come

830: before him with a small child, both claiming to be the mother of

831: the child.

832: 

833: \begin{quote}

834:     He sent for a sword, and when it was brought, he said,

835:     ``Cut the living child in two and give each woman half of it.''

836:     The real mother, her heart full of love for her son, said to

837:     the king, ``Please, Your Majesty, don't kill the child! Give it

838:     to her!'' But the other woman said, ``Don't give it to either of

839:     us; go on and cut it in two.'' Then Solomon said, ``Don't kill the

840:     child! Give it to the first woman, she is its real mother.''

841: \end{quote}

842: 

843: The story exemplifies the need for a mechanism very well: Since

844: Solomon does not know who the real mother is (i.e., he does not

845: know the women's preferences), he cannot impose the outcome of his

846: choice function directly. Rather, he needs to devise a mechanism

847: which will provide an incentive to the women to reveal this

848: information to him.

849: 

850: To mathematically model Solomon's situation, we consider three

851: outcomes: $a$ (baby is given to Anne, player 1), $b$ (baby is

852: given to Bess, player 2), and $c$ (baby is cut in two). Solomon

853: has to consider two possible situations: In case Anne is the real

854: mother, the preference profile is given by $\theta_1$, in case

855: Bess is the real mother, the preference profile is $\theta_2$.

856: \[ \begin{array}{rccc}

857: \theta_1: &  a >_1 b >_1 c & \mbox{ and } & b >_2 c >_2 a \\

858: \theta_2: & a >_1 c >_1 b & \mbox{ and } & b >_2 a >_2 c

859: \end{array} \]

860: Solomon's problem is to find a mechanism which implements the

861: social choice correspondence $f$ for which $f(\theta_1)=\{a\}$ and

862: $f(\theta_2)=\{b\}$. In spite of Solomon's apparent cleverness, it

863: turns out that $f$ is not Nash-implementable 

864: (see \cite{Moore:implementation} for a proof). However, by slightly

865: modifying the problem, one can obtain an implementation

866: nonetheless.

867: 

868: Let us consider the situation where instead of quarreling about a

869: child, Anne and Bess argue about who is the owner of a painting.

870: Furthermore, we allow Solomon to impose fines on the two women,

871: i.e., we allow for monetary side payments. We can then think of the

872: possible outcomes as triples $(x,m_1,m_2)$, where $x \in

873: \{0,1,2\}$ denotes who obtains the painting (0 denoting that it is

874: cut in two), and $m_i$ denotes the fine player $i$ has to pay to

875: Solomon. Now suppose that the legitimate owner of the paining has

876: valuation $v_H$ and the other woman has valuation $v_L$, where

877: $v_H > v_L > 0$. Then if player $i$ does not get the painting, her

878: payoff is $-m_i$. If she does get the painting, her payoff will be

879: $v_H-m_i$ in case she is the legitimate owner, and $v_L-m_i$

880: otherwise. If player $i$ is the legitimate owner, these payoffs

881: will then induce a preference profile $\theta_i$ in the obvious

882: way. In this new setup, Solomon wishes to implement the social

883: choice rule $f$ for which $f(\theta_i)=\{(i,0,0)\}$, i.e., the

884: painting is given to the legitimate owner and nobody has to pay

885: any fines (we assume here that Solomon does not engage in dispute

886: resolution to make money). More precisely, Solomon is looking for

887: a pair $(\gamma,Q)$ which SPE-implements $f$, i.e., for which

888: \[{\mathcal I}[\theta_1] \models

889: \{o=(1,0,0)\} \gamma \{Q\} \mbox{ and } {\mathcal I}[\theta_2]

890: \models \{o=(2,0,0)\} \gamma \{Q\}.\]

891: 

892: The following mechanism $\gamma$ achieves this goal: First, Anne

893: is asked whether the painting is hers or not. If she says no, the

894: painting is given to Bess and no fines are imposed. Otherwise,

895: Bess is asked the same question. If Bess answers the painting is

896: not hers, it is given to Anne, again without imposing any fines.

897: Finally, in case both players have claimed to be the owner of the

898: painting, Anne is fined a small amount $\varepsilon > 0$ and Bess 

899: gets the painting but has to pay a large amount $M$ for which

900: $v_L < M < v_H$. The mechanism $\gamma$ can be programmed as

901: follows, where we take the real numbers as our domain:

902: \begin{tabbing}

903: $\mathtt{ch}_{\{1\}}(\{x_1\})$; \\

904: $\mathtt{if} \: x_1 > 0 \:$ \= $\mathtt{then} \: owner:=2$  \\

905:     \>      $\mathtt{else} \:$ \= $\mathtt{ch}_{\{2\}}(\{x_2\});$

906:     \\ \>\> $\mathtt{if} \: x_2 > 0 \: \mathtt{then} \: owner:=1 \: \mathtt{else} \: owner:=0$

907: \end{tabbing}

908: As for the payoff specification, let $Q$ be the e-predicate

909: corresponding to the following formula:

910: \[ \begin{array}{rl}

911: & (owner=1 \rightarrow o=(1,0,0)) \\ \wedge & (owner=2 \rightarrow

912: o=(2,0,0)) \\ \wedge & (owner=0 \rightarrow o=(2,\varepsilon,M))

913: \end{array} \]

914: Game theoretically, it is easy to verify that for preference

915: profile $\theta_i$, the following game form has a subgame-perfect

916: equilibrium yielding outcome $(i,0,0)$. We will return to this

917: example in section \ref{apps} and give a formal verification of

918: this mechanism.

919: 

920: \begin{picture}(100,50)

921: \put(80,-10){\mbox{\special{psfile=solomon.eps

922:     hscale=80

923:     vscale=80}}}

924: \end{picture}

925: 

926: %

927: %--------------------------------------------------------

928: %

929: \section{Axiomatic Mechanism Verification}

930: \label{calculus}

931: %

932: %--------------------------------------------------------

933: %

934: 

935: %

936: \subsection{A Hoare-style Calculus}

937: %

938: 

939: Below we present a calculus for deriving the correctness

940: assertions we introduced above. Note that the calculus is a

941: natural generalisation of the standard Hoare calculus, where the

942: only addition is an axiom for the new construct $\mathtt{ch}_A$.

943: Given e-predicate $P$, we let $P[x/t] = \{(s,o) \in S_{\mathcal I}

944: \times D_{\mathcal I} | (s^x_t,o) \in P\}$.

945: 

946: \[ \begin{array}{|cr|}

947: \hline & \\

948: \{Q[x/t]\} x:=t \{Q\} & \mbox{(ass.)}\\[3ex]

949: 

950: \{wpre(ch_{A}(X), Q, {\mathcal I})\} 

951: ch_{A}(X) \{Q\} & \mbox{(choice)} \\[3ex]

952: 

953: \dfrac{\{P\} \gamma_1 \{R\} \;\;\; \{R\} \gamma_2 \{Q\}}{\{P\}

954: \gamma_1 ; \gamma_2 \{Q\}} & \mbox{(comp.)} \\[3ex]

955: 

956: \dfrac{\{P \cap B^{\mathcal I}\} \gamma_1 \{Q\} \;\;\; \{P \cap

957: \overline{B^{\mathcal I}}\} \gamma_2 \{Q\}}{\{P\} \mathtt{if} \: B

958: \: \mathtt{then} \: \gamma_{1} \: \mathtt{else} \:

959: \gamma_{2} \{Q\}} & \mbox{(if)} \\[5ex]

960: 

961: \dfrac{\{P \cap B^{\mathcal I}\} \gamma \{P\}}{\{P\}

962: \mathtt{while} \: B \: \mathtt{do} \: \gamma \{P \cap

963: \overline{B^{\mathcal

964: I}}\}} & \mbox{(while)} \\[3ex]

965: 

966: \dfrac{P \subseteq P', \; \{P'\} \gamma \{Q'\}, \; Q' \subseteq

967: Q}{\{P\} \gamma \{Q\}}

968: & \mbox{(l.c.)} \\[3ex] \hline

969: \end{array} \]

970: In the choice axiom, $wpre(\gamma, Q, {\mathcal I})$ refers to the {\em weakest precondition}

971: of $Q$ under $\gamma$. Given interpretation ${\mathcal I}$,

972: mechanism $\gamma$, and e-predicate $Q$, we define $wpre$ as

973: follows:

974: \[ \begin{array}{lcl}

975:     wpre(\gamma, Q, {\mathcal I}) & = & \{(s,o) \in S_{\mathcal I} \times D_{\mathcal I}\:

976:        | \: \exists \widehat{o} \in \widehat{O}_{Q} \exists \sigma: \;

977:     \sigma \mbox{ is an SPE in } \\ && \;\;\; G(\gamma, s, {\mathcal I},

978:     \widehat{o}) \mbox{ and } \widehat{o}(\sigma)=o\}

979: \end{array} \]

980: Note that by definition, ${\mathcal I} \models \{wpre(\gamma, Q, {\mathcal

981: I})\} \gamma \{Q\}$, and for every e-predicate $P$ such that

982: ${\mathcal I} \models \{P\} \gamma \{Q\}$, we have $P \subseteq

983: wpre(\gamma, Q, {\mathcal I})$. Weakest preconditions will play an important

984: role in the completeness proof of section \ref{compl}.

985: 

986: Let $\Delta_{\mathcal I}$ be the smallest set of correctness

987: assertions $\{P\} \gamma \{Q\}$ over ${\mathcal I}$ which includes

988: the axioms and is closed under the inference rules above. We shall

989: usually write $\{P\} \gamma \{Q\} \in \Delta_{\mathcal I}$ as

990: ${\mathcal I} \vdash \{P\} \gamma \{Q\}$. In order to gain some intuitions

991: regarding this calculus, the reader may wish to consult section \ref{apps}

992: before proceeding with the subsequent soundness and completeness results.

993: 

994: Before establishing soundness and completeness of the calculus presented,

995: some further comments regarding the choice axiom are in order.  As

996: mentioned, the calculus is extensional in the sense that preconditions and

997: postconditions are semantic rather than syntactic objects, predicates

998: rather than formulas of, say, first-order logic.  As a consequence, we

999: do not get a syntactic proof system, but rather what one might call a

1000: compositional proof methodology.  Hence, while the precondition of the

1001: choice axiom may seem tautological, it still suffices to reduce

1002: reasoning about subgame-perfect equilibria in complex games to

1003: reasoning about Nash equilibria in simple games.  Hence, while we are

1004: still in need of a semantic argument to establish the Nash

1005: equilibrium, it is a simpler semantic argument which applies only to

1006: the simplest game, the atomic choice game.  As the examples in section

1007: \ref{apps} will illustrate, this decomposition is achieved by moving

1008: the complexity from the mechanism into the mechanism's postcondition

1009: or payoff assignment, and it is this which the calculus allows one to

1010: do.  In other words, the complexity is moved from the dynamic to the

1011: static part, from the mechanism to the predicates describing pre- and

1012: postconditions.

1013: 

1014: In verification practice, it turns out that the precondition of the

1015: choice axiom is often rather analogous to the precondition of the

1016: assignment axiom, where Nash equilibrium strategies are substituted

1017: for the choice variables in the precondition.  Slightly more formally,

1018: suppose that the postcondition $Q$ is a functional e-predicate which

1019: simply assigns outcomes based on the choice variables, and that $Q$

1020: only contains these choice variables and no other variables.  An

1021: example of such a postcondition is the postcondition $\psi$ of the

1022: second-price auction discussed in section \ref{auctions}.  Since this

1023: postcondition depends on the state only in terms of the choice

1024: variables, we can say that the weakest precondition of the choice

1025: construct is simply $Q$ where each choice variable $x_{i}$ is replaced

1026: by the Nash equilibrium strategy of player $i$ in the choice game

1027: played in any state with payoffs given by $Q$.  In fact, this is

1028: precisely what happened with the precondition $\phi$ of the second-price

1029: auction where $x_{i}$ is replaced by $v_{i}$.  In general, however,

1030: things are not quite so simple, as the analysis of the Dutch auction

1031: in section \ref{apps} will illustrate.

1032: 

1033: %

1034: \subsection{Soundness}

1035: %

1036: 

1037: The following lemma presents the first of the two most difficult

1038: cases of the subsequent soundness result. It guarantees that

1039: equilibria of subgames can be composed into equilibria of the

1040: supergame.

1041: 

1042: \begin{lemma}[Composition] If we have both ${\mathcal I} \models

1043: \{P\} \gamma_1 \{R\}$ and ${\mathcal I} \models \{R\} \gamma_2

1044: \{Q\}$ then ${\mathcal I} \models \{P\} \gamma_1 ; \gamma_2

1045: \{Q\}$. \label{sound-comp}

1046: \end{lemma}

1047: \begin{proof}

1048:     Let $(s,o) \in P$, and consider $G(\gamma_1 ;

1049:     \gamma_2, s, {\mathcal I})$. By our first

1050:     assumption, there is an outcome function $\widehat{o}_1 \in

1051:     \widehat{O}_{R}$ and a strategy profile $\sigma_1$ such that $\sigma_1$

1052:     is an SPE in $G_1(\gamma_1, s, {\mathcal I}, \widehat{o}_1)$ and

1053:     $\widehat{o}_1(\sigma_1)=o$.

1054: 

1055:     Now for every finite run $\tau_1$ of $G_1$ ending in some terminal

1056:     state $t$ with $\widehat{o}_1(\tau_1)=o_t$, since $(t,o_t) \in

1057:     R$, we know by our second assumption that there is some

1058:     outcome function $\widehat{o}_t \in \widehat{O}_{Q}$ and some strategy

1059:     profile $\sigma_t$ such that $\sigma_t$ is an SPE in

1060:     $G_t(\gamma_2, t, {\mathcal I}, \widehat{o}_t)$ and

1061:     $\widehat{o}_t(\sigma_t)=o_t$. Taken together, $\sigma_1$ and

1062:     the $\sigma_t$ induce a strategy profile $\sigma$ for $G$, and

1063:     similarly $\widehat{o}_1$ (for the infinite runs of $G_1$) and the

1064:     $\widehat{o}_t$ induce an outcome function $\widehat{o} \in

1065:     \widehat{O}_Q$ for $G$. Hence, it remains to show that $\sigma$ 

1066:     is an SPE and that $\widehat{o}(\sigma)=o$.

1067: 

1068:     First, it is easily seen that $\widehat{o}(\sigma)=o$, for

1069:     $\widehat{o}_1(\sigma_1)=o$, and so in case $\sigma_1$ is finite,

1070:     $(s_{\sigma_1},o) \in R$, from which by definition it follows that

1071:     $\widehat{o}(\sigma)=o$. Second, we need to show that $\sigma$

1072:     is an SPE in $G(\gamma_1 ; \gamma_2, s, {\mathcal I},

1073:     \widehat{o})$. So consider any subgame $G'(\pi, t, {\mathcal I})$ of $G$. In

1074:     the easy case, $G'$ will be a subgame of some $G_{t'}$, where $t'$

1075:     is a terminal state in $G_1$, for in this case,

1076:     our second assumption immediately guarantees the equilibrium property.

1077:     In the more complicated case, $G'$ lies partly in $G_1$.  For simplicity,

1078:     we shall for the rest of this argument assume that $\sigma = \sigma_1 {\cdot} \sigma_2$

1079:     refers to its restriction to $G'$.  So consider any strategy profile $\tau_1

1080:     {\cdot} \tau_2$ for $G'$ such that $\sigma = \sigma_1 {\cdot}

1081:     \sigma_2 \sim_i \tau_1 {\cdot} \tau_2 = \tau$, where $\sigma_1$ and $\tau_1$ both

1082:     yield finite runs.  Suppose further

1083:     that $\widehat{o}(\sigma)=o_0$ and $\widehat{o}(\tau)=o_2$, as

1084:     depicted below.

1085: 

1086: \begin{picture}(200,150)

1087: \put(70,10){\mbox{\special{psfile=comp2.eps

1088:     hscale=50

1089:     vscale=50}}}

1090: \put(168,112){$t$}

1091: \put(56,90){$\gamma_1$}

1092: \put(56,30){$\gamma_2$}

1093: \put(151,75){$\sigma_1$}

1094: \put(181,75){$\tau_1$}

1095: \put(146,61){$o_0$}

1096: \put(186,61){$o_1$}

1097: \put(166,61){$\geq_i$}

1098: 

1099: \put(127,15){$\sigma_2$}

1100: \put(192,15){$\sigma_2$}

1101: \put(207,15){$\tau_2$}

1102: 

1103: \put(120,3){$o_0$}

1104: \put(186,3){$o_1$}

1105: \put(202,3){$\geq_i$}

1106: \put(217,3){$o_2$}

1107: \end{picture}

1108: 

1109: \noindent Now supposing that $\widehat{o}(\tau_1 {\cdot}

1110: \sigma_2)=o_1$, we know by definition of $\sigma$ that $o_1 \geq_i

1111: o_2$, and that $\widehat{o}_1(\tau_1)=o_1$. Furthermore, since

1112: $\sigma_1$ was an SPE in $G_1$, we know also that

1113: $\widehat{o}_1(\sigma_1) \geq_i o_1$. Since $o_0 =

1114: \widehat{o}(\sigma)=\widehat{o}_1(\sigma_1)$, we can conclude by

1115: transitivity that $o_0 \geq_i o_2$.

1116: 

1117: Finally, note that the case where either $\sigma_1$ or $\tau_1$ or

1118: both are infinite can be treated by a simplification of the above

1119: argument.

1120: \end{proof}

1121: 

1122: The following lemma isolates the arguments needed to prove the

1123: soundness of the inference rule for iteration. Our assumption that

1124: our model ${\mathcal I}$ contains a uniformly worst element is

1125: needed here.

1126: 

1127: \begin{lemma}

1128: If ${\mathcal I} \models \{P \cap B^{\mathcal I} \} \gamma \{P\}$

1129: then ${\mathcal I} \models \{P\} \mathtt{while} \: B \:

1130: \mathtt{do} \: \gamma \{P \cap \overline{B^{\mathcal I}}\}$.

1131: \label{sound-iteration}

1132: \end{lemma}

1133: \begin{proof}

1134: Roughly speaking, the proof is an iterated application of the

1135: preceding composition lemma, but a few subtleties have to be dealt

1136: with, in particular the possibility of newly arising infinite

1137: runs.

1138: 

1139: Suppose that $(s,o) \in P$. In order to define a strategy $\sigma$

1140: and outcome function $\widehat{o}$ for $G(\mathtt{while} \: B \:

1141: \mathtt{do} \: \gamma, s, {\mathcal I})$, we shall inductively

1142: define strategy profile $\sigma_n$ and outcome function

1143: $\widehat{o}_n$ for game $G_n$ which consists of the first $n$

1144: iterations of game $G$. Game $G_0$ simply consists of

1145: configuration $(\Lambda, s)$, strategy profile $\sigma_0$ consists

1146: of doing nothing, and as an outcome function we take

1147: $\widehat{o}_0((\Lambda,s))=o$. Note that $\widehat{o}_0 \in

1148: \widehat{O}_P$.

1149: 

1150: For the inductive step, define $G_{n+1}$ as $G_n$ where for every

1151: terminal state $(t,o_t) \in P \cap B^{\mathcal I}$ in $G_n$ we

1152: concatenate $G_t(\gamma,t,{\mathcal I})$ to $t$. By our

1153: assumption, for each such terminal state, we have an outcome

1154: function $\widehat{o}_t$ and a SPE strategy profile $\sigma_t$, and we

1155: define $\sigma_{n+1}$ and $\widehat{o}_{n+1}$ in the natural way,

1156: by extending $\sigma_n$ and $\widehat{o}_n$ to $G_{n+1}$ using the

1157: $\widehat{o}_t$ and $\sigma_t$.

1158: 

1159: Now with slight abuse of notation, we can define strategy

1160: profile $\sigma$ and outcome function $\widehat{o}$ for $G$ as

1161: follows: We take $\sigma = \bigcup_i \sigma_i$, i.e., we simply

1162: take the profile generated by the $\sigma_i$. Similarly, we define

1163: $\widehat{o} = \bigcup_i \widehat{o}_i$, i.e., every run $\tau$ of

1164: $G$ which is part of some $G_i$ is evaluated according to

1165: $\widehat{o}_i$. Furthermore, there may be new infinite runs in

1166: $G$ which are not part of any $G_i$, but are instead generated by

1167: an infinite number of plays of $\gamma$ itself. Given such an

1168: infinite run $\tau$, we define $\widehat{o}(\tau)=o_c$ in case

1169: there is some $j$ such that for all $k \geq j$ we have

1170: $\widehat{o}_k(\tau | G_k)=o_c$; otherwise, we let

1171: $\widehat{o}(\tau)=-\infty$. Thus, for infinite runs which

1172: converge on a certain outcome $o_c$, we assign $o_c$ to the run,

1173: and otherwise simply the uniformly worst outcome. Note that

1174: $\widehat{o} \in \widehat{O}_{P \cap \overline{B^{\mathcal I}}}$.

1175: 

1176: Observe first that $\widehat{o}(\sigma)=o$. For we have

1177: $\widehat{o}_1(\sigma_1)=o$,

1178: $\widehat{o}_2(\sigma_2)=\widehat{o}_1(\sigma_1)=o$, etc., and so

1179: in case $\sigma$ is finite, there is some maximal $k$ such that

1180: $\widehat{o}(\sigma)=\widehat{o}_k(\sigma_k)=o$. In case $\sigma$

1181: is infinite, we have a constant and hence converging sequence of

1182: outcomes consisting of $o$ only.

1183: 

1184: Hence, all we need to show is that $\sigma$ is an SPE in

1185: $G(\mathtt{while} \: B \: \mathtt{do} \: \gamma, s, {\mathcal I},

1186: \widehat{o})$. So consider any subgame $G'$ of $G$ and a strategy

1187: $\tau \sim_i \sigma$ such that $\widehat{o}(\sigma)=o_0$ and

1188: $\widehat{o}(\tau)=o_2$. Now the reasoning can proceed along the

1189: lines of the composition lemma and the figure given there: In case

1190: $\tau$ yields a run which lies in $G_k$, we can show by induction

1191: on $k$ that $o_0 \geq_i o_2$, each step involving the reasoning

1192: carried out in the composition lemma. On the other hand, in case

1193: $\tau$ is an infinite run generated by infinitely many

1194: $\gamma$-repetitions, we need to distinguish two cases: In the

1195: easy case where $\widehat{o}(\tau)=-\infty$, the result is

1196: obvious. In the more complicated case, $\widehat{o}(\tau)=o_c$ due

1197: to a sequence of outcomes which converges on $o_c$. Suppose $k$ is

1198: the smallest number for which $\widehat{o}_k(\tau | G_k)=o_c$.

1199: Then again we can apply the reasoning of the composition lemma $k$

1200: times to show that $o_0 \geq_i o_c$.

1201: \end{proof}

1202: 

1203: 

1204: \begin{theorem}[Soundness]

1205: If ${\mathcal I} \vdash \{P\} \gamma \{Q\}$ then ${\mathcal I}

1206: \models \{P\} \gamma \{Q\}$.

1207: \end{theorem}

1208: \begin{proof}

1209:     The proof is by induction on the length of the derivation,

1210: so we start with showing the validity of the axioms.  The soundness of

1211: the $\mathtt{ch}_{A}$ axiom follows by definition.

1212: 

1213: For ${\mathcal I} \vdash \{Q[x/t]\} x:=t \{Q\}$, suppose that

1214: $(s,o) \in Q[x/t]$.  We know that all runs in $G(x:=t,s,{\mathcal

1215: I})$ are finite.  Since no choices need to be made in

1216: $G(x:=t,s,{\mathcal I})$, the one existing strategy profile

1217: $\sigma$ is trivially an equilibrium in $G(x:=t,s,{\mathcal

1218: I},\widehat{o})$ for any outcome function $\widehat{o} \in

1219: \widehat{O}_{Q}$, and in particular for the outcome function

1220: $\widehat{o}$ which assigns $o$ to $\sigma$. Note that since

1221: $(s,o) \in Q[x/t]$, $(s^x_t,o) \in Q$, and hence $\widehat{o} \in

1222: \widehat{O}_Q$.

1223: 

1224: Turning to the inference rules, note that the case of composition

1225: is treated in lemma \ref{sound-comp}, and the logical consequence

1226: rule is an easy consequence of the semantic definition of

1227: ${\mathcal I} \models \{P\} \gamma \{Q\}$. For conditional

1228: branching, the conclusion follows directly from the two premises,

1229: given that $G(\mathtt{if} \: B \: \mathtt{then} \: \gamma_{1} \:

1230: \mathtt{else} \: \gamma_{2}, s, {\mathcal I})$ is either

1231: $G_{1}(\gamma_{1}, s, {\mathcal I})$ or $G_{2}(\gamma_{2}, s,

1232: {\mathcal I})$.  Finally, lemma \ref{sound-iteration} takes care

1233: of iteration.

1234: \end{proof}

1235: 

1236: Note that the soundness result also holds for Nash equilibria: If

1237: in the definition of ${\mathcal I} \models \{P\} \gamma \{Q\}$ we

1238: replace SPE by NE, the above soundness result can still be proved.

1239: This is as it should be, since every subgame-perfect equilibrium

1240: is also a Nash equilibrium.

1241: 

1242: %

1243: \subsection{Completeness}

1244: \label{compl}

1245: %

1246: 

1247: Like in the completeness proof for the standard Hoare calculus,

1248: the notion of a weakest precondition plays an important role for

1249: our calculus as well. The following lemma contains the essential 

1250: argument for the completeness result.

1251: 

1252: \begin{lemma}[Decomposition]

1253: If ${\mathcal I} \models \{P\} \gamma_1;\gamma_2 \{Q\}$, then for

1254: some $R$ we have ${\mathcal I} \models \{P\} \gamma_1 \{R\}$ and

1255: ${\mathcal I} \models \{R\} \gamma_2 \{Q\}$.

1256: \end{lemma}

1257: \begin{proof}

1258: Our assumption is ${\mathcal I} \models \{P\}

1259: \gamma_{1};\gamma_{2} \{Q\}$. Let $R=wpre(\gamma_2, Q, {\mathcal

1260: I})$, then all we need to show is that ${\mathcal I} \models \{P\}

1261: \gamma_1 \{R\}$. So supposing that $(s,o) \in P$, we need to

1262: provide an outcome function $\widehat{o}_1 \in \widehat{O}_R$ and

1263: a strategy profile $\sigma_1$ such that $\sigma_1$ is an SPE in

1264: $G_1(\gamma_1, s, {\mathcal I}, \widehat{o}_1)$ and

1265: $\widehat{o}_1(\sigma_1)=o$.

1266: 

1267: Consider the outcome function $\widehat{o} \in \widehat{O}_Q$ and

1268: the strategy profile $\sigma$ for $G(\gamma_1;\gamma_2, \linebreak

1269: s, {\mathcal I})$ provided by our assumption. We let $\sigma_1 =

1270: \sigma | G_1$. As for the definition of $\widehat{o}_1$, for every

1271: infinite run $\tau$ of $G_1$ we let

1272: $\widehat{o}_1(\tau)=\widehat{o}(\tau)$. If on the other hand

1273: $\tau$ is finite, we define $\widehat{o}_1(\tau)=\widehat{o}(\tau

1274: {\cdot} \sigma_{\tau})$, where $\sigma_{\tau} = \sigma |

1275: G_{\tau}$. By our assumption, we have

1276: $\widehat{o}_1(\sigma_1)=\widehat{o}(\sigma)=o$. Furthermore,

1277: since $(s_{\tau},\widehat{o}(\tau {\cdot} \sigma_{\tau})) \in R$,

1278: $\widehat{o}_1 \in \widehat{O}_R$.

1279: 

1280: Hence, all we need to show is that $\sigma_1$ is an SPE in

1281: $G_1(\gamma_1, s, {\mathcal I}, \widehat{o}_1)$. So consider any

1282: subgame $G'_1=(\pi, t, {\mathcal I}, \widehat{o}_1)$ of $G_1$, and

1283: a strategy profile $\tau_1 \sim_i \sigma_1$, where we take

1284: $\widehat{o}_1(\sigma_1)=o_0$ and $\widehat{o}_1(\tau_1)=o_1$.

1285: Assume first that both $\sigma_1$ and $\tau_1$ are finite.

1286: Considering $G'=(\pi;\gamma_2, t, {\mathcal I}, \widehat{o})$, we

1287: know that there is a profile $\sigma_2$ (derived from $\sigma$)

1288: such that $\sigma_1 {\cdot} \sigma_2$ is an SPE in $G'$ and

1289: $\sigma_1 {\cdot} \sigma_2 \sim_i \tau_1 {\cdot} \sigma_2$. The

1290: situation is depicted below. 

1291: 

1292: \begin{picture}(200,150)

1293: \put(70,10){\mbox{\special{psfile=decomp3.eps

1294:     hscale=50

1295:     vscale=50}}}

1296: \put(168,112){$t$}

1297: \put(56,90){$\gamma_1$}

1298: \put(56,30){$\gamma_2$}

1299: \put(151,75){$\sigma_1$}

1300: \put(181,75){$\tau_1$}

1301: \put(146,61){$o_0$}

1302: \put(186,61){$o_1$}

1303: \put(166,61){$\geq_i$}

1304: 

1305: \put(119,15){$\sigma_2$}

1306: 

1307: \put(207,15){$\sigma_2$}

1308: 

1309: \put(112,3){$o_0$}

1310: 

1311: \put(217,3){$o_1$}

1312: \end{picture}

1313: 

1314: By definition, we know that $\widehat{o}_1(\sigma_1) =

1315: \widehat{o}(\sigma_1 {\cdot} \sigma_2)=o_0$ and

1316: $\widehat{o}_1(\tau_1) = \widehat{o}(\tau_1 {\cdot}

1317: \sigma_2)=o_1$, and hence we must have $o_0 \geq_i o_1$.

1318: 

1319: Note that in case either $\sigma_1$ or $\tau_1$ or both are

1320: infinite, a simplified version of the above argument can be

1321: applied.

1322: \end{proof}

1323: 

1324: The above lemma is what distinguishes subgame-perfect equilibria

1325: from Nash equilibria, since only the former can be decomposed in

1326: the way shown by the decomposition lemma. For Nash equilibria, the

1327: above lemma fails: when defining $\widehat{o}_1$ in the above

1328: proof, we cannot be sure that $\widehat{o}_1 \in \widehat{O}_R$,

1329: since a subprofile of an equilibrium profile may itself not be an

1330: equilibrium profile. Consequently, also the following completeness

1331: result does not hold for Nash equilibria.

1332: 

1333: \begin{theorem}[Completeness]

1334: If ${\mathcal I} \models \{P\}\gamma\{Q\}$ then

1335: ${\mathcal I} \vdash \{P\}\gamma\{Q\}$.

1336: \end{theorem}

1337: \begin{proof}

1338: The proof proceeds by induction on the structure of $\gamma$. For

1339: $x:=t$, note that for any state $s$, the game $G(x:=t, s,

1340: {\mathcal I})$ contains only a single finite run ending in state

1341: $s^x_t$. Observe that $P \subseteq Q[x/t]$: if $(s,o) \in P$,

1342: every run terminates in state $(s^x_t,o) \in Q$, and hence $(s,o)

1343: \in Q[x/t]$. Applying the logical consequence rule to the

1344: assignment axiom, we then obtain ${\mathcal I} \vdash \{P\} x:=t

1345: \{Q\}$.

1346: 

1347: For $\mathtt{ch}_A$, we use the axiom and the logical consequence rule,

1348: and for $\gamma_1 ; \gamma_2$, we can appeal to the decomposition

1349: lemma, induction hypothesis, and the composition rule.  The case of

1350: $\mathtt{if} \: B \: \mathtt{then} \: \gamma_{1} \: \mathtt{else} \:

1351: \gamma_{2}$ is straight-forward, so we only need to deal with the

1352: while-loop.

1353: 

1354: For iteration, suppose that ${\mathcal I} \models \{P\}

1355: \mathtt{while} \: B \: \mathtt{do} \: \gamma \{Q\}$.  Similarly,

1356: to the proof of the decomposition lemma, we let $R =

1357: wpre(\mathtt{while} \: B \: \mathtt{do} \: \gamma, Q, {\mathcal

1358: I})$. First, we shall establish that ${\mathcal I} \models \{R

1359: \cap B^{\mathcal I}\} \gamma \{R\}$.  By definition, we have

1360: ${\mathcal I} \models \{R\} \mathtt{while} \: B \: \mathtt{do} \:

1361: \gamma \{Q\}$.  From this, ${\mathcal I} \models \{R \cap

1362: B^{\mathcal I}\} \gamma ; \mathtt{while} \: B \: \mathtt{do} \:

1363: \gamma \{Q\}$ is easily seen to follow.  Now we can apply the

1364: decomposition lemma: Since the $R$ provided by the proof of the

1365: decomposition lemma is precisely the one we defined above, we can

1366: conclude that ${\mathcal I} \models \{R \cap B^{\mathcal I}\}

1367: \gamma \{R\}$.

1368: 

1369: Now using the induction hypothesis and applying the while-rule, we obtain

1370: \[ {\mathcal I} \vdash \{R\} \mathtt{while} \: B \:

1371:  \mathtt{do} \: \gamma \{R \cap \overline{B^{\mathcal I}}\}.\]

1372: Since $P \subseteq R$ and $R \cap \overline{B^{\mathcal I}}

1373: \subseteq Q$, we can apply the logical consequence rule to derive

1374: ${\mathcal I} \vdash \{P\} \mathtt{while} \: B \: \mathtt{do} \:

1375: \gamma \{Q\}$.

1376: \end{proof}

1377: 

1378: %

1379: %--------------------------------------------------------

1380: %

1381: \section{Applying the Calculus - Some Examples}

1382: \label{apps}

1383: %

1384: %--------------------------------------------------------

1385: %

1386: 

1387: %

1388: \subsection{Solomon's Dilemma}

1389: %

1390: 

1391: Consider again Solomon's 2-stage mechanism given in 

1392: section \ref{sol}, where we will replace the variable

1393: $owner$ by $w$ to save space. We will show one of the two required

1394: correctness claims, namely that ${\mathcal I}[\theta_1] \vdash$

1395: \begin{tabbing}

1396: $\{o=(1,0,0)\}$ \\

1397: $\mathtt{ch}_{\{1\}}(\{x_1\})$; \\

1398: $\mathtt{if} \: x_1 > 0 \:$ \= $\mathtt{then} \: w:=2$  \\

1399:     \>      $\mathtt{else} \:$ \= $\mathtt{ch}_{\{2\}}(\{x_2\});$

1400:     \\ \>\> $\mathtt{if} \: x_2 > 0 \: \mathtt{then} \: w:=1 \: 

1401:           \mathtt{else} \: w:=0$ \\

1402: $\{(w=1 \rightarrow o=(1,0,0)) \wedge  (w=2 \rightarrow

1403: o=(2,0,0)) \wedge (w=0 \rightarrow o=(2,\varepsilon,M))\}$,

1404: \end{tabbing}

1405: corresponding to the situation where player 1 is the real owner of

1406: the painting.  Note that for ease of notation we are now simply

1407: representing (extended) predicates by formulas in first-order logic.

1408: 

1409: Denoting the postcondition by $Q_0$, we have ${\mathcal I}[\theta_1] \vdash

1410: \{o=(2,\varepsilon,M)\} w:=0 \{Q_0\}$ and ${\mathcal I}[\theta_1] \vdash

1411: \{o=(1,0,0)\} w:=1 \{Q_0\}$ using the assignment axiom. Hence, by

1412: the if-rule we have ${\mathcal I}[\theta_1] \vdash$ 

1413: \begin{tabbing}

1414: $\{(x_2 > 0 \rightarrow o=(1,0,0)) \wedge (x_2 \leq 0 \rightarrow o=(2,\varepsilon,M))\}$  

1415: \\ $\mathtt{if} \: x_2 > 0 \: \mathtt{then} \: w:=1 \: \mathtt{else} \: w:=0$ \\

1416: $\{Q_0\}.$

1417: \end{tabbing}

1418: Denote the new precondition by $Q_1$. Since in $\theta_1$, we have $(1,0,0)

1419: >_2 (2,\varepsilon,M)$, we know that when choosing a value for $x_2$, player

1420: 2 will choose the outcome $(1,0,0)$, and hence we have ${\mathcal I}[\theta_1]

1421: \vdash \{o=(1,0,0)\} \mathtt{ch}_{\{2\}}(\{x_2\}) \{Q_1\}$.  On the

1422: other hand, we know by the assignment rule that ${\mathcal

1423: I}[\theta_1] \vdash \{o=(2,0,0)\} w:=2 \{Q_0\}$.  Hence, using the

1424: if-rule and composition, we have ${\mathcal I}[\theta_1] \vdash$

1425: \begin{tabbing}

1426: $\{(x_1 > 0 \rightarrow o=(2,0,0)) \wedge (x_1 \leq 0 \rightarrow o=(1,0,0))\}$\\  

1427: $\mathtt{if} \: x_1 > 0 \:$ \= $\mathtt{then} \: w:=2$  \\

1428:     \>      $\mathtt{else} \:$ \= $\mathtt{ch}_{\{2\}}(\{x_2\});$

1429:     \\ \>\> $\mathtt{if} \: x_2 > 0 \: \mathtt{then} \: w:=1 \: 

1430:           \mathtt{else} \: w:=0$ \\

1431: $\{Q_0\},$

1432: \end{tabbing}

1433: where we denote the new precondition by $Q_2$.

1434: Finally, since $(1,0,0) >_1 (2,0,0)$, player 1 will choose $(1,0,0)$ in an

1435: equilibrium,  and so we have 

1436: ${\mathcal I}[\theta_1] \vdash \{o=(1,0,0)\} \mathtt{ch}_{\{1\}}(\{x_1\}) \{Q_2\}$.

1437: Using the composition rule, we have thereby succeeded in verifying the original claim,

1438: that the 2-stage mechanism does indeed provide an SPE-implementation solving

1439: Solomon's (modified) dilemma.

1440: 

1441: %

1442: \subsection{Auctions}

1443: %

1444: 

1445: \subsubsection*{Second-Price Sealed-Bid Auction}

1446:     

1447: We have already presented the sealed-bid second-price auction in section 

1448: \ref{auctions}.

1449: We argued that in the relevant model ${\mathcal I}$ where two players

1450: have private valuations represented by the constants $v_{1}$ and $v_{2}$, we

1451: have ${\mathcal I} \models$

1452: \begin{tabbing}

1453: $\{(v_1 \geq v_2 \rightarrow (o_1=v_1-v_2 \wedge o_2=0)) \wedge

1454:     (v_1 < v_2 \rightarrow (o_1=0 \wedge o_2=v_2-v_1))\}$ \\

1455: $\mathtt{ch}_{\{1,2\}}(\{x_1,x_2\})$ \\

1456: $\{(x_1 \geq x_2 \rightarrow (o_1=v_1-x_2 \wedge o_2=0)) \wedge

1457:     (x_1 < x_2 \rightarrow (o_1=0 \wedge o_2=v_2-x_1))\}$,

1458: \end{tabbing}

1459: due to the fact that we obtain a Nash equilibrium if each player bids

1460: his valuation, i.e.\ $x_{i} = v_{i}$. We abbreviate the given

1461: precondition with $P$ and the postcondition with $R$.  Note that $P$

1462: is not the weakest precondition of

1463: $G(\mathtt{ch}_{\{1,2\}}(\{x_1,x_2\}), R, {\mathcal I})$, and hence

1464: ${\mathcal I} \vdash \{P\} \mathtt{ch}_{\{1,2\}}(\{x_1,x_2\}) \{R\}$

1465: is not an axiom.  This is because there are equilibria other than the

1466: one mentioned.  For example, suppose that $v_{1} \geq v_{2}$.  Then if

1467: $v_{2} \leq x_{1} = x_{2} \leq v_{1}$, we also have a Nash

1468: equilibrium.  Hence, for $v_{2} \leq k \leq v_{1}$, we can also

1469: consider the following precondition $P_{k}$ \[ (v_1 \geq v_2

1470: \rightarrow (o_1=v_1-k \wedge o_2=0)) \wedge (v_1 < v_2 \rightarrow

1471: (o_1=0 \wedge o_2=v_2-k)) \] for which we also have ${\mathcal I}

1472: \models \{P_{k}\} \mathtt{ch}_{\{1,2\}}(\{x_1,x_2\}) \{R\}$. 

1473: Consequently, $P_{k} \vee P$ is weaker than $P$ for $k \neq v_{2}$,

1474: and hence ${\mathcal I} \vdash \{P\}

1475: \mathtt{ch}_{\{1,2\}}(\{x_1,x_2\}) \{R\}$ is indeed not an axiom. 

1476: Still, it can be easily obtained from the choice axiom using the

1477: logical consequence rule.

1478: 

1479: \subsubsection*{Dutch Auction}

1480: 

1481: We shall now illustrate the calculus in action for verifying the more complex

1482: Dutch auction which involves a while loop.  In fact, we shall

1483: illustrate that the Dutch auction is equivalent to the preceding

1484: sealed-bid second-price auction in the very weak sense that the Dutch

1485: auction has the same subgame-perfect equilibrium as the sealed-bid

1486: second-price auction, where the player with the higher valuation

1487: receives the object, paying the price of the other player's valuation. 

1488: More formally, we shall show that both implement the same social

1489: choice correspondence defined in section \ref{auctions}, under certain conditions.

1490: 

1491: As mentioned in section \ref{auctions}, in a Dutch auction, the auctioneer

1492: continues to lower the price of an object until a player decides to

1493: take the object for the current price.  Over the domain of natural

1494: numbers, the Dutch auction is captured by the following mechanism

1495: $\alpha$:

1496: \begin{tabbing}

1497: $p:=init$; \\ $w:=0$; \\

1498: $\mathtt{while}$ \= $\: p > 0 \wedge w=0 \: \mathtt{do}$ \\ \>

1499: $\mathtt{ch}_{\{1,2\}}(\{x_1,x_2\})$; \\

1500:     \> $\mathtt{if} \: x_1 > 0 \:$ \= $\mathtt{then} \: w:=1$ \\

1501:     \>\> $\mathtt{else} \: \mathtt{if} \: x_2 > 0 \:$ \= $\mathtt{then}

1502:     \: w:=2$ \\

1503:     \>\>\> $\mathtt{else} \: p:=p-1$

1504: \end{tabbing}

1505: Variable $w$ keeps track of the winner, $p$ keeps track of the current

1506: price, and is initialised to some value $init$.  For each offer, both

1507: players can choose a nonnegative number signaling their desire to buy

1508: the object for price $p$.  As the algorithm is written down here, in

1509: case both players want to buy the object, player 1 gets it.  Note that

1510: it is also subtleties like these which provide an argument for

1511: formally specifying and verifying mechanisms.  The following

1512: postcondition $Q$ naturally assigns payoffs at the end of the Dutch auction:

1513: \[ \begin{array}{rl}

1514: & (w=1 \rightarrow (o_1=v_1-p \wedge o_2=0)) \\ \wedge & (w=2

1515: \rightarrow (o_1=0 \wedge o_2=v_2-p)) \\ \wedge & (w=0 \rightarrow

1516: (o_1=0 \wedge o_2=0))

1517: \end{array}    \]

1518: Our goal will be to show that ${\mathcal I} \vdash \{P\} \alpha

1519: \{Q\}$, i.e., just like the sealed-bid

1520: auction $(\mathtt{ch}_{\{1,2\}}(\{x_1,x_2\}),R)$ SPE-implements our desired

1521: social choice correspondence, so does $(\alpha,Q)$.

1522: 

1523: As in standard program verification, the art of proving the

1524: correctness of a while-loop lies in finding an invariant which remains

1525: true at the beginning of every loop execution.  Consider the following

1526: invariant $Inv$:

1527: \[ \begin{array}{l}

1528: v_{1} \geq v_{2} > 0 \wedge p \geq v_{2} \wedge w \in \{0,1,2\} \\ \wedge \:

1529: (w=1  \rightarrow (o_1=v_1-p \wedge o_2=0)) \\ \wedge  \: (w=2 

1530: \rightarrow (o_1=0 \wedge o_2=v_2-p)) \\ \wedge \:

1531: (w=0 \rightarrow (o_{1}=v_{1} - v_{2} \wedge o_{2} = 0))

1532: \end{array}    \]

1533: 

1534: Note that in order to simplify the exposition we have restricted ourselves

1535: to the case where $v_1 \geq v_2$, but this restriction is in no way essential.

1536: The invariant is similar to the desired postcondition $Q$, the main

1537: difference lies in the situation where there is no winner. In that case, our

1538: desired outcome will be the SPE of the remaining subgame, the outcome

1539: designated by our social choice function, $o_{1} = v_{1} - v_{2}$ and

1540: $o_{2} = 0$. Besides these winning conditions, we state the range of variable 

1541: $w$ as well as two conditions for $v_2$. First, $v_2$ must never be greater than 

1542: the current price, for our equilibrium strategies force us to exit the loop

1543: at $v_2$. If, e.g., the auction started with a price below $v_2$, player 1 could

1544: immediately take the object and thereby receive a payoff higher than $v_1-v_2$.

1545: Second, $v_2$ must be strictly greater than 0, for otherwise, it would be optimal 

1546: for player 1 to take the object in the last round, where the price $p=1$, and hence

1547: obtaining a payoff lower than $v_1-v_2$. Note that the need for these additional 

1548: constraints was discovered in the verification process and hence the ``discovery''

1549: of these crucial side conditions should be regarded as a result of the 

1550: verification effort.

1551: 

1552: We will now proceed to show that $Inv$ is indeed an

1553: invariant, i.e., that ${\mathcal I} \vdash$

1554: \begin{tabbing}

1555:  $\{Inv \wedge p>0 \wedge w=0\}$ \\

1556: $\mathtt{ch}_{\{1,2\}}(\{x_1,x_2\})$; \\

1557:     $\mathtt{if} \: x_1 > 0 \:$ \= $\mathtt{then} \: w:=1$ \\

1558:     \> $\mathtt{else} \: \mathtt{if} \: x_2 > 0 \:$ \= $\mathtt{then}

1559:     \: w:=2$ \\

1560:     \>\> $\mathtt{else} \: p:=p-1$ \\

1561: $\{Inv\}$

1562: \end{tabbing}

1563: Note that in fact, $p>0$ is already implied by $Inv$ which means that

1564: if $Inv$ is indeed an invariant, the auction can never terminate due

1565: to the price having reached 0.  Hence, for the purposes of verifying the

1566: desired equilibrium, the condition $p>0$ is redundant in the guard

1567: condition of the while-loop.

1568: 

1569: To begin with, applying the assignment rule and the if-rule, it is

1570: easy to check that  ${\mathcal I} \vdash$

1571: \begin{tabbing}

1572: $\{ v_{1} \geq v_{2} > 0 \wedge p \geq v_{2} \wedge

1573: (x_{1} > 0 \rightarrow (o_1=v_1-p \wedge o_2=0))$ \\ $\wedge \: ((x_{1}=0

1574: \wedge x_{2} > 0) \rightarrow (o_1=0 \wedge o_2=v_2-p))$ \\ $\wedge \:

1575: ((x_{1}=0 \wedge x_{2} = 0) \rightarrow Inv[p/p-1])\}$ \\

1576:     $\mathtt{if} \: x_1 > 0 \:$ \= $\mathtt{then} \: w:=1$ \\

1577:     \> $\mathtt{else} \: \mathtt{if} \: x_2 > 0 \:$ \= $\mathtt{then}

1578:     \: w:=2$ \\

1579:     \>\> $\mathtt{else} \: p:=p-1$ \\

1580: $\{Inv\},$

1581: \end{tabbing}

1582: where $Inv[p/p-1]$ results from substituting $p-1$ for $p$ in

1583: $Inv$.  Denote the new precondition as $Inv_{2}$.  Now we claim that

1584: ${\mathcal I} \vdash$ 

1585: \begin{tabbing}

1586:     $\{v_{1} \geq v_{2} > 0 \wedge p \geq v_{2} \wedge w=0$ \= $\wedge \:

1587:     (p \leq v_{2} \rightarrow (o_{1}=v_{1} - p \wedge o_{2} = 0))$\\

1588:     \> $\wedge \: (p>v_{2} \rightarrow (o_{1}=v_{1} - v_{2} \wedge o_{2} =

1589:     0))\}$ \\

1590:     $\mathtt{ch}_{\{1,2\}}(\{x_1,x_2\})$ \\

1591:     $\{Inv_{2}\}$

1592: \end{tabbing}

1593: Assume that $v_{1} \geq v_{2} > 0$, and consider a state $s$ where $p \geq

1594: v_{2}$ and $w=0$.  We distinguish two cases.  First, if $p \leq v_{2}$

1595: (i.e., $p=v_{2}$), both players asking for the object, i.e., $x_{1} >

1596: 0$ and $x_{2} > 0$, constitutes a Nash equilibrium in the game with

1597: payoffs according to $Inv_{2}$, with payoffs $o_{1}= v_{1}-p$ and

1598: $o_{2} = 0$.  Second, suppose that $p > v_{2}$.  In this case, both

1599: players declining the object, i.e., $x_{1} = x_{2} = 0$, constitutes a

1600: Nash equilibrium.  Player 2 should not ask for it since the price

1601: exceeds his valuation, and player 1 should not ask for it since the

1602: price will be lower in the next round; formally, declining the object

1603: yields $o_{1} = v_{1}-v_{2}$, whereas demanding the object only yields

1604: $o_{1} = v_{1} - p$.  Note that here it is essential that $v_{2} > 0$,

1605: since it allows us to conclude that also $p-1 > 0$, i.e., we have not

1606: reached the last auction round yet, there will be another round with a

1607: lower price.

1608: 

1609: Denote the new precondition as $Inv_{3}$.  Note that $Inv \wedge w=0

1610: \subseteq Inv_{3}$.  Hence, by using the composition rule and the

1611: logical consequence rule, we have established that $Inv$ is indeed an

1612: invariant of the loop.  Hence, we can apply the while rule to derive

1613: that ${\mathcal I} \vdash$

1614: \begin{tabbing}

1615: $\{Inv\}$ \\

1616: $\mathtt{while}$ \= $\: p > 0 \wedge w=0 \: \mathtt{do}$ \\ \>

1617: $\mathtt{ch}_{\{1,2\}}(\{x_1,x_2\})$; \\ \>

1618:     $\mathtt{if} \: x_1 > 0 \:$ \= $\mathtt{then} \: w:=1$ \\ \>

1619:     \> $\mathtt{else} \: \mathtt{if} \: x_2 > 0 \:$ \= $\mathtt{then}

1620:     \: w:=2$ \\ \>

1621:     \>\> $\mathtt{else} \: p:=p-1$ \\

1622: $\{Inv \wedge \neg (p>0 \wedge w=0)\}$

1623: \end{tabbing}

1624: 

1625: So to conclude the verification of the Dutch auction, it suffices to

1626: note two things.  First, $Inv \wedge \neg (p>0 \wedge w=0)

1627: \subseteq Q$, and hence we can apply the logical consequence rule to

1628: obtain the desired postcondition $Q$.  Second, we have ${\mathcal I}

1629: \vdash$

1630: \begin{tabbing}

1631: $\{v_{1} \geq v_{2} > 0 \wedge init \geq v_{2} \wedge o_{1} = v_{1}

1632: - v_{2} \wedge o_{2} = 0 \}$ \\

1633: $p:=init$; \\ $w:=0$ \\

1634: \{Inv\}

1635: \end{tabbing}

1636: Hence, using the composition rule, we have now shown that ${\mathcal

1637: I} \vdash$

1638: \begin{tabbing}

1639: $\{v_{1} \geq v_{2} > 0 \wedge init \geq v_{2} \wedge o_{1} = v_{1} -

1640: v_{2} \wedge o_{2} = 0 \}$ \\

1641: $p:=init$; \\ $w:=0$; \\

1642: $\mathtt{while}$ \= $\: p > 0 \wedge w=0 \: \mathtt{do}$ \\ \>

1643: $\mathtt{ch}_{\{1,2\}}(\{x_1,x_2\})$; \\

1644:     \> $\mathtt{if} \: x_1 > 0 \:$ \= $\mathtt{then} \: w:=1$ \\

1645:     \>\> $\mathtt{else} \: \mathtt{if} \: x_2 > 0 \:$ \= $\mathtt{then}

1646:     \: w:=2$ \\

1647:     \>\>\> $\mathtt{else} \: p:=p-1$ \\

1648: $\{(w=1 \rightarrow (o_1=v_1-p \wedge o_2=0)) \wedge (w=2

1649: \rightarrow (o_1=0 \wedge o_2=v_2-p))$ \\ $\wedge \: (w=0 \rightarrow

1650: (o_1=0 \wedge o_2=0))\}$

1651: \end{tabbing}

1652: 

1653: Note that the verification process has revealed two crucial details

1654: which had to be added to our original precondition $P$.  First, $init

1655: \geq v_2$.  This means that we need to make sure that we start the

1656: auction at a price that is high enough.  If the players' valuations

1657: are not known, the choice of the initial price can indeed be a

1658: problem.  On the other hand, the condition tells us exactly what

1659: ``high enough'' means, in particular, the initial price does not need

1660: to exceed everybody's valuation.  Second, $v_2 > 0$.  Hence, it does not

1661: suffice if only a single player has a non-zero valuation of the

1662: object.  The problem here lies in the fact that in order to obtain the

1663: object one has to pay at least something, and if the other player's

1664: valuation is zero, that something is more than the other player's

1665: valuation, and hence the payoff is in turn lower than expected.  Hence,

1666: we have succeeded in verifying that $(\alpha,Q)$ does indeed implement

1667: the social choice correspondence of section \ref{auctions} associated

1668: with the second-price auction, on condition that $init \geq v_{2} >

1669: 0$.

1670: 

1671: Finally, it should be emphasised again that the weak equivalence of the Dutch

1672: auction and the sealed-bid second-price auction demonstrated here is very

1673: weak indeed, since these auctions are very different.

1674: Crucially, in the sealed-bid second-price

1675: auction, a player does not need to know the other player's valuation. 

1676: It suffices that each player submits his own valuation as a bid.  In

1677: the Dutch auction, however, obtaining the same equilibrium outcome

1678: requires the player with the higher valuation to know the valuation of

1679: the other player so that he can decide to shout out just at the right

1680: moment.  Hence, the two auctions do not satisfy the same knowledge

1681: preconditions. The standard result concerning the equivalence between Dutch 

1682: auction and first-price auction does take these knowledge preconditions into 

1683: account.

1684: 

1685: 

1686: 

1687: 

1688: %

1689: %----------------------------

1690: %

1691: \section{Conclusions}

1692: %

1693: %-----------------------------

1694: %

1695: 

1696: Two main directions for future research present themselves: On the

1697: foundational side, the question arises whether the present

1698: approach can also be applied to other equilibrium notions. We have

1699: already remarked that while the calculus presented can also be

1700: used to reason about Nash equilibria, the non-compositional nature

1701: of these equilibria stands in the way of a complete calculus.

1702: Hence, alternative equilibrium notions that promise to be amenable

1703: to our approach will be refinements of subgame-perfect equilibria.

1704: Second, we mentioned already that an intensional approach to pre-

1705: and postconditions is worth developing. For this, the crucial

1706: question is whether the logic used (FOL) and the expressiveness

1707: results obtained for programs can be carried over to mechanisms.

1708: 

1709: At the most general level, we hope that this paper has shown that

1710: tools from computational logic can be extended from program

1711: verification to the verification of game-theoretic mechanisms. The

1712: examples provided should suffice to convince the reader of the

1713: variety of possible applications of such an extension. The

1714: semantics of the correctness assertions for mechanisms is more

1715: complex than for programs, but this is counterbalanced by the fact

1716: that the mechanisms we would like to verify (e.g., spectrum

1717: auctions for telecommunication markets) may turn out to be simpler

1718: than their counterparts in computer software (e.g., operating

1719: systems).

1720: 

1721: %

1722: %----------

1723: \subsection*{Acknowledgments}

1724: %----------

1725: %

1726: For their comments and suggestions, I would like to thank the anonymous referees,

1727: Peter McBurney, Mike Wooldridge and the members of Rohit Parikh's seminar 

1728: at the Graduate Center of the City University of New York (CUNY).

1729: 

1730: \bibliographystyle{plain}

1731: \bibliography{marc}

1732: 

1733: 

1734: \end{document}

1735: