A Logical Interpretation of the CAP Theorem

The three component properties of the CAP theorem have been explained to death in other places. The zeitgeist reminds you daily that any system can only exhibit two out of those three properties, and that you must pick P. That is, the only possible system configurations are CP, AP, and CA.

But nobody really talks about what the logical form of these two three combinations actually are. As this question was implicitly raised in two recent blog posts—here and here—now seems like an opportune time to write down their logical forms, thus clarifying the way in which P, and its absence, are interpreted in these system descriptions. So here are their logical forms, in prose and symbols.

Consistency/Partition Tolerance

For any given system state σ, if the system is experiencing a network partition—e.g., P(σ) holds—then the system will be able to handle operations while maintaining consistency or it will become unavailable—e.g., C(σ) ∨ ¬A(σ) holds. In other words:

CP ≡ ∀σ. P(σ) ⇒ C(σ) ∨ ¬A(σ)

Availability/Partition Tolerance

For any given system state σ, if the system is experiencing a network partition then the system will be able to handle operations (consistently or inconsistently) while maintaining availability—e.g., A(σ) holds. Using symbols instead of words:

AP ≡ ∀σ. P(σ) ⇒ A(σ)

Consistency/Availability

For any given system state σ, if the system is not experiencing a network partition then the system will be able to handle operations while maintaining both availability and consistency. For the sake of Frege:

CA ≡ ∀σ. ¬P(σ) ⇒ C(σ) ∧ A(σ)

Using contraposition, it’s straightfoward to conclude that this is equivalent to:

∀σ. ¬C(σ) ∨ ¬A(σ) ⇒ P(σ)

Logic is Symbols, Logic is Simple

Recall that the truth tables for logical implication, both for when the antecedent is not negated and when it is negated, are as follows:

The first two rows are the important ones. One of the aforementioned posts claims that a system cannot remain CA during a network partition by becoming unavailable. Taking X ≡ P(σ) and Y ≡ C(σ) ∧ A(σ), the second row of the truth table says that you can. Since X is true, the system is experiencing a network partition. At the same time Y is false, so either the system is unavailable or will behave inconsistently. Yet the table still states that ¬X ⇒ Y is true, i.e., the CA property is preserved in this system state.

While this seems to contradict the CAP theorem, it does not. The consistency and availability of a CA system are predicated on there not being a network partition. If there is no network partition, then the system is available and consistent. But what if there is a network partition? The CA property says nothing about the behavior of the system during that time. It does not say that availability will be maintained. It does not say that consistency will be maintained. Translated to the language of meaningless symbols that know nothing about computer:

P(σ₀), ∀σ. ¬P(σ) ⇒ C(σ) ∧ A(σ) ⊭ A(σ₀) P(σ₀), ∀σ. ¬P(σ) ⇒ C(σ) ∧ A(σ) ⊭ C(σ₀)

Simply put, you cannot deduce availability or consistency from the assumptions of a CA system and a network partition in a particular system state, here written as σ₀.

The confusion may arise from the first row of the truth table, which states that the CA property can be preserved by a system state that is experiencing a network partition, and is both available and consistent. In general this can’t happen because of the CAP theorem. But of course, since CA doesn’t really say anything about the behavior of a system while experiencing a partition, it may have some limited capacity to handle a certain subset of possible network partitions, sort of like a CP system!

CP Systems are Useless

Strictly speaking, you have to assume this without knowing anything else about the system. This is because the CP property only says something about the behavior of the system during a network partition. What about the times when there is no network partition? Just like you can’t deduce availability or consistency from the CA property in the presence of a network partition, similarly you cannot deduce availability or consistency from the CP property in the absence of a network partition. In lyrical syntax:

¬P(σ), ∀σ. P(σ) ⇒ C(σ) ∨ ¬A(σ) ⊭ A(σ₀) ¬P(σ), ∀σ. P(σ) ⇒ C(σ) ∨ ¬A(σ) ⊭ C(σ₀)

And yet, most CP systems are built to be available and consistent during normal operations, in the absence of a network partition. That sounds like a familiar property. It sounds like all CP systems that are in popular use today are also CA systems:

CP' ≡ CP ∧ CA

So clearly, CA ∩ CP' ≠ ∅. In fact CA ∩ CP' = CP'. Practically speaking, any useful CP system is going to also be CA. It doesn’t really make sense to talk about one without the other. Or perhaps all of this is too restrictive and there’s another way to think about it.

CP ∧ CA ≠ CAP

— or —

A Wittgensteinian Language Puzzle?

There seems to be common misconception that the symbols C, A, and P individually represent logical propositions. By concatenating these symbols to produce things like CP, for example, you create a new symbol whose meaning is determined by the conjunction of the logical propositions that correspond to C and P. Restated in a way that may clarify for some, but obfuscate for others, it’s commonly assumed that the denotational mapping from the syntactic monoid generated by {C, A, P} is a homomorphism, with a left inverse. Given the preceding text, that seems to not be the case, and for a very simple reason: P by itself has no useful denotation. Sure, a system may be partition tolerant, but with respect to what invariant? It can’t just be partition tolerant period, full stop. That conveys no useful information about the behavior of the system.

Rather, the presence or absence of P in the description of a system property must modify the scope of the property to the presence or absence of network partitions, respectively.

Thanks to Evan Jones and Justin DeBrabant for reading drafts of this post.