Розглянуто проблему зв'язку між коректністю діаграми подій розподіленого обчислення з погляду комунікації між локальними процесами цього обчислення та існуванням для такої діаграми логічного годинника. Проблему досліджено за допомогою програми The Coq Proof Assistant без припущення про справедливість закону виключення третього. Інакше кажучи, отримані результати є коректними з погляду конструктивної логіки, що важливо для комп'ютерних наук. Формально доведено, що існування логічного годинника для розподіленого обчислення забезпечує іррефлексивність причинно-наслідкового зв'язку, пов'язаного з цим обчисленням. Сформульовано гіпотезу про справедливість оберненого твердження.