这篇文章 Seth Gilbert 和 Nancy Lynch 形式化证明了 Brewer 的 CAP 理论。讨论了异步网络环境和半异步网络环境下 CAP 理论的正确性。鄙人英语 so so ，再加上文章比较枯燥，仅翻译下所列出的定理:

Theorem 1 It is impossible in the asynchronous network model to implement a read/write data object that guarantees the following properties:
          • Availability
          • Atomic consistency in all fair executions (including those in which messages are lost).

定理1 在异步网络模型中应用一个读/写数据对象并满足以下特性是不可能的：
           • 可用性
           • 在所有请求平等下的原子一致性（包括消息丢失情况）

Corollary 1.1 It is impossible in the asynchronous network model to implement a read/write data object that guarantees the following properties:
          • Availability, in all fair executions,
          • Atomic consistency, in fair executions in which no messages are lost.

推论1.1 在异步网络模型中应用读/写数据对象并满足以下特性是不可能的：
          • 对所有平等请求满足可用性
          • 没有消息丢失下所有平等请求满足原子一致性

 

Theorem 2 It is impossible in the partially synchronous network model to implement a read/write data object that guarantees the following properties:
           • Availability
           • Atomic consistency in all executions (even those in which messages are lost).

定理2 在半异步网络模型中应用一个读/写数据对象并满足以下特性是不可能的：
          • 可用性
          • 在所有请求平等下的原子一致性（包括消息丢失情况）

 

Theorem 4 The modified centralized algorithm is Delayed-t consistent.

定理4 改进的中心算法是延迟 t 时间一致性的。