On the semantics of the universal quantifier
type: Item
instance of: scholarly article
title: On the semantics of the universal quantifier
zbMATH Open document ID: 0883.03052
DOI: 10.1016/S0168-0072(96)00051-6
author: Djordje Čubrić
published in: Annals of Pure and Applied Logic
publication date: 1998-02-23T00:00:00Z
review text: The author studies the proof theory and categorical semantics of the \((\top,\wedge,\to,\forall)\) fragment of intuitionistic logic, using a class of fibrations which he calls \(\forall\)-fibrations to provide the models. The key observation which makes it easy to prove completeness theorems for this fragment is that the above connectives are precisely those whose interpretations are preserved by the Yoneda embedding (when they exist).
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 18D30
zbMATH DE Number: 1080827
zbMATH Keywords: proof theory
zbMATH Keywords: categorical semantics
zbMATH Keywords: fragment of intuitionistic logic
zbMATH Keywords: fibrations
zbMATH Keywords: completeness theorems
zbMATH Keywords: Yoneda embedding
reviewed by: Peter Johnstone
describes a project that uses: Automath
MaRDI profile type: Publication
cites work: Q4281490
cites work: Fibered categories and the foundations of naive category theory
cites work: Categories for Types
cites work: Q4068706
cites work: Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi
cites work: On the rules of suppositions in formal logic
cites work: The virtues of eta-expansion
cites work: Q4029341
cites work: Q3727946
cites work: Adjointness in Foundations
cites work: Q5642701
cites work: The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 1
cites work: The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 2
cites work: Q4170869
cites work: Q3786612
cites work: An application of open maps to categorical logic
cites work: Q5559220
cites work: HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
cites work: Locally cartesian closed categories and type theory
cites work: Yoneda structures on 2-categories
description: scientific article; zbMATH DE number 1080827