假定存在一个全局的消息队列，进程可以发送消息，也可以在其上接收消息。send(p,m)表示向进程p发送消息m；receive(p,m)表示进程p收到了消息m。

所有进程的状态集，进程的状态包括初始值、决议值、消息队列的内容。初始Configuration表示各个进程的初始值是随机的，同时消息队列为空，决议值为空。

事件代表给某个进程发送消息，并且消息已送达，可用event(p,m)表示。根据消息队列的定义可以知道，event(p,m)即send(p,m)与receive(p,m)的交。由于某个事件，某个Configuration可以转化为另一个Configuration。

一连串顺序执行的事件序列，记为run，即runn=[event1(p1,m1), event2(p2,m2),…?,eventn(pn,mn)]。

在对某个Configuration A应用了某个run事件序列之后，得到Configuration B，则称B从A可达——可记为B?A。

把所有的进程P分成两个不相交的集合P1，P2，有两个run R1，R2，如果先给P1应用R1，再给P2应用R2与先给P2应用R2，再给P1应用R1，对P的Configuration C来说得到的结果是一致的。

结果显而易见，不再罗列证明。

初始Configuration不确定性

对任何算法P，都存在至少一个不确定性的初始Configuration。

可以用反证法证明此引理。

因为候选的决议值必须大于1个才需要保证决议的一致性，这里选取了最简单的两个候选值的情况，候选值分别是value1和value2。而多候选值情形可以根据归纳法证明。

这里再做一个定义：

Configuration相邻

若两个Configuration间，仅有一个进程的状态存在差别，那么称为Configuration相邻。

假设所有初始Configuration都是确定的，那么对于任意一个非空进程集P，必然至少存在一对相邻的Configuration 1（C1）和Configuration 2（C2），二者的决议分别是value1和value2，其连接进程是P0。

假设连接进程突然间掉线了，那么C1和C2剩余进程的状态必然是完全一致的。那么此时，我们就无法从剩余进程中知道当前Configuration的确切的决议值。

不可终止性

设C是一个不确定Configuration，event(p,m)是可以应用到C的事件。设X是从C可达并且未应用过event的Configuartion的集合，并构造Y = e(X) = {e(E) | E∈X a并且 e应用于E}。那么，Y一定包含不确定的configuration。

简而言之：不确定性是可以传播的。

根据上文中的设定，我们可以得到如下示意图：

同样使用反证法证明：设Y中的Configuration都是确定的。

因为C是不确定的，因此必然从C可达一个确定的0-value Configuration(C0)，同时可达一个确定的1-value Configuration(C1)。

由于C0是0-value，无论是D0从C0可达，或是C0从D0可达，都可以推导出D0是0-value。同理，也可以推导出Y中存在一个D1是1-value。

由于0-value和1-value的C都必然存在，因此我们可以很容易得出下图：

我们无须关心该图中C0或者C1的具体值，只需知道必然存在一个C1，C1从C0可达。

虚线部分如下：

假设e和f操作的进程分别是pe和pf，那么分为两种情况：

pe!=pf

根据引理1（连通性）很容易得到下图：

显然，D0和D1应该是不同的值，因此导出一个矛盾：Y中有两个值，因此是不确定的。

pe==pf

由于C0已确定，因此经过σ，得到的应该是一个确定的F。 经过eσ，得到的是一个确定的E0（D0已确定）。 经过feσ，得到的是一个确定的E1（D1已确定），并且E1!=E0。

同时，由于σ和e/f操作的是不同的进程，所以可以应用引理1（连通性）。 因此可以导出σe等价于eσ，σfe等价于feσ，所以，根据上图，F可以分别导出两个不同的结果E0和E1——这和之前的推导是相互矛盾的。

综上所述，Y中可能会包含一个不确定的Configuration。

尽管FLP impossible原理是基于简单的系统模型假设，但我们可以根据归纳法得出，在更复杂的系统模型下，我们仍然没有任何算法能够完全保证分布式系统下的一致性。

但我们不必绝望，此结论只是说明了100%保证一致性是不可能的，这并不影响我们对分布一致性的探索（99%以上的一致性还是完全有可能做到的）。

• LoopJump. FLP impossibility证明 阅读笔记

• 纯粹的码农. FLP Impossibility