Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

769 questions

886 answers

1.3k comments

424 users

0 votes
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
in * TF "Emb. Sys. and Rob." by (790 points)

1 Answer

0 votes
 
Best answer
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])
by (117k points)
selected by

Related questions

0 votes
1 answer
asked Feb 12, 2021 in * TF "Emb. Sys. and Rob." by daodubasit (790 points)
0 votes
1 answer
Imprint | Privacy Policy
...