Can tuple variables bound by quantifiers occur on the left of '|' in Tuple Relational Calculus?

Question

Quoting the general expression of Tuple Relational Calculus (Fundamentals of Database Systems - Elmasri, Navathe; 6th edition)

A general expression of the tuple relational calculus is of the form

{t1.Aj, t2.Ak, ..., tn.Am | COND(t1, t2, ..., tn, tn+1, tn+2, ..., tn+m)}

where t1, t2, ..., tn, tn+1, ..., tn+m are tuple variables, each Ai is an attribute of the relation on which ti ranges, and COND is a condition or formula of the tuple relational calculus. A formula is made up of predicate calculus atoms, which can be one of the following:

1. An atom of the form R(ti), where R is a relation name and ti is a tuple variable. This atom identifies the range of the tuple variable ti as the relation whose name is R. It evaluates to TRUE if ti is a tuple in the relation R, and evaluates to FALSE otherwise.

2. An atom of the form ti.A op tj.B, where op is one of the comparison operators in the set {=, <, ≤, >, ≥, ≠}, ti and tj are tuple variables, A is an attribute of the relation on which ti ranges, and B is an attribute of the relation on which t ranges. An atom of the form ti.A op c or c op tj.B, where op is one of the comparison operators in the set {=, <, ≤, >, ≥, ≠}, ti and tj are tuple variables, A is an attribute of the relation on which ti ranges, B is an attribute of the relation on which tj ranges, and c is a constant value.

*Edit(Thanks to philipxy): The meaning of a query in TRC with respect to the above general expression would be,

For {t|p}--"The result of such a query is the set of all tuples t that evaluate COND(t) to TRUE". For {t.a1,t.a2,...|p}--"we first specify the requested attributes […] for each selected tuple t. Then we specify the condition for selecting a tuple following the bar".

There is also a mention of,

The only free tuple variables in a tuple relational calculus expression should be those that appear to the left of the bar (|).

---

Consider for example, a relation Students(id, grade) and we would like to find the "id's of all students who have secured the highest grade". The query specified in Tuple Relational Calculus could be

Q1 = {s1. id | students(s1) ^ ¬(∃ s2, students(s2) ^ ( s2. grade > s1.grade) )}

Here, s1 is the free variable.

Q1 can be interpreted as all id values of tuple variable s1, where s1 ranges within the relation student (i.e. s1 belongs to student) AND there does not exist a variable s2 such that s2 belongs to student and s2.grade > s1.grade.

Consider the queries,

Q2 = {s1. id | ∃ s1, students(s1) ^ ¬(∃ s2, students(s2) ^ ( s2. grade > s1.grade) )}

and

Q3 = {s1. id | ∀ s1, students(s1) ^ ¬(∃ s2, students(s2) ^ ( s2. grade > s1.grade) )}

As we can see, s1 (variable on the left of the bar) in Q2 and Q3 is also bounded by ∃ and ∀ respectively.

How is the interpretation of Q2 and Q3 different from Q1 assuming Q2 and Q3 are even possible ?

---

Note:

• Queries Q2 and Q3 were made up from Q1 with the purpose of trying to understand what the queries would mean if the variables on the left side of '|' were bound by existential or universal quantifiers.
• (Edit, after thinking a bit more) My interpretation of Q2 and Q3 is that the result of Q2 and Q1 will be the same will not be the same as Q2 will produce all id values of s1 if there exists atleast one s1 that belongs to student and for which there does not exist s2 such that s2 belongs to student and s2.grade > s1.grade (meaning, the result of Q2 is the "set of all student id if there exists atleast one student who got the highest grade"). Q3 will produce all id values of s1 if for every s1 that belongs to student and for which there does not exist s2 such that s2 belongs to student and s2.grade > s1.grade (meaning, the result of Q3 is the "set of all student id if every student got the highest grade"). But, I'm not sure if the queries Q2 and Q3 are even possible or even if such a scenario where the variables on the left of the bar are also bounded by quantifiers could occur in general.