Reasoning about knowledge  Part 1
In this series of posts, I will talk about the reasoning about knowledge like how to reach an agreement under different harsh conditions. This field is called Epistemic modal logic and this post will mainly discuss reaching agreement in the presence of faults in the distributed system.
Introduction
Reaching an agreement in the presence of faults in the distributed system is an enduring problem in computer science and epistemic modal logic. The solutions of this problem are widely used in Cryptocurrency and aerospace industry.
One of the most famous algorithms is mentioned in Reaching Agreement in the Presence of Faults, which later became the wellknown Byzantine Fault Tolerance problem.
Conventions
Faulty
Interactive Consistency
Interactive Consistency requires following prerequisites:
 Nonfaulty processors have the same vector.
 In every nonfaulty processor, the element corresponding to a given nonfaulty processor is the private value of that processor.
Problem
Consider there are \(n\) processors in which \(m\) processor(s) is(are) faulty \((n,m\in{}\mathbb{N}_{+})\).
Every processor \(p\) keeps a value \(V_{p}\). And every processor has a vector of \(n\) length, which comprises the values of every processor (include itself). The purpose is devising an algorithm which computes a vector that satisfies the interactive consistency.
Algorithm
The algorithm in the Reaching Agreement in the Presence of Faults is quite abstract and complex. In this section, I will spoil it down for you.
This algorithm only applies to the situation in which \(n>3m\). We will prove that the \(n>3m\) is the necessary and sufficient condition.
In order to describe the algorithm easily, we will describe it in a formal way.
Definitions
Sets
Let \(P\) be a set of processors.
We also need \(n\) trees. Each tree's root node is denoted by one processor's name respectively. Let \(T\) be a set of the trees.
Notation
For any tree \(t\), we denote the properties of that as \(S(d,f)\) in which \(d\) stands for the depth of the tree and \(f\) stands for the number of the faulty processors (include root node) in the subtree.
Functions

Evaluator \(\sigma{}(w)\)
\(\sigma{}(w)\) gives the value of the node which is denoted by the edge \(w\) (\(w\) is a string which comprises names of processors. e.g. \(w=p_{1}p_{2}p_{3}\)).
Furthermore, we can deduce that \(\sigma{}(pw)=\sigma{}(p)\) where \(w\) comprises names of nonfaulty processors since nonfaulty processors always pass on the value directly. 
Sender \(\varphi{}(w)\)
\(\varphi{}(w)\) sends the value of \(\sigma{}(w)\) to every processor \(p\in{}\complement_{P}\scriptsize W\) (\(W\) is a set which comprises all the names of the processors in the \(w\)).

Receiver \(\xi{}(w,v)\to{}w'\)
If the edge is not illegal(trying to override or \(w\) is not ended with the sender's name), \(\xi{}(w)\) will append the receiver's own name to the \(w\) (the new string is called \(w'\)). And store the received value \(v\) to the tree according to the edge \(w'\). Finally, it returns \(w'\)
Procedure
For a processor \(p\in{}P\), follow these steps:
 Performs \(\varphi{}(p)\).
 Receives the values from others by performing \(\xi{}(w,v)\). Then performs \(\varphi{}(w')\).
 Performs step 2 repeatedly until there is nothing to receive.
 (For the first time, starts from the bottom of the tree) Performs the \(majority\) function on a group of nodes which share the same parent, then replaces the value of the parent by the result of the \(majority\) function. In the end, moves to the upper level.
 Performs step 4 repeatedly until the top level.
 Redoes step 4 and 5 for every tree \(t\in{}T\).
The vector of the values of the root nodes of all the trees in \(T\) satisfies the interactive consistency.
Example
This is an example of the tree of processor \(p_{4}\) from viewpoint of \(p_{1}\) (\(n=4,m=1\)):
++  p4    +++       ++  ++    +++ +++ +++  p2   p3   p1        +++ +++ ++   +++ +++  p1   p1      ++ ++
Proofs
Conventions
Interactive Consistency for tree
We call following rules Interactive Consistency for tree:
 For every viewpoint, the evaluated value of the tree is the same. (\(IC'_{1}\))
 If the root node of the tree is nonfaulty, the evaluated value for every viewpoint should be \(\sigma{}(EdgeToRoot)\). (\(IC'_{2}\))
In particular, \(IC'_{1}\) follows from \(IC'_{2}\) if the root node is nonfaulty.
If every tree \(t\in{}T\) satisfies both \(IC'_{1}\) and \(IC'_{2}\), the \(T\) satisfies interactive consistency.
Proof of correctness for \(n>3m\)
Lemma 1
Lemma 1: For all \(n>3m\) cases, tree \(t\in{}T\) satisfy \(IC'_{2}\) if the root node of the tree is nonfaulty.
Proof: Let \(n=3m+k\ (k\in{}\mathbb{N}_{+})\). The degree of any node in depth \(d\) is:
\[D_{d} = \begin{cases}
nd1 &\text{if } d\in{}[0,m] \\
0 &\text{if } d=m+1
\end{cases}\]
For any subtree \(S(i,j)\text{ where }i\in{}[0,m),j\in{}[0,m]\):
\[\tag{1} \begin{aligned}
D_{i}m &= nd1m \\
&= 2m+kd1 \\
&\geq{} m+k
\end{aligned}\]
\(D_{i}m\geq{}m+k\) indicates subtree \(S(i,j)\) can tolerate that at most \(m\) faulty processor(s) is(are) its child(ren) since the majority of its child is nonfaulty processor.
The proof of the Lemma 1 is by induction on \(i\) \((m\geq{}2)\).
 \(Basic\ i=m1\) if the root node of subtree \(S(m1,j)\) is nonfaulty, by (1), we can know that it satisfies \(IC'_{2}\).
 \(Induction\ Step\ i\in{}[0,m2]\) We assume nonfaultyroot subtrees \(S(i+1,j)\) satisfy \(IC'_{2}\), and prove it for nonfaultysubtree subtree \(S(i1,j)\). By (1), we can prove it.
For \(m=1\), it is proved in the basic section in induction proof.
Therefore, tree \(t\in{}T\) of \(S(0,m)\) satisfies \(IC'_{2}\).\(\ \square\)
Theorem 1
Theorem 1 For all \(n>3m\) cases, tree \(t\in{}T\) satisfy both \(IC'_{1}\) and \(IC'_{2}\).
Proof Because \(IC'_{1}\) follows from \(IC'_{2}\) if the root node is nonfaulty, we only need prove the case where the root node is faulty.
By the induction in the proof of Lemma 1, we know that every nonfaulty processor can always get the same value with any nonfaultysubtree \(S(i,j)\text{ where }i\in{}[0,m),j\in{}[0,m]\). So we can replace the value of root node of \(S(i,j)\) with the evaluated value and eliminate every subtree of it.
Obviously, for any faultysubtree \(t'\) whose child(ren) all satisfy \(IC'_{1}\), \(t'\) also satisfies \(IC'_{1}\).
Therefore, \(t\) satisfies \(IC'_{1}\).
Hence, for all \(n>3m\) cases, tree \(t\in{}T\) satisfy both \(IC'_{1}\) and \(IC'_{2}\).\(\ \square\)
Proof of impossibility for \(n\leq{}3m\)
Proof Let \(n=3mk\ (k\in{}\N)\). If \(n\leq{}3m\), then \(D_{i}m\leq{}mk\) in (1), which leads to inevitable failure of \(Basic\) in the induction of Lemma 1. Therefore, Theorem 1 can't be proved.\(\ \square\)
Conclusion
It took me at least 1 month to finish this post. The journey of learning this algorithm is quite hard for me but exciting. This algorithm is the bedrock of many other theories, Libra's consensus algorithm is also based on that. However, this algorithm has many restrictions such as nolatency communication between processors, which are very ideal and unrealistic in reality.
The incentive of writing this post is that few people are trying to spoil it down and prove the algorithm for others. Almost every post of proof or explanation of this algorithm I saw is copypasty post. I think it is essential for me to understand the algorithm thoroughly and write it down for both me and you.
References
 M. Pease, R. Shostak, and L. Lamport. 1980. Reaching Agreement in the Presence of Faults. J. ACM 27, 2 (April 1980), 228234. DOI=http://dx.doi.org/10.1145/322186.322188
 Leslie Lamport, Robert Shostak, and Marshall Pease. 1982. The Byzantine Generals Problem. ACM Trans. Program. Lang. Syst. 4, 3 (July 1982), 382401. DOI=http://dx.doi.org/10.1145/357172.357176