Translation between different logic[2020 Exam paper]

Question

Hello,

I have one doubt regarding the below question.

• ϕ2 = ¬EFE[1 SU ¬a] ∧ AGA[a SB b]

= ¬EFE[1 SU ¬a] ∧ AGA[a SB b]

= ¬EFEF¬a ∧ AGA[a SB b]

= AGAGa ∧ AGA[a SB b]

 = AGAGa ∧ AG [a SB b]

 = AGa ∧ AG(Fa ∧ ¬b)

= AG(a ∧ ¬b)

In the last step, how we are getting AG(a ∧ ¬b) from AGa ∧ AG(Fa ∧ ¬b) ?. Is it because, "a & Fa" can be written as "a".?

Thanks

Answer 1

As AG means “on every step of every infinite path”, we can use the well known conversion:

AGa ∧ AG(Fa ∧ ¬b)  = AGa ∧ AGFa ∧ AG¬b

As a implies Fa, AGa also implies AGFa (intuitively: whenever we satisfy AGa, we also satisfy AGFa, so it makes no difference in the conjunction). Hence, we just drop AGFa. And there you go, a beautifully hand-crafted:

AGa ∧ AG¬b

Comments

Thank You so much for the explanation!