# Paxos made simple, invariant P2c

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$.

We prove it ($P2^c \implies P2^b$) by strong induction (wiki). 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: