Editing Tuple relational calculus (section)

=== Formulas ===

The atoms can be combined into formulas, as is usual in first-order logic, with the logical operators ∧ (and), ∨ (or) and ¬ (not), and we can use the existential quantifier (∃) and the universal quantifier (∀) to bind the variables. We define the ''set of formulas'' ''F''[''S'',''type''] inductively with the following rules:
# every atom in ''A''[''S'',''type''] is also in ''F''[''S'',''type'']
# if ''f''<sub>1</sub> and ''f''<sub>2</sub> are in ''F''[''S'',''type''] then the formula  ''f''<sub>1</sub> ∧ ''f''<sub>2</sub>  is also in ''F''[''S'',''type'']
# if ''f''<sub>1</sub> and ''f''<sub>2</sub> are in ''F''[''S'',''type''] then the formula  ''f''<sub>1</sub> ∨ ''f''<sub>2</sub>  is also in ''F''[''S'',''type'']
# if ''f'' is in ''F''[''S'',''type''] then the formula  ¬ ''f''  is also in ''F''[''S'',''type'']
# if ''v'' in ''V'', ''H'' a header and ''f'' a formula in ''F''[''S'',''type''<sub>[''v''->''H'']</sub>] then the formula  ∃ ''v'' : ''H'' ( ''f'' )  is also in ''F''[''S'',''type''], where ''type''<sub>[''v''->''H'']</sub> denotes the function that is equal to ''type'' except that it maps ''v'' to ''H'',
# if ''v'' in ''V'', ''H'' a header and ''f'' a formula in ''F''[''S'',''type''<sub>[''v''->''H'']</sub>] then the formula  ∀ ''v'' : ''H'' ( ''f'' )  is also in ''F''[''S'',''type'']

Examples of formulas:

* ''t''.name = "C. J. Date" ∨ ''t''.name = "H. Darwen"
* Book(''t'') ∨ Magazine(''t'')
* ∀ ''t'' : {author, title, subject} ( ¬ ( Book(''t'') ∧ ''t''.author = "C. J. Date" ∧ ¬ ( ''t''.subject = "relational model")))
Note that the last formula states that all books that are written by C. J. Date have as their subject the relational model. As usual we omit brackets if this causes no ambiguity about the semantics of the formula.

We will assume that the quantifiers quantify over the universe of all tuples over the domain in the schema. This leads to the following formal semantics for formulas given a database ''db'' over ''S'' and a tuple variable binding ''val'' : ''V'' -> ''T''<sub>''D''</sub>:

#  ''f''<sub>1</sub> ∧ ''f''<sub>2</sub>  is true if and only if  ''f''<sub>1</sub>  is true and  ''f''<sub>2</sub>  is true,
#  ''f''<sub>1</sub> ∨ ''f''<sub>2</sub>  is true if and only if  ''f''<sub>1</sub>  is true or  ''f''<sub>2</sub>  is true or both are true,
#  ¬ ''f''  is true if and only if  ''f''  is not true,
#  ∃ ''v'' : ''H'' ( ''f'' )  is true if and only if there is a tuple ''t'' over ''D'' such that ''dom''(''t'') = ''H'' and the formula  ''f''  is true for ''val''<sub>[''v''->''t'']</sub>, and
#  ∀ ''v'' : ''H'' ( ''f'' )  is true if and only if for all tuples ''t'' over ''D'' such that ''dom''(''t'') = ''H'' the formula  ''f''  is true for ''val''<sub>[''v''->''t'']</sub>.