How do we make sure in Paxos that we don't propose a different value if a majority has formed?

Question

Recall that Paxos is a distributed system algorithm with the goal that the processes participating in its protocol will reach consensus on one of the valid values.

I was studying Paxos from:

http://research.microsoft.com/en-us/um/people/lamport/pubs/paxos-simple.pdf

and I was confused about one specific part. How does or why does property $P2^b$ satisfy property $P2^c$?

These are the properties:

$P2^b = $ If a proposal with value $v$ is chosen, then every higher-numbered (i.e. approx. later in time) proposal issue 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$ (some majority) of acceptors such that either:

(a)no acceptor in $S$ has accepted any proposal numbered less than $n$, or

(b)$v$ is the value of the highest-numbered proposal among all proposals numbered less than $n$ accepted by the acceptors in $S$ (some majority).

The paper uses $S$ to denote some majority and $C$ to denote some majority that has actually chosen a value.

The thing that I am confused about is, for me $P2^b$ is saying, ok once a value has been chosen, say at sequence number $n$ (i.e. roughly time $n$), then after that time, we want to make sure that any proposer is only able to propose the value of the majority (chosen value). If we have that, then, we do not risk the already formed majority from reverting weirdly. i.e. once we have formed a majority, we want it to stick and stay like that. However, it was not 100% clear to me why property $P2^c$ satisfied that requirement. I kind of see why (a) is a nice property to have, since, having (a) means that its safe to issue a new proposal $(n, v)$ since we contacted some majority $S$ and none of them had accepted anything in a time earlier than now $n$. So, if a majority had formed we would have seen at least one value and we did not see anything accepted, its safe to propose something since a majority has not formed.

---

Author: Leslie Lamport

Title: Paxos made simple

Institution: Microsoft Research

Answer 1

$P2^c\implies P2^b$ since $P2^c\iff (a)\lor (b)$ and the logical statement $(a)\lor(b) \implies P2^b$ is equivalent to $(a)\implies P2^b\land (b)\implies P2^b$.

Let's consider $(a)$. If no acceptor in $S$ has accepted anything below $n$, then $P2^b$ is trivially satisfied (the implication predicate is false).

Otherwise, assume $(b)$. Then there exists a highest-numbered accepted value $(v, n)$ for some acceptor within $S$, which the proposer will decide to send as an accept request. Thus $v$ must have been chosen already, since an acceptor had it.