HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION

DOI10.1002/MALQ.19830291005MaRDI QIDQ3679177zbMATH OpenOpenAlexFDO

Authors R. A. G. Seely

Publication date 1983

Published in Mathematical Logic Quarterly (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1002/malq.19830291005

zbMATH Keywords

substitutionquantifiersadjointnesspull-backfibered categorieshyperdoctrineassociated theorycategory of types

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Fibered categories (18D30)

Recommendations

• scientific article; zbMATH DE number 4002342
• Full Lambek Hyperdoctrine: Categorical Semantics for First-Order Substructural Logics
• Fibred algebraic semantics for a variety of non-classical first-order logics and topological logical translation
• Partial hyperdoctrines: categorical models for partial function logic and Hoare logic
• Elementary doctrines as coalgebras

Cited in

(33)

• A minimalist two-level foundation for constructive mathematics
• On duality and model theory for polyadic spaces
• Graded multicategories of polynomial-time realizers
• scientific article; zbMATH DE number 29052 (Why is no real title available?)
• A category-theoretic account of program modules
• Polyadic spaces and profinite monoids
• Coherence in linear predicate logic
• A general framework for the semantics of type theory
• The proof monad
• A characterization of generalized existential completions
• A fully abstract semantics for concurrent constraint programming
• Elementary doctrines as coalgebras
• On the algebraic structure of declarative programming languages
• Smooth and proper maps with respect to a fibration
• Categorical proof-theoretic semantics
• Dialectica principles via Gödel doctrines
• On the semantics of the universal quantifier
• Hyperdoctrines and the ontology of stratified semantics
• Some properties of internal locale morphisms externalised
• New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic
• Fibred algebraic semantics for a variety of non-classical first-order logics and topological logical translation
• On the semantics of classical disjunction
• Alpha conversion, conditions on variables and categorical logic
• Deep fried logic
• scientific article; zbMATH DE number 7533330 (Why is no real title available?)
• From proof-theoretic validity to base-extension semantics for intuitionistic propositional logic
• A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine
• First-order homotopical logic
• Categorical semantics for higher order polymorphic lambda calculus
• Categories with families and first-order logic with dependent sorts
• Internal diagrams and archetypal reasoning in category theory
• Dictoses
• Proof-search in type-theoretic languages: An introduction

This page was built for publication: HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION

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