Categories with families and first-order logic with dependent sorts

DOI10.1016/J.APAL.2019.102715zbMATH Open1458.18003arXiv1605.01586OpenAlexW2955445504WikidataQ127577540 ScholiaQ127577540MaRDI QIDQ2326422FDOQ2326422

Authors: Erik Palmgren 

Publication date: 7 October 2019

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Abstract: First-order logic with dependent sorts, such as Makkai's first-order logic with dependent sorts (FOLDS), or Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL), may be regarded as logic enriched dependent type theories. Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-L"of type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and DFOL fit in this semantical framework. A soundness and completeness theorem is proved for DFOL. The semantics is functorial in the sense of Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra for a DFOL theory. Agreement with standard first-order semantics is established. Applications of DFOL to constructive mathematics and categorical foundations are given. A key feature is a local propositions-as-types principle.

Full work available at URL: https://arxiv.org/abs/1605.01586

Recommendations

• First-Order Logic with Dependent Types
• Dependently Sorted Logic
• Categories with families: unityped, simply typed, and dependently typed
• scientific article; zbMATH DE number 1241699
• Full Lambek Hyperdoctrine: Categorical Semantics for First-Order Substructural Logics

zbMATH Keywords

categorical logicdependent typesintuitionistic first-order logicmodels of type theory

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Categorical logic, topoi (03G30) Theories (e.g., algebraic theories), structure, and semantics (18C10) Semantics in the theory of computing (68Q55)

Cites Work

• Categorical logic and type theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Generalized algebraic theories and contextual categories
• Title not available (Why is that?)
• AN ELEMENTARY THEORY OF THE CATEGORY OF SETS
• Internal type theory
• A minimalist two-level foundation for constructive mathematics
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets
• Proof-relevance of families of setoids and identity in type theory
• Title not available (Why is that?)
• The generalised type-theoretic interpretation of constructive set theory
• Dependently Sorted Logic
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories

Cited In (6)

• First-Order Logic with Dependent Types
• A formal logic for formal category theory
• Determinisation of relational substitutions in ordered categories with domain
• A 2-categorical analysis of context comprehension
• Translating a Dependently-Typed Logic to First-Order Logic
• Homotopical inverse diagrams in categories with attributes

This page was built for publication: Categories with families and first-order logic with dependent sorts

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2326422)