# The proof of P2b in Paxos made simple

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

## 1 Answer

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

• Now I understand the additional assumption comes from strong induction. But I still have many questions. 1)Why you say the base case P(m) is trivial? Can you make it clear a bit? For me, If P(m) holds, then when proposal m is chosen, a higher-numbered proposal, say m+1, issued by other proposer must also has value v. But I can't figure it out. Unless on your strong induction, proposal m..n-1 has value v, so P(m) is true. But I think we should make strong induction after we have checked the base case P(m) is true. – StrikeW Nov 17 '14 at 4:56
• 2) The inference of C-condition is the most confusing. On my view, you showed that the C-condition follows by just replace m with m..(n-1), isn't it? If it is, I can't bridge the gap from m to m..(n-1) on my mind. – StrikeW Nov 17 '14 at 5:04