<p><em>Note:</em> I have had a similar question about the correctness proof of Paxos and Fast Paxos before and <a href="https://cstheory.stackexchange.com/q/25851/12739">posted it here</a>. Wish the excellent answer to it be helpful to you.</p>

<hr>

<p><em>A few words about this paper:</em></p>

<p>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 <em>follow</em> a theorem; instead, it <em>comes along with</em> a theorem. The paper "Paxos Made Simple" is a typical example of this style.</p>

<hr>

<p><em>About your questions:</em></p>

<blockquote>
  <p><em>Your question (1):</em> How can he add the additional assumption? Is it reasonable?</p>
</blockquote>

<p>Leslie Lamport is using <a href="https://en.wikipedia.org/wiki/Mathematical_induction#Complete_induction" rel="nofollow noreferrer">strong induction</a>. The goal here is to prove </p>

<blockquote>
  <p><span class="math-container">$P2^{b}:$</span> If a proposal with value <span class="math-container">$v$</span> i chosen (say, with number <span class="math-container">$m$</span>), then every higher-numbered proposal issued by any proposer has value <span class="math-container">$v$</span>.</p>
</blockquote>

<p>We apply strong induction to natural number <span class="math-container">$\mathbb{N}$</span>. I summarize the proof as follows and explain it later.</p>

<ul>
<li><p>The base case is "some proposal with number <span class="math-container">$m$</span> and value <span class="math-container">$v$</span> is chosen".</p></li>
<li><p>The <em>strong</em> induction hypothesis is "every proposal issued with a number in <span class="math-container">$m .. (n-1)$</span> has value <span class="math-container">$v$</span>".</p></li>
<li><p><strong>The induction step to prove <span class="math-container">$P2^{b}$</span></strong>: Combining the premise of "<span class="math-container">$m$</span> is chosen (with value <span class="math-container">$v$</span>)" with the above induction hypothesis, we get (for reference, I call it <span class="math-container">$C$</span>-condition):</p></li>
</ul>

<blockquote>
  <p><em><span class="math-container">$C$</span>-condition:</em> Every acceptor in <span class="math-container">$C$</span> (defined in the paper) has accepted a proposal with number in <span class="math-container">$m .. (n-1)$</span>, and every proposal with number in <span class="math-container">$m .. (n-1)$</span> accepted by any acceptor has value <span class="math-container">$v$</span>.</p>
</blockquote>

<p>Now, Lamport introduces <span class="math-container">$P2^{c}$</span>, which, along with the above <span class="math-container">$C$</span>-condition, is sufficient for <span class="math-container">$P2^{b}$</span>.</p>

<p>You can think of this induction process step by step:</p>

<ol>
<li>The base case <span class="math-container">$m$</span> is trivially valid.</li>
<li>Given that step 1 is valid, the argument in "<strong>The induction step</strong>" above (of course with <span class="math-container">$P2^{C}$</span>) shows that the proposals numbered <span class="math-container">$m+1$</span> has value <span class="math-container">$v$</span>.</li>
<li>Given both step 1 and step 2 are valid, the same argument shows that the proposals numbered <span class="math-container">$m + 2$</span> has value <span class="math-container">$v$</span>.</li>
<li>And so on.</li>
</ol>

<p>This also answers your second question.</p>

<blockquote>
  <p><em>Your question (2):</em> In reality, proposal numbered in <span class="math-container">$m..(n - 1)$</span> can have value other than v, isn't it?</p>
</blockquote>

<p>No, it isn't. The Paxos algorithm guarantees that all the proposals with larger numbers than <span class="math-container">$m$</span> must have value <span class="math-container">$v$</span>, given that <span class="math-container">$m$</span> is chosen with value <span class="math-container">$v$</span>.</p>

CC BY-SA 3.0
2014-11-17T04:56:43.790Z
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
CC BY-SA 3.0
2014-11-17T05:04:09.990Z
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
CC BY-SA 4.0
2014-11-10T05:47:13.337Z
2019-05-23T02:59:17.777Z
2019-05-23T02:59:17.777Z
hengxin
<p>I am reading <em><a href="http://research.microsoft.com/en-us/um/people/lamport/pubs/paxos-simple.pdf" rel="nofollow">Paxos Made Simple</a></em>. I am quite confused about the proof of P2b. It said</p>

<blockquote>
  <p>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.</p>
</blockquote>

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

<p>I am really confused about that, please help! Thanks</p>

<dc.distributed-comp>
The proof of P2b in Paxos made simple
StrikeW
# The proof of P2b in Paxos made simple

(Asked by: username_0 on 2014-11-09)

I am reading *[Paxos Made Simple](http://research.microsoft.com/en-us/um/people/lamport/pubs/paxos-simple.pdf)*. 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

**Tags:** dc.distributed-comp

---

## 1 answers

### Answer by username_1 on 2014-11-10. Score: 1 | Accepted answer

*Note:* I have had a similar question about the correctness proof of Paxos and Fast Paxos before and [posted it here](https://cstheory.stackexchange.com/q/25851/12739). 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](https://en.wikipedia.org/wiki/Mathematical_induction#Complete_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$.

> **Comments:**
> **username_0**: 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.  
> **username_0**: 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.  

---

