Quantification in Double-Categorical Database Schemas

Double-categorical database schemas are enriched with universal quantification in the form of right adjoints to substitution. This allows phrasing of the important query, relational division. It is shown that such right adjoints together with suitable tabulators interpret modal operators, provide cartesian closed structure, and, when combined with global cocartesian structure, interpret first-order predicate logic and thus description logic. These structures are applied throughout to querying and optimization. It is seen, for example, that Frobenius reciprocity and Beck-Chevalley hold in any suitably structured double database schema and that these provide pushdown optimization rules. Likewise, negation queries are introduced and studied as a result of cocartesian and local implication structure.