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.

Authors

• Ulrich Schöpp

Keywords

• Higher-Order Abstract Syntax
• First-Order Logic
• Model Theory
• Categorical Logic