<p>We prove it ($P2^c \implies P2^b$) by <a href="https://en.wikipedia.org/wiki/Mathematical_induction#Complete_induction" rel="nofollow noreferrer">strong induction (wiki)</a>. This proof has actually been given in the "Paxos Made Simple" paper (see the arguments between $P2^b$ and $P2^c$). I re-organize it in the order of "what we know, what we want to prove, and how to prove". Hope it helps.</p>

<hr>

<p><strong><em>What we know:</em></strong></p>

<p><em>Base case:</em> Some proposal with number $m$ and value $v$ is chosen.</p>

<p><em>Inductive assumption:</em> Every proposal issued with a number in $m \ldots (n-1)$ has value $v$.</p>

<p><em>The chosen rule of a proposal:</em> For the proposal number $m$ to be chosen, there must be some set $C$ consisting of a majority of acceptors such that every acceptor in $C$ accepted it.</p>

<p><em>The issue rule of a proposal:</em> It is the existence of a set $S$ such that $P2^c (1)$ + $P2^c (2)$.</p>

<p><strong><em>What we want to prove is:</em></strong></p>

<p><em>Goal:</em> Any proposal issued with number $n &gt; m$ also have value $v$.</p>

<hr>

<p><strong><em>Proof:</em></strong></p>

<p>Combining "base case" and "chosen-rule" with "inductive assumption", we obtain:<br>
<strong><em>The $C$-condition:</em></strong> Every acceptor in $C$ has accepted a proposal with number in $m \ldots (n-1)$ (<em>Note:</em> because at least each of them has accepted a proposal with number $m$),<br>
and every proposal with number in $m \ldots (n-1)$ accepted by any acceptor has value $v$ (<em>Note:</em> due to the inductive assumption and the fact that a proposal must be issued by a proposer before it can be accepted by an acceptor).</p>

<p>Now consider the set $S$ in $P2^c$ which consists of a majority of acceptors. Because $S \cap C \neq \emptyset$, $P2^c(1)$ cannot happen. Then $P2^c(2)$ must be true. $P2^c(2)$ is actually the "value-issued rule": the value $v'$ of the proposal with number $n$ is the value of the highest-numbered proposal among all proposals numbered less than $n$ accepted by the acceptors in $S$, therefore $v' = v$ because of the $C$-condition.</p>

<hr>

<p>Related posts: </p>

<ul>
<li><a href="https://cstheory.stackexchange.com/q/27391/12739">The proof of P2b in Paxos made simple@cstheory</a></li>
<li><a href="https://cstheory.stackexchange.com/q/25851/12739">Correctness proofs of classic Paxos and Fast Paxos@cstheory</a>.</li>
</ul>

CC BY-SA 3.0
2016-01-09T06:11:05.840Z
2016-01-09T06:11:05.840Z
2017-04-13T12:32:28.167Z
hengxin
<p>I am reading 
Leslie Lamport's <a href="http://research.microsoft.com/en-us/um/people/lamport/pubs/paxos-simple.pdf" rel="nofollow">Paxos Made Simple</a> paper. </p>

<p>Can someone explain why $P2^c$ implies $P2^b$?</p>

<blockquote>
  <p>$P2^b$ If a proposal with value $v$ is chosen, 
  then every higher-numbered proposal issued by any proposer has value $v$.</p>
  
  <p>$P2^c$ For any $v$ and $n$, 
  if a proposal with value $v$ and number $n$ is issued,
  then there is a set $S$ 
  consisting of a majority of acceptors such that either </p>
  
  <ol>
  <li>no acceptor in $S$ has accepted any proposal numbered less than $n$, or </li>
  <li>$v$ is the value of the highest-numbered proposal among
  all proposals numbered less than $n$ accepted by the acceptors in $S$.</li>
  </ol>
</blockquote>

<ds.algorithms><dc.distributed-comp><proofs>
Paxos made simple, invariant P2c
PNT
# Paxos made simple, invariant P2c

(Asked by: username_0 on 2016-01-04)

I am reading
Leslie Lamport's [Paxos Made Simple](http://research.microsoft.com/en-us/um/people/lamport/pubs/paxos-simple.pdf) paper.

Can someone explain why $P2^c$ implies $P2^b$?

> $P2^b$ If a proposal with value $v$ is chosen,
> then every higher-numbered proposal issued by any proposer has value $v$.
>
> $P2^c$ For any $v$ and $n$,
> if a proposal with value $v$ and number $n$ is issued,
> then there is a set $S$
> consisting of a majority of acceptors such that either
>
> 1. no acceptor in $S$ has accepted any proposal numbered less than $n$, or
> 2. $v$ is the value of the highest-numbered proposal among
>    all proposals numbered less than $n$ accepted by the acceptors in $S$.

**Tags:** ds.algorithms, dc.distributed-comp, proofs

---

## 1 answers

### Answer by username_1 on 2016-01-09. Score: 2

We prove it ($P2^c \implies P2^b$) by [strong induction (wiki)](https://en.wikipedia.org/wiki/Mathematical_induction#Complete_induction). This proof has actually been given in the "Paxos Made Simple" paper (see the arguments between $P2^b$ and $P2^c$). I re-organize it in the order of "what we know, what we want to prove, and how to prove". Hope it helps.

---

***What we know:***

*Base case:* Some proposal with number $m$ and value $v$ is chosen.

*Inductive assumption:* Every proposal issued with a number in $m \ldots (n-1)$ has value $v$.

*The chosen rule of a proposal:* For the proposal number $m$ to be chosen, there must be some set $C$ consisting of a majority of acceptors such that every acceptor in $C$ accepted it.

*The issue rule of a proposal:* It is the existence of a set $S$ such that $P2^c (1)$ + $P2^c (2)$.

***What we want to prove is:***

*Goal:* Any proposal issued with number $n > m$ also have value $v$.

---

***Proof:***

Combining "base case" and "chosen-rule" with "inductive assumption", we obtain:  
***The $C$-condition:*** Every acceptor in $C$ has accepted a proposal with number in $m \ldots (n-1)$ (*Note:* because at least each of them has accepted a proposal with number $m$),  
and every proposal with number in $m \ldots (n-1)$ accepted by any acceptor has value $v$ (*Note:* due to the inductive assumption and the fact that a proposal must be issued by a proposer before it can be accepted by an acceptor).

Now consider the set $S$ in $P2^c$ which consists of a majority of acceptors. Because $S \cap C \neq \emptyset$, $P2^c(1)$ cannot happen. Then $P2^c(2)$ must be true. $P2^c(2)$ is actually the "value-issued rule": the value $v'$ of the proposal with number $n$ is the value of the highest-numbered proposal among all proposals numbered less than $n$ accepted by the acceptors in $S$, therefore $v' = v$ because of the $C$-condition.

---

Related posts:

* [The proof of P2b in Paxos made simple@cstheory](https://cstheory.stackexchange.com/q/27391/12739)
* [Correctness proofs of classic Paxos and Fast Paxos@cstheory](https://cstheory.stackexchange.com/q/25851/12739).


---

