Interpreting L01 formulas

Question

In this formula ∀t1.(t0 ≤ t1 → (∃t0.t1 ≤ t0 ∧ (∀t2.(t1 ≤ t2 ∧ t2 < t0 → c t2 )) ∧ b t0 ) ∨ a t1 )

It says for all points of time t1, t0 is less than t1 and this implies that there is a point in time t0 where t1 <= t0. Isn't this contradictory since we had already said t0 <= t1

Answer 1

No, it is not a contradiction since in predicate logic, you can do bounded renaming which means you can rename bounded variables as you like. Hence, the above formula is equivalent to

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