Modelling Generic Judgements

We propose a semantics for the ∇-quantifier of Miller and Tiu. First we consider the case for classical first-order logic. In this case, the interpretation is close to standard Tarski-semantics and completeness can be shown using a standard argument. Then we put our semantics into a broader context by giving a general interpretation of ∇ in categories with binding structure. Since categories with binding structure also encompass nominal logic, we thus show that both ∇-logic and nominal logic can be modelled using the same definition of binding. As a special case of the general semantics in categories with binding structure, we recover Gabbay & Cheney's translation of FOλ∇ into nominal logic.