Dependently Sorted Logic

Abstract. We propose syntax and semantics for systems of intuitionistic and classical first order dependently sorted logic, with and withlity, retaining type dependency, but otherwise abstracting, from systems for dependent type theory, and which can be seen as generalised systems of multisorted logic. These are presented as extensions to Gentzen systems for first order logic in which the logic is developed relative to a context of variable declarations over a theory of dependent sorts. A generalised notion of Kripke structure provides the semantics for the intuitionistic systems.

• Type: Conference
• Year: 2007
• Where: TYPES
• Authors: João Filipe Belo
• Keywords: Classical first Order, Formal Methods, TYPES 2007, first Order, first Order Logic