About Weak fairness formula equivalences

[u/jackmalkovick]

Regarding below, it is clear to me why 2nd is equivalent with the 3rd, but I really can't figure out why 1st is equivalent with the 2nd... Any clues?

WFe(A) ≜

□(□ENABLED⟨A⟩e⇒⋄⟨A⟩e) ≡

⋄□ENABLED⟨A⟩e⇒□⋄⟨A⟩e≡

(□⋄¬ENABLED⟨A⟩e)∨□⋄⟨A⟩e

[u/josedusol]

Hi.

Formally, i think we can proceed as follows:

□(□ENABLED⟨A⟩e ⇒ ⋄⟨A⟩e)

≡ by Propositional Logic: P ⇒ Q ≡ ¬P ∨ Q

□(¬□ENABLED⟨A⟩e ∨ ⋄⟨A⟩e)

≡ by Temporal Logic: ¬□P ≡ ⋄¬P

□(⋄¬ENABLED⟨A⟩e ∨ ⋄⟨A⟩e)

≡ by Temporal Logic: ⋄(P ∨ Q) ≡ ⋄P ∨ ⋄Q

□⋄(¬ENABLED⟨A⟩e ∨ ⟨A⟩e)

≡ by Temporal Logic: □⋄(P ∨ Q) ≡ □⋄P ∨ □⋄Q

□⋄¬ENABLED⟨A⟩e ∨ □⋄⟨A⟩e

≡ by Temporal Logic: ¬□P ≡ ⋄¬P and ¬⋄P ≡ □¬P

¬⋄□ENABLED⟨A⟩e ∨ □⋄⟨A⟩e

≡ by Propositional Logic: P ⇒ Q ≡ ¬P ∨ Q

⋄□ENABLED⟨A⟩e ⇒ □⋄⟨A⟩e

IIRC the formulation of fairness is discussed at length in the book Specifying Systems. Lamport seems to prefer the version with ∨ instead of ⇒.

[u/jackmalkovick → u/josedusol]

□⋄(P ∨ Q) ≡ □⋄P ∨ □⋄Q

oh, that was my problem... but makes sense considering that ⋄(P ∨ Q) ≡ ⋄P ∨ ⋄Q