# [DOUBT] Translation of temporal formula to LO2 In paper 17.02.2021, the solution to the conversion of the formula to LO2 is given. However, I could not understand how the timesteps are assigned to the LO2 formula.

I came up with the below solution while solving, as my understanding was, that F(phi) assigns timestep t1 to phi. Is the answer written below an accepted one?. +1 vote

F[a WU b] is translated to

∃t1. t0≤t1 ∧ (∀t0. (t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2≤t0 → ¬b[t2])) → a[t0]))

which has a free occurrence of t0 and also bound occurrences. You may rename the bound occurrences and then you get the following

∃t1. t0≤t1 ∧ (∀t3. (t1≤t3 ∧ (∀t2. (t1≤t2 ∧ t2≤t3 → ¬b[t2])) → a[t3]))

If now now exchange t2 and t3, you get your formula.
by (142k points)
selected by
Thanks a lot for the explanation. As you mentioned, that exchanging t2 and t3 would yield the equation I got, I wonder if the solution I got would still be accepted.

If so, could you please tell me if any of the 3 solutions would be accepted?
Renaming bound variables does not change the meaning of a formula unless names of free variables in the scope of the quantifier are chosen. Hence, all of the formulas discussed above are equivalent to each other.
Thanks a lot for the help. It makes sense.