Paxos算法提出与证明首先将议员的角色分为 proposers，acceptors，和 learners（允许身兼数职）

proposers 提出提案，提案信息包括提案编号和提议的 value；acceptor 收到提案后可以接受（accept）提案，若提案获得多数 acceptors 的接受，则称该提案被批准（chosen）；learners 只能“学习”被批准的提案

划分角色后，就可以更精确的定义问题：决议（value）只有在被 proposers 提出后才能被批准（未经批准的决议称为“提案（proposal）”）；在一次 Paxos 算法的执行实例中，只批准（chosen）一个 value；learners 只能获得被批准（chosen）的 value

另外还需要保证 progress

这一点以后再讨论

作者通过不断加强上述3个约束（主要是第二个）获得了 Paxos 算法

批准 value 的过程中，首先 proposers 将 value 发送给 acceptors，之后 acceptors 对 value 进行接受（accept）

为了满足只批准一个 value 的约束，要求经“多数派（majority）”接受的 value 成为正式的决议（称为“批准”决议）

这是因为无论是按照人数还是按照权重划分，两组“多数派”至少有一个公共的 acceptor，如果每个 acceptor 只能接受一个 value，约束2就能保证

于是产生了一个显而易见的新约束：P1：一个 acceptor 必须接受（accept）第一次收到的提案

注意 P1 是不完备的

如果恰好一半 acceptor 接受的提案具有 value A，另一半接受的提案具有 value B，那么就无法形成多数派，无法批准任何一个 value

约束2并不要求只批准一个提案，暗示可能存在多个提案

只要提案的 value 是一样的，批准多个提案不违背约束2

于是可以产生约束 P2：P2：一旦一个具有 value v 的提案被批准（chosen），那么之后批准（chosen）的提案必须具有 value v

注：通过某种方法可以为每个提案分配一个编号，在提案之间建立一个全序关系，所谓“之后”都是指所有编号更大的提案

如果 P1 和 P2 都能够保证，那么约束2就能够保证

批准一个 value 意味着多个 acceptor 接受（accept）了该 value

因此，可以对 P2 进行加强：P2a：一旦一个具有 value v 的提案被批准（chosen），那么之后任何 acceptor 再次接受（accept）的提案必须具有 value v

由于通信是异步的，P2a 和 P1 会发生冲突

如果一个 value 被批准后，一个 proposer 和一个 acceptor 从休眠中苏醒，前者提出一个具有新的 value 的提案

根据 P1，后者应当接受，根据 P2a，则不应当接受，这中场景下 P2a 和 P1 有矛盾

于是需要换个思路，转而对 proposer 的行为进行约束：P2b：一旦一个具有 value v 的提案被批准（chosen），那么以后任何 proposer 提出的提案必须具有 value v

由于 acceptor 能接受的提案都必须由 proposer 提出，所以 P2b 蕴涵了 P2a，是一个更强的约束

但是根据 P2b 难以提出实现手段

因此需要进一步加强 P2b

假设一个编号为 m 的 value v 已经获得批准（chosen），来看看在什么情况下对任何编号为 n（n>m）的提案都含有 value v

因为 m 已经获得批准（chosen），显然存在一个 acceptors 的多数派 C，他们都接受（accept）了v

考虑到任何多数派都和 C 具有至少一个公共成员，可以找到一个蕴涵 P2b 的约束 P2c：P2c：如果一个编号为 n 的提案具有 value v，那么存在一个多数派，要么他们中所有人都没有接受（accept）编号小于 n 的任何提案，要么他们已经接受（accept）的所有编号小于 n 的提案中编号最大的那个提案具有 value v

可以用数学归纳法证明 P2c 蕴涵 P2b：假设具有value v的提案m获得批准，当n=m+1时，采用反证法，假如提案n不具有value v，而是具有value w，根据P2c，则存在一个多数派S1，要么他们中没有人接受过编号小于n的任何提案，要么他们已经接受的所有编号小于n的提案中编号最大的那个提案是value w

由于S1和通过提案m时的多数派C之间至少有一个公共的acceptor，所以以上两个条件都不成立，导出矛盾从而推翻假设，证明了提案n必须具有value v；若（m+1）..（N-1）所有提案都具有value v，采用反证法，假如新提案N不具有value v，而是具有value w',根据P2c，则存在一个多数派S2，要么他们没有接受过m..（N-1）中的任何提案，要么他们已经接受的所有编号小于N的提案中编号最大的那个提案是value w'

由于S2和通过m的多数派C之间至少有一个公共的acceptor，所以至少有一个acceptor曾经接受了m，从而也可以推出S2中已接受的所有编号小于n的提案中编号最大的那个提案的编号范围在m..（N-1）之间，而根据初始假设，m..（N-1）之间的所有提案都具有value v，所以S2中已接受的所有编号小于n的提案中编号最大的那个提案肯定具有value v，导出矛盾从而推翻新提案n不具有value v的假设

根据数学归纳法，我们证明了若满足P2c，则P2b一定满足

P2c是可以通过消息传递模型实现的

另外，引入了P2c后，也解决了前文提到的P1不完备的问题

以上内容由大学时代综合整理自互联网，实际情况请以官方资料为准。