Categories with families and first-order logic with dependent sorts

DOI10.1016/J.APAL.2019.102715MaRDI QIDQ2326422zbMATH OpenOpenAlexWikidataFDO

Authors Erik Palmgren

Publication date 7 October 2019

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

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

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)

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.

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

Cites work

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

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)