The proof of P2b in Paxos made simple

Question

I am reading Paxos Made Simple. I am quite confused about the proof of P2b. It said

We would make the proof easier by using induction on n, so we can prove that proposal number n has value v under the additional assumption that every proposal issued with a number in m..(n - 1) has value v.

How can he add the additional assumption? Is it reasonable? In reality, proposal numbered in m..(n - 1) can have value other than v, isn't it?

I am really confused about that, please help! Thanks

Answer 1

Note: I have had a similar question about the correctness proof of Paxos and Fast Paxos before and posted it here. Wish the excellent answer to it be helpful to you.

---

A few words about this paper:

Leslie Lamport has his own, very impressive writing style. He is not satisfied with the common pattern of stating a theorem, proving it, moving on to another theorem, and so on. He is good at demonstrating the way how to solve a problem. In his paper, you will see that proof does not follow a theorem; instead, it comes along with a theorem. The paper "Paxos Made Simple" is a typical example of this style.

---

About your questions:

Your question (1): How can he add the additional assumption? Is it reasonable?

Leslie Lamport is using strong induction. The goal here is to prove

$P2^{b}:$ If a proposal with value $v$ i chosen (say, with number $m$), then every higher-numbered proposal issued by any proposer has value $v$.

We apply strong induction to natural number $\mathbb{N}$. I summarize the proof as follows and explain it later.

• The base case is "some proposal with number $m$ and value $v$ is chosen".

• The strong induction hypothesis is "every proposal issued with a number in $m .. (n-1)$ has value $v$".

• The induction step to prove $P2^{b}$: Combining the premise of "$m$ is chosen (with value $v$)" with the above induction hypothesis, we get (for reference, I call it $C$-condition):

$C$-condition: Every acceptor in $C$ (defined in the paper) has accepted a proposal with number in $m .. (n-1)$, and every proposal with number in $m .. (n-1)$ accepted by any acceptor has value $v$.

Now, Lamport introduces $P2^{c}$, which, along with the above $C$-condition, is sufficient for $P2^{b}$.

You can think of this induction process step by step:

1. The base case $m$ is trivially valid.
2. Given that step 1 is valid, the argument in "The induction step" above (of course with $P2^{C}$) shows that the proposals numbered $m+1$ has value $v$.
3. Given both step 1 and step 2 are valid, the same argument shows that the proposals numbered $m + 2$ has value $v$.
4. And so on.

This also answers your second question.

Your question (2): In reality, proposal numbered in $m..(n - 1)$ can have value other than v, isn't it?

No, it isn't. The Paxos algorithm guarantees that all the proposals with larger numbers than $m$ must have value $v$, given that $m$ is chosen with value $v$.