# Use of existential quantifier in tuple relational calculus

It is somewhat confusing to me when to use quantifiers in tuple relational calculus (TRC). I stumbled upon following problem and I am still scratching my head thinking why not TRC query can be constructed without using existential quantifier.

The given problem reads like this:

Relations:
student (rollNo, name, degree, year, sex, deptNo, advisor)
department (deptId, name, hod, phone)
professor (empId, name, sex, startYear, deptNo, phone)
course (courseId, cname, credits, deptNo)
enrollment (rollNo, courseId, sem, year, grade)
teaching (empId, courseId, sem, year, classRoom)
preRequisite(preReqCourse, courseID)

Question: Obtain the names of courses enrolled by student named "Roger".

Given solution:

{ c.name | course(c) ^
(∃s) (∃e) ( student(s) ^
enrollment(e) ^
s.name = “Roger” ^
s.rollNo= e.rollNo ^
c.courseId = e.courseId}


Why I cant just have following? :

{c.name | course(c) ^
enrollment(e) ^
student(s) ^
c.courseId = e.courseId ^
e.rollNo = s.rollNo ^
s.name = "Roger" }


Something like { c.name | ... } is shorthand for something like

{z : (name) | (∃c) (z.name = c.name ^ ...) }.


As described on, e.g., the Wikipedia page, the fundamental form of the set comprehension (i.e. query) notation expects a variable to the left of the |. If you are familiar with anonymous functions/lambda notation, it is very similar to $\lambda z.(\dots)$. If we named it, it's like we're defining a predicate $P(z)\equiv(\dots)$. The upshot is that the notation effectively binds z (or c in the original form). But in your version without existential quantifiers, nothing is binding e or s. It's like you're referring to undeclared variables in a programming language.

Since whether the variables are bound with a universal or existential quantifier and where exactly that quantifier appears in the formula are all relevant, it would be difficult to infer which quantifiers should be added and where. (And as an additional possibility, we could just imagine that the variables are completely free and essentially become additional parameters to the anonymous predicate we're defining, but that doesn't fit in well with the Tuple Relational Calculus.) Prolog and Datalog do use a syntax that makes existential quantifiers implicit, but they are (in their basic forms) also limited to a language that 1) omits universal quantifiers, and 2) only allows formulas where existential quantifiers can always be pulled to being the outermost connective. Actually, when negation is added to Datalog, this stops being true and this implicit syntax starts to become ambiguous and confusing. Some implementations add an explicit existential and/or universal quantifier in such cases.

The upshot is, at the most fundamental level, all variables need to be bound, either by a quantifier or by the set comprehension syntax. There do exist various shorthands and conventions that are often used that can cloud this picture up, but ultimately every variable is introduced by some binding form.

• Seems that I am unable to match your frequency and hence not able to get the point from your answer. One neat question: Is it (existential quantifier is used) because, omitting existential quantifier will return single course multiple times if there are more than one student named "Roger" enrolled to it? With existential quantifier, such course will be returned only once. – anir May 13 '18 at 13:38
• No. Without the existential quantifier (or some other binder), you just have a syntax error (i.e. an ill-formed [closed] formula). It's just meaningless if you don't bind all the variables. It's like you saying, "Computer! Is $x > 5$?" It's going to respond, "I can't answer that. I don't know what $x$ is." If you instead asked, "Does there exist an $x>5$?", i.e. ($\exists x.x >5$) then the computer can readily answer, "yes". – Derek Elkins May 13 '18 at 18:33
• Did you mean that every variable should be bound by quantifier? Please check page 13, section 6.6.4, 3rd bullet point of this. The query is {e.FNAME, e.LNAME, s.FNAME, s.LNAME | EMPLOYEE(e) and EMPLOYEE(s) and e.SUPERSSN = s.SSN}. It has variables not bound by quantifier. – anir May 17 '18 at 16:32
• The convention being used there is what I explain at the very beginning of my answer. There's an implied existential quantifier binding e and s so that expression is equivalent to {z | (∃e)(∃s) (z.FNAME = e.FNAME ^ z.LNAME = e.LNAME ^ z.FNAME = s.FNAME ^ z.LNAME = s.LNAME ^ EMPLOYEE(e) ^ EMPLOYEE(s) ^ e.SUPERSSN = s.SSN) }. When using this convention, there can be no unbound variables to the right of the | that don't also appear to the left of the |. Also, I didn't say every variable should be bound by a quantifier, I said every variable should be bound. {z | ...} binds z. – Derek Elkins May 17 '18 at 18:43