Abstract. This paper addresses the problem of the relationship between the correctness of the event diagram of distributed computing from the standpoint of communication between local processes of this computing and the existence of a logical clock for that diagram. The problem is analyzed using The Coq Proof Assistant software without assuming the fairness of the principle of excluded middle. That is, the obtained results are correct from the point of view of constructive logic, which is essential for computer science. It has been formally proved that the existence of a logical clock for distributed computing ensures the irreflexivity of the causal relation related to that computing. The conjecture about the fairness of the converse statement has been claimed.

Keywords: distributed computing, cloud platform, blockchain, digital distributed ledgers, global time, logical clock, event ordering.